Changes between Version 5 and Version 6 of TypeNats/InductiveDefinitions
 Timestamp:
 Feb 7, 2011 8:12:28 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/InductiveDefinitions
v5 v6 6 6 7 7  8  Extending GHC.TypeNats with these two declarationsallows us to8  Extending GHC.TypeNats with these two function allows us to 9 9  write inductive definitions. 10 10 … … 17 17 where unsafe :: Integer > UNat n 18 18 unsafe 0 = unsafeCoerce Zero 19 unsafe n = unsafeCoerce (Succ (unsafe (n1)))19 unsafe n = unsafeCoerce (Succ (unsafe $! (n1))) 20 20 21 21  … … 29 29 show (Cons x xs) = show x ++ " : " ++ show xs 30 30 31 cat :: Vec m a > Vec n a > Vec (m + n) a 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 32 36 cat Nil ys = ys 33 37 cat (Cons x xs) ys = Cons x (cat xs ys) 34 35 split :: UNat m > Vec (m + n) a > (Vec m a, Vec n a)36 split Zero xs = (Nil, xs)37 split (Succ n) (Cons x xs) = case split n xs of38 (as,bs) > (Cons x as, bs)39 38 40 39 vecLen :: NatI n => Vec n a > Nat n 41 40 vecLen _ = nat 42 41 43 autoSplit :: NatI m => Vec (m + n) a > (Vec m a, Vec n a)44 autoSplit xs = res45 where res@(as,_) = split len xs46 len = toUNat (vecLen as)47 }}}48 42 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) 49 47 48 vecSplitAt :: Nat m > Vec (m + n) a > (Vec m a, Vec n a) 49 vecSplitAt n = splitU (toUNat n) 50 51 vecSplit :: NatI m => Vec (m + n) a > (Vec m a, Vec n a) 52 vecSplit = vecSplitAt nat 53 }}}