[Haskell-cafe] Finite but not fixed length...

[Miguel Mitrofanov]

  hdList :: List a n -> Maybe a
hdList Nil = Nothing
hdList (Cons a _) = Just a

hd :: FiniteList a -> Maybe a
hd (FL as) = hdList as

*Finite> hd ones

this hangs, so, my guess is that ones = _|_


13.10.2010 12:13, Eugene Kirpichov пишет:
> {-# LANGUAGE ExistentialQuantification, GADTs, EmptyDataDecls #-}
> module Finite where
>
> data Zero
> data Succ a
>
> class Finite a where
>
> instance Finite Zero
> instance (Finite a) =>  Finite (Succ a)
>
> data List a n where
>    Nil :: List a Zero
>    Cons :: (Finite n) =>  a ->  List a n ->  List a (Succ n)
>
> data FiniteList a where
>    FL :: (Finite n) =>  List a n ->  FiniteList a
>
> nil :: FiniteList a
> nil = FL Nil
>
> cons :: a ->  FiniteList a ->  FiniteList a
> cons a (FL x) = FL (Cons a x)
>
> list123 = cons 1 (cons 2 (cons 3 nil))
>
> ones = cons 1 ones -- typechecks ok