Changes between Version 1 and Version 2 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 4:36:40 PM (5 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v1 v2  
    99{{{
    1010module GHC.TypeNats where
     11}}}
    1112
    12 data Nat (n :: Nat)                                     -- Abstract "singleton" types.
     13== Basic Operations ==
    1314
    14 natToInteger :: Nat n -> Integer                        -- Convert a singleton to an integer.
    15 integerToNat :: Integer -> (forall n. Nat n -> a) -> a  -- Convert an integer into a singleton.
     15{{{
     16data Nat n
    1617
    1718class TypeNat n where
    18   nat :: Nat n                                          -- A value in a "singleton" type.
     19  nat :: Nat n
    1920
    20  instance TypeNat 0
    21  instance TypeNat 1
    22  instance TypeNat 2
    23  ...
     21natToInteger :: Nat n -> Integer
    2422
    25 -- property:  natToInteger (nat :: Nat n) == n
     23checkNat :: TypeNat n => (Integer -> Bool) -> Maybe (Nat n)
    2624}}}
     25
     26== Type-Level Operations ==
     27
     28{{{
     29type family m ^ n :: Nat
     30type family m * n :: Nat
     31type family m + n :: Nat
     32class m <= n
     33}}}
     34
     35== Natural Numbers ==
     36
     37{{{
     38data Natural = forall n . Natural !(Nat n)
     39
     40data NaturalInteger
     41  = Negative Natural
     42  | NonNegative Natural
     43
     44toNaturalInteger :: Integer -> NaturalInteger
     45
     46subNatural :: Natural -> Natural -> NaturalInteger
     47}}}