Changes between Version 1 and Version 2 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 4:36:40 PM (3 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}}}