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