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

[Martin Sulzmann]

The append example is meant to make a general point about
the connection between dependent types and Haskell with
extensions. 

I know that the example itself is rather trivial, and
DML/index types, Omega, Haskell+GAD and Chameleon might
seem as too big canons for a rather small target.

 > 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.
 > 

Good, I was waiting for some type class trickery :)
You turn clauses into instance declarations.
This will only work for terminating programs!

Martin