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