[Haskell-cafe] Safe lists with GADT's

[David Roundy]

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