[Haskell-cafe] Re: Type-level arithmetic

[Roberto Zunino]

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.