Andrew Coppin wrote:
I was actually thinking more along the lines of a programming language where you can just write
head :: (n > 1) => List n x -> x
Current GHC can approximate this with a GADT: ========================================== {-# OPTIONS -fglasgow-exts #-} module SafeHead where data Z data S a data List n a where Nil :: List Z a Cons :: a -> List n a -> List (S n) a head1 :: List (S n) a -> a head1 (Cons x _) = x -- head1 Nil = undefined -- error: inaccessible -- test0 = head1 Nil -- error: Z /= S n test1 = head1 (Cons 'a' Nil) ========================================== For more complex type arithmetic, you need the GHC 6.8RC for type families: ========================================== data TT -- true data FF -- false type family Geq a b -- a >= b type instance Geq a Z = TT type instance Geq Z (S n) = FF type instance Geq (S n) (S m) = Geq n m head2 :: Geq n (S Z) ~ TT => List n a -> a head2 (Cons x _) = x -- head2 Nil = undefined -- no error, but useless -- test2 = head2 Nil -- error: TT /= Geq Z (S Z) test3 = head2 (Cons 'a' Nil) ========================================== Of course, the downside is that using the List GADT can be inconvenient since you need to be able to express _in a static way_ the length of the lists: (++) :: List n a -> List m a -> List (Sum n m) a (\\) :: List n a -> List m a -> List (???????) a The (\\) case is impossible to predict (if you know only the lengths), so you probably need to return a simple [a] there. Of course, you can recover a "better" type with un-time checks, as in (roughly) checkLength :: [a] -> n -> Maybe (List n a) Regards, Zun.