22 Sep
2008
22 Sep
'08
10:20 p.m.
data Nat a where Z :: Nat a S :: Nat a -> Nat (S a)
data Z data S a
n00 = Z n01 = S n00 n02 = S n01 n03 = S n02 n04 = S n03
data MaxList t where Nil :: MaxList a Cons :: Nat a -> MaxList a -> MaxList a
a = Cons n02 $ Cons n02 $ Cons n01 $ Nil --- ":t a" gives "forall a. MaxList (S (S a))" which tells you exactly --- what you want: elements are at least 2.
mlTail :: forall t. MaxList t -> MaxList t mlTail (Cons h t) = t
Is there a way to define a function that only takes a list with a max of 1? Because only1 :: MaxList (S a) -> String only1 _ = "only1" will work over
a = Cons n02 $ Cons n02 $ Cons n01 $ Nil without any problems