Hi folks
There is nothing ingenious with this solution --- I basically translated
Oleg's and Conor's code.
Neither Oleg nor Bruno translated my code; they threw away my
structurally recursive on-the-fly automaton and wrote combinator parsers
instead. That's why there's no existential, etc. The suggestion that
removing the GADT simplifies the code would be better substantiated if
like was compared with like. By the way, the combinator parsers, as
presented, don't quite work: try
asMayBe $ parse (Star One) "I really must get to the bottom of this..."
with Oleg's code, or the analogous (star one) with Bruno's.
But it's almost as easy a mistake to fix (I hope) as it is to make, so
the point that the GADT isn't strictly necessary does stand. I wouldn't
swear my code's correct either, but I don't think it loops on finite input.
Oleg simulates GADTs with Ye Olde Type Class Trick, getting around the
fact that type classes aren't closed by adding each necessary piece of
functionality to the methods. By contrast, Bruno goes straight for the
Church encoding, as conveniently packaged by type classes: even if you
can't write down the (morally) *initial* RegExp algebra, you can write
down what RegExp algebras are in general. These two approaches aren't
mutually exclusive: you can use Bruno's algebras to capture the
canonical functionality which should be supported for all types in
Oleg's class. Then you're pretty much writing down that a GADT is an
inductive relation, which perhaps you had guessed already...
Where we came in, if you recall, was the use of a datatype to define
regular expressions. I used a GADT to equip this type with some useful
semantic information (namely a type of parsed objects), and I wrote a
program (divide) which exploited this representation to compute the
regexp the tail of the input must match from the regexp the whole input
must match. This may be a bit of a weird way to write a parser, but it's
a useful sort of thing to be able to do. There are plenty of other
examples of 'auxiliary' types computed from types to which they relate
in some interesting way, the Zipper being the a favourite. It's useful
to have a syntax (Generic Haskell, GADTs etc) which makes that look as
straightforward and concrete as possible.
I'm sure the program I actually wrote can be expressed with the type
class trick, just by cutting up my functions and pasting the bits into
individual instances; the use of the existential is still available. I
don't immediately see how to code this up in Bruno's style, but that
doesn't mean it can't be done. Still, it might be worth comparing like
with like. I suspect that once you start producing values with the
relevant properties (as I do) rather than just consuming them (as Oleg
and Bruno do), the GADT method might work out a little neater.
And that's the point: not only does the GADT have all the disadvantages
of a closed datatype, it has all the advantages too! It's easy to write
new functions which both consume and produce data, without having to go
back and change the definition. I didn't have to define Division or
divide in order to say what a regular expression was. If I remember
rightly, regular languages are closed under a whole bunch of useful
stuff (intersection, complementation, ...) so someone who can remember
better than me might implement the corresponding algorithms together
with their related operations; they don't need to change the definition
of RegExp to do that. Might we actually decide semantic subtyping
(yielding a coercion) that way?
So what's the point? GADTs are a very convenient way to provide data
which describe types. Their encoding via type classes, or
whatever, may be possible, but this encoding is not necessarily as
convenient as the GADT. Whether or not the various encodings of GADTs
deliver more convenience in this example is not clear, because the
programs do not correspond. Moreover, once you have to start messing
about with equality constraints, the coding to eliminate GADTs becomes a
lot hairier. I implemented it back in '95 (when all these things had
different names) and I was very glad not to have to do it by hand any more.
But your mileage may vary
Conor
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
