[Haskell-cafe] Safe lists with GADT's

David Roundy droundy at darcs.net
Mon Feb 26 11:35:25 EST 2007


On Mon, Feb 26, 2007 at 04:35:06PM +0100, Pepe Iborra wrote:
> First, via existentials:
> > appendL1 :: List a t1 -> List a t2 -> exists t3. List a t3

It seems like this problem is begging for the new indexed types (for which
I never remember the right syntax).

type AddListTs :: * -> * -> *
AddListTs NilT NilT = NilT
AddListTs NilT t = t
AddListTs (ConsT t) t' = AddListTs t (ConsT t')

then

appendLi :: List a t1 -> List a t2 -> List a (AddListTs t1 t2)

I'd be interested if Manuel had an idea whether this would work right.  I
think it can be made equivalent to the FD approach, but doesn't require
that you define a "stupid" class, and is far, far prettier.
-- 
David Roundy
Department of Physics
Oregon State University


More information about the Haskell-Cafe mailing list