Skip to content

HORIZON HASKELL Docs lts/ghc-9.14.x7a6c33e2026-10-12Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · 7a6c33e · 2026-10-12

Modulelinear-base-0.8.1

Data.Arity.Linear.Internal

1 type
1 class

Packagelinear-base-0.8.1
Exports6
LicenceMIT

familytype family Arity b f :: Nat where

Equations

Arity b b = 0
Arity b (a %1 -> f) = Arity b f + 1
Arity b f = TypeError (((('Text "Arity: " ':<>: 'ShowType f) ':<>: 'Text " isn't a linear function with head ") ':<>: 'ShowType b) ':<>: 'Text ".")

familytype family FunN (n :: Peano) a b where

Equations

FunN 'Z _1 b = b
FunN ('S n) a b = a %1 -> FunN n a b

classclass IsFunN a b f

Instances2IsFunN

IsFunN a b bDefined in linear-base-0.8.1 · Data.Arity.Linear.Internal
(IsFunN a b f, a' ~ a, p ~ 'One) => IsFunN a b (a' %p -> f)Defined in linear-base-0.8.1 · Data.Arity.Linear.Internal

familytype family NatToPeano (n :: Nat) :: Peano where

Equations

NatToPeano 0 = 'Z
NatToPeano n = 'S (NatToPeano (n - 1))

datadata Peano

Constructors

Z
S Peano

familytype family PeanoToNat (n :: Peano) :: Nat where

Equations

PeanoToNat 'Z = 0
PeanoToNat ('S n) = 1 + PeanoToNat n