Changes between Version 7 and Version 8 of TypeNats/InductiveDefinitions
 Timestamp:
 Mar 21, 2012 1:37:19 AM (2 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/InductiveDefinitions
v7 v8 1 The module {{{GHC.TypeLits}}} provides two views on values of type {{{TNat}}}, 2 which make it possible to define inductive functions using {{{TNat}}} values. 3 4 == Checking for Zero (Unary Strucutre of Nat) == 5 6 The first view provides the same functionality as usual 7 Peano arithmetic definition of the natural numbers. It 8 is useful when using {{{TNat}}} to count something. 1 9 {{{ 2 {# LANGUAGE TypeNaturals, GADTs #} 10 isZero :: TNat n > IsZero n 3 11 4 import GHC.TypeNats 5 import Unsafe.Coerce 12 data IsZero :: Nat > * where 13 IsZero :: IsZero 0 14 IsSucc :: !(TNat n) > IsZero (n + 1) 15 }}} 6 16 7  8  Extending GHC.TypeNats with these two declarations allows us to 9  write inductive definitions. 10 11 data UNat :: Nat > * where 12 Zero :: UNat 0 13 Succ :: UNat n > UNat (n + 1) 14 15 toUNat :: Nat n > UNat n 16 toUNat n = unsafe (natToInteger n) 17 where unsafe :: Integer > UNat n 18 unsafe 0 = unsafeCoerce Zero 19 unsafe n = unsafeCoerce (Succ (unsafe $! (n1))) 20 21  22 23 data Vec :: Nat > * > * where 24 Nil :: Vec 0 a 25 Cons :: a > Vec n a > Vec (n + 1) a 26 27 instance Show a => Show (Vec n a) where 28 show Nil = "[]" 29 show (Cons x xs) = show x ++ " : " ++ show xs 30 31 instance Functor (Vec n) where 32 fmap f Nil = Nil 33 fmap f (Cons x xs) = Cons (f x) (fmap f xs) 34 35 cat :: Vec m a > Vec n a > Vec (m + n) a 36 cat Nil ys = ys 37 cat (Cons x xs) ys = Cons x (cat xs ys) 38 39 vecLen :: NatI n => Vec n a > Nat n 40 vecLen _ = nat 17 By using {{{isZero}}} we can check if a number is 0 or the successor 18 of another number. The interesting aspect of {{{isZero}}} is that 19 the result is typed: if {{{isZero x}}} returns {{{IsSucc y}}}, 20 then the type checker knows that the type of {{{y}}} is one smaller 21 then {{{x}}}. 41 22 42 23 43 splitU :: UNat m > Vec (m + n) a > (Vec m a, Vec n a) 44 splitU Zero xs = (Nil, xs) 45 splitU (Succ n) (Cons x xs) = let (as,bs) = splitU n xs 46 in (Cons x as, bs) 24 == Checking for Evenness (Binary Structure of Nat) == 47 25 48 vecSplitAt :: Nat m > Vec (m + n) a > (Vec m a, Vec n a) 49 vecSplitAt n = splitU (toUNat n) 26 The other view provides a more "bitoriented" view of 27 the natural numbers, by allowing is to check if the least 28 significant bit of a number is 0 or 1. It is useful 29 when we use {{{TNat}}} values for splitting things 30 in half: 31 {{{ 32 isEven :: TNat n > IsEven n 50 33 51 vecSplit :: NatI m => Vec (m + n) a > (Vec m a, Vec n a) 52 vecSplit = vecSplitAt nat 34 data IsEven $a where 35 IsEvenZero :: IsEven 0 36 IsEven :: !(TNat (n + 1)) > IsEven (2 * (n + 1)) 37 IsOdd :: !(TNat n) > IsEven ((2 * n) + 1) 53 38 }}}