Re: [Haskell] Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types
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.
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
participants (2)
-
Martin Sulzmann -
MR K P SCHUPKE