GADTs have the problem that they're not extensible, but type classes are! Imagine if we add regular hedges. So, I think Oleg has a point here. Oleg's solution may look rather cryptic. But if we recall that type class instances describe proof systems, then Oleg's solutions starts looking quite elegant. Note that the GADTs serve the same purpose, i.e. encoding proof rules. An interesting question is whether there's something GADTs can do "better" than type classes and vice versa. Here's an example, many regexp algorithms can be formulated co-inductively. We'll have trouble to encode these algorithms with "standard" type classes, unless we consider some type class extensions (if this sounds interesting check out the "co-induction type class" paper on my home-page). I don't think this will cause trouble for GADTs. Martin Ralf Hinze writes:

...

The code seems a bit simpler, too.

Do you really think so? To me replacing a GADT by class and instance declarations seems the wrong way round. We should not forget that the DT in GADT stands for `data type'. One could certainly argue that the gist of functional programming is to define a collection of data types and functions that operate on these types. The fact that with GADTs constructors can have more general types just allows us to use the functional design pattern more often (freeing us from the need or temptation to resort to type class hackery with multiple parameter type classes, undecidable instances, functional dependencies etc).

Cheers, Ralf _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On 10/19/05, oleg@pobox.com wrote:

I never argued about convenience of GADTs. They can be quite handy when dealing with existentials: GADT embody a safe cast and so spare us form writing the boring casting code ourselves. And perhaps this is the only compelling case for GADTs.

Speaking about casts, I was playing with using GADTs to create a non-extensible version of Data.Typeable and Data.Dynamic. I wonder if it's possible to write such a thing without GADTs (and unsafeCoerce, which is used in Data.Dynamic, IIRC). BTW, being non-extensible has some benefits, for example, I feel a bit uneasy when I use full blown Dynamics in Haskell (not that I do it that often). See code in the attachment. It has some functions which I didn't find in Data.Dynamics, actually one function: withDyn :: Dyn -> (forall a. Typed a => a -> b) -> b Best regards Tomasz

On Wed, Oct 26, 2005 at 01:37:29PM +0200, Tomasz Zielonka wrote:

On 10/19/05, oleg@pobox.com wrote:

...

I never argued about convenience of GADTs. They can be quite handy when dealing with existentials: GADT embody a safe cast and so spare us form writing the boring casting code ourselves. And perhaps this is the only compelling case for GADTs.

Speaking about casts, I was playing with using GADTs to create a non-extensible version of Data.Typeable and Data.Dynamic. I wonder if it's possible to write such a thing without GADTs (and unsafeCoerce, which is used in Data.Dynamic, IIRC).

BTW, being non-extensible has some benefits, for example, I feel a bit uneasy when I use full blown Dynamics in Haskell (not that I do it that often).

See code in the attachment. It has some functions which I didn't find in Data.Dynamics, actually one function: withDyn :: Dyn -> (forall a. Typed a => a -> b) -> b

perhaps something like class Typeable a => MyTypeable a newtype MyDynamic = MyDynamic Dynamic instnance MyTypeable Int instance MyTypeable Foo (and add whatever appropriate access methods you like) and then not export the MyTypeable class so new instances could not be declared. John -- John Meacham - ⑆repetae.net⑆john⑈

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

On Tue, Oct 18, 2005 at 05:51:13PM +0100, Conor McBride wrote: | 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. Here's a version in H98 + existentials. I'm not claiming it proves anything.

module RegExp where

import Control.Monad

data RegExp tok a = Zero | One a | Check (tok -> a) (tok -> Bool) | Plus (RegExp tok a) (RegExp tok a) | forall b. Mult (RegExp tok (b -> a)) (RegExp tok b) | forall e. Star ([e] -> a) (RegExp tok e)

I could just use Prod (One f) instead of fmap f, but the functor instance is mechanical:

instance Functor (RegExp tok) where fmap f Zero = Zero fmap f (One v) = One (f v) fmap f (Check k p) = Check (f.k) p fmap f (Plus r1 r2) = Plus (fmap f r1) (fmap f r2) fmap f (Mult r1 r2) = Mult (fmap (f.) r1) r2 fmap f (Star k r) = Star (f.k) r

Constructors

one :: RegExp tok () one = One ()

check :: (tok -> Bool) -> RegExp tok tok check = Check id

plus :: RegExp tok a -> RegExp tok b -> RegExp tok (Either a b) plus r1 r2 = Plus (fmap Left r1) (fmap Right r2)

mult :: RegExp tok a -> RegExp tok b -> RegExp tok (a,b) mult r1 r2 = Mult (fmap (,) r1) r2

star :: RegExp tok a -> RegExp tok [a] star = Star id

Parsing

parse :: RegExp tok a -> [tok] -> Maybe a parse r [] = empty r parse r (t : ts) = parse (divide t r) ts

empty :: RegExp tok a -> Maybe a empty Zero = mzero empty (One v) = return v empty (Check _ _) = mzero empty (Plus r1 r2) = empty r1 `mplus` empty r2 empty (Mult r1 r2) = empty r1 `ap` empty r2 empty (Star k _) = return (k [])

divide :: tok -> RegExp tok a -> RegExp tok a divide t Zero = Zero divide t (One v) = Zero divide t (Check k p) | p t = One (k t) | otherwise = Zero divide t (Plus r1 r2) = Plus (divide t r1) (divide t r2) divide t (Mult r1 r2) = case empty r1 of Nothing -> Mult (divide t r1) r2 Just f -> Plus (Mult (divide t r1) r2) (fmap f (divide t r2)) divide t (Star k r) = Mult (fmap k_cons (divide t r)) (Star id r) where k_cons x xs = k (x:xs)