[Haskell] Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types

[MR K P SCHUPKE]

Just a couple of quick points...

Why store the length along with the list, the length is stored
using type level naturals (Succ | Zero) but these are identical
to the recursion pattern in a List (Cons | Nil) - therefore it
is no less work than having a length function which converts
from one to the other (Cons x -> Succ, Nil -> Zero), so
it is really redundant having both.

Second you can express append in a much simpler and readable
way in Haskell using type classes:

-------------------------------------------------------------

data Nil deriving Show
data List a = Cons a (List a) deriving Show

class Append l l' l'' | l l' -> l'' where
   append :: l -> l' -> l''
instance List l' => Append Nil l' l' where
   append _ l' = l'
instance Append l l' l'' => Append (Cons a l) l' (Cons a l'') where
   append (Cons a l) l' = Cons a (append l l')

-------------------------------------------------------------

Thats the complete definition, no need for extra stuff or
complex exqualities or casts...

Doesn't look too bad to me.

	Keean.