
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe