David Roundy droundy at darcs.net
Mon Feb 26 09:26:12 EST 2007

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