Safe Haskell | Safe-Inferred |
---|
Type level peano natural number, some arithmetic functions and their singletons.
- data Nat
- data SNat n where
- sZ :: SNat Z
- sS :: SNat n -> SNat (S n)
- min :: Nat -> Nat -> Nat
- type family Min n m :: Nat
- sMin :: SNat n -> SNat m -> SNat (Min n m)
- max :: Nat -> Nat -> Nat
- type family Max n m :: Nat
- sMax :: SNat n -> SNat m -> SNat (Max n m)
- type family n :+: m :: Nat
- (%+) :: SNat n -> SNat m -> SNat (n :+: m)
- type family n :*: m :: Nat
- (%*) :: SNat n -> SNat m -> SNat (n :*: m)
- type family n :-: m :: Nat
- (%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m)
- data Leq n m where
- class n :<= m
- type family n :<<= m :: Bool
- data LeqInstance n m
- leqRefl :: SNat n -> LeqInstance n n
- leqSucc :: SNat n -> LeqInstance n (S n)
- boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
- boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
- propToClassLeq :: Leq n m -> LeqInstance n m
- class Sing n where
- data SingInstance a where
- SingInstance :: Sing a => SingInstance a
- singInstance :: SNat n -> SingInstance n
- natToInt :: Integral n => Nat -> n
- intToNat :: (Integral a, Ord a) => a -> Nat
- sNatToInt :: Num n => SNat x -> n
- type Zero = Z
- type One = S Zero
- type Two = S One
- type Three = S Two
- type Four = S Three
- type Five = S Four
- type Six = S Five
- type Seven = S Six
- type Eight = S Seven
- type Nine = S Eight
- type Ten = S Nine
- type Eleven = S Ten
- type Twelve = S Eleven
- type Thirteen = S Twelve
- type Fourteen = S Thirteen
- type Fifteen = S Fourteen
- type Sixteen = S Fifteen
- type Seventeen = S Sixteen
- type Eighteen = S Seventeen
- type Nineteen = S Eighteen
- type Twenty = S Nineteen
- sZero :: SNat Z
- sOne :: SNat One
- sTwo :: SNat Two
- sThree :: SNat Three
- sFour :: SNat Four
- sFive :: SNat Five
- sSix :: SNat Six
- sSeven :: SNat Seven
- sEight :: SNat Eight
- sNine :: SNat Nine
- sTen :: SNat Ten
- sEleven :: SNat Eleven
- sTwelve :: SNat Twelve
- sThirteen :: SNat Thirteen
- sFourteen :: SNat Fourteen
- sFifteen :: SNat Fifteen
- sSixteen :: SNat Sixteen
- sSeventeen :: SNat Seventeen
- sEighteen :: SNat Eighteen
- sNineteen :: SNat Nineteen
- sTwenty :: SNat Twenty
- type N0 = Z
- type N1 = One
- type N2 = Two
- type N3 = Three
- type N4 = Four
- type N5 = Five
- type N6 = Six
- type N7 = Seven
- type N8 = Eight
- type N9 = Nine
- type N10 = Ten
- type N11 = Eleven
- type N12 = Twelve
- type N13 = Thirteen
- type N14 = Fourteen
- type N15 = Fifteen
- type N16 = Sixteen
- type N17 = Seventeen
- type N18 = Eighteen
- type N19 = Nineteen
- type N20 = Twenty
- sN0 :: SNat Z
- sN1 :: SNat One
- sN2 :: SNat Two
- sN3 :: SNat Three
- sN4 :: SNat Four
- sN5 :: SNat Five
- sN6 :: SNat Six
- sN7 :: SNat Seven
- sN8 :: SNat Eight
- sN9 :: SNat Nine
- sN10 :: SNat Ten
- sN11 :: SNat Eleven
- sN12 :: SNat Twelve
- sN13 :: SNat Thirteen
- sN14 :: SNat Fourteen
- sN15 :: SNat Fifteen
- sN16 :: SNat Sixteen
- sN17 :: SNat Seventeen
- sN18 :: SNat Eighteen
- sN19 :: SNat Nineteen
- sN20 :: SNat Twenty
Natural numbers and its singleton type
Peano natural numbers. It will be promoted to the type-level natural number.
Smart constructors
Arithmetic functions and thir singletons.
Type-level predicate & judgements
Comparison witness via GADTs.
data LeqInstance n m Source
leqRefl :: SNat n -> LeqInstance n nSource
leqSucc :: SNat n -> LeqInstance n (S n)Source
boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n mSource
propToClassLeq :: Leq n m -> LeqInstance n mSource
Type-classes for singletons
Singleton type-class. This class will be removed soon after singletons package available for the latest Haskell Paltform.
data SingInstance a whereSource
Witness for Sing
instance.
This type will be removed soon after singletons package available for the latest Haskell Paltform.
SingInstance :: Sing a => SingInstance a |
singInstance :: SNat n -> SingInstance nSource
Get witness for singleton integers. This function will be removed soon after singletons package available for the latest Haskell Paltform.