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