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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
