[Haskell-cafe] Safe lists with GADT's

[Pepe Iborra]

I am really curious about this style of programming, and find myself  
playing with it from time to time.
The example so far is very nice, but the funniest part is missing.  
That is, defining appendL.

 > appendL :: List a t1 -> List a t2 -> List a t3

This says that the append of a list of length t1 and a list of length  
t2 is a list of whatever length t3 we want. Obviously this is not  
true and will not typecheck.
After some healthy days of reading papers and theses, I've found at  
least three ways of defining it.

First, via existentials:
 > appendL1 :: List a t1 -> List a t2 -> exists t3. List a t3

Second, attaching a proof. Question: what would be the advantage of  
the proof here?
 > data Add a b c where Base :: Add NilT a a ; Step :: Add a b c ->  
Add (ConsT a) b (ConsT c)
 > appendL2 :: List a t1 -> List a t2 -> exists t3. (Add t1 t2 t3,  
List a t3)

Third, via Type Classes.
\begin{code}
class AddList a b c | a b -> c
         where append :: List x a -> List x b -> List x c
instance AddList NilT b b
         where append Nil x = x
instance AddList a b c => AddList (ConsT a) b (ConsT c)
         where append (Cons x l) l' = Cons x (append l l')
\end{code}


Given the three methods, I wouldn't know which one should be  
preferred, and why.
In the first one you pay the burden of programming with existentials.
The second one in addition to that is the least efficient, as  
building the proof surely has a cost. Since we are building it, isn't  
there a way to use it to remove the existential?
Finally, with the third one your compiler will produce error messages  
that will make you swear, apart from possible efficiency losses too.

Thanks for reading, any hints will be appreciated
pepe

On 26/02/2007, at 15:26, David Roundy wrote:

> On Sun, Feb 25, 2007 at 10:40:13PM +0000, Neil Mitchell wrote:
>>> data ConsT a
>>> data NilT
>>>
>>> data List a t where
>>>    Cons :: a -> List a b -> List a (ConsT b)
>>>    Nil  :: List a NilT
> ...
>> Defining safeMap was trivial, but one thing I couldn't figure out was
>> how to write something like fromList:
>>
>> fromList [] = Nil
>> fromList (a:as) = Cons a (fromList as)
>>
>> fromList could obviously be anything such as reading from a file etc,
>> where the input is not known in advance. Are there any techniques for
>> this?
>
> My favorite ways to wrap an existential is with another GADT:
>
> data Existential a where Existential :: a b -> a
>
> (Yes, properly speaking this isn't a GADT, just an existential ADT,  
> but
> it's easier for me to understand this way.)
>
> Then
>
> fromList [] = Existential Nil
> fromList (a:as) = case fromList as of
>                   Existential as' -> Existential (Cons a as')
>
> This is a pretty easy way to deal with the fromList.  You'll now  
> also want
> (which I don't think you mentioned in your example code) a GADT  
> version of
> null, and perhaps other length operators:
>
> data NullT t where
>   IsNull :: NullT NilT
>   NotNull :: NullT (ConsT t)
>
> nullL :: List a t -> NullT t
>
> so you can now actually use your head function on a dynamically  
> generated
> list, by running something like (e.g. in a monad)
>
>    do cs <- readFile "foo"
>       Existential cs' <- return $ fromList cs
>       -- note: we'll pattern-match fail on non-empty list here, which
>       -- may not gain much, we'd use case statements in reality, or  
> we'd
>       -- catch failure within the monad, which is also safe-- 
> provided you
>       -- catch them, which the language doesn't force you to do!  
> (Or if
>       -- we're in a pure monad like Maybe.)
>       NotNull <- nullL cs'
>       let c = headL cs'
>           t = tailL cs'
>           -- Now to illustrate the power of the GADT, a line that  
> will fail
>           -- at compile time:
>           t' = tailL t
>       return c
>
> -- 
> David Roundy
> http://www.darcs.net
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe