[Haskell-cafe] Regular Expressions without GADTs

[Ross Paterson]

On Wed, Oct 19, 2005 at 03:17:41PM +0100, Conor McBride wrote:
> It's nice that the syntax of regular expressions survives, but it
> has been somewhat spun in favour of the functionality required in
> the example.

I'm not sure about that either -- the existential coding supports
elimination too, if the result type is functorial (again specializing
the general scheme):

caseRegExp
	:: Functor r
	=> r Empty
	-> r ()
	-> ((tok -> Bool) -> r tok)
	-> (forall a b. RegExp tok a -> RegExp tok b -> r (Either a b))
	-> (forall a b. RegExp tok a -> RegExp tok b -> r (a, b))
	-> (forall a. RegExp tok a -> r [a])
	-> RegExp tok v -> r v
caseRegExp fZero fOne fCheck fPlus fMult fStar x = case x of
	Zero		-> fmap (const bot)	fZero
	One v		-> fmap (const v)	fOne
	Check k p	-> fmap k		(fCheck p)
	Plus r1 r2	-> fmap (either id id)	(fPlus r1 r2)
	Mult r1 r2	-> fmap (uncurry id)	(fMult r1 r2)
	Star k r	-> fmap k		(fStar r)
  where bot = error "can't happen"

Not that this is comfortable to use, but it does show that existentials
are as expressive, assuming the functor: they can't do RegExp t a -> a -> a.

> I would say that the availability of 'this workaround for this example, 
> that workaround for that example', is evidence in *favour* of adopting 
> the general tools which are designed to support many examples. If a 
> job's worth doing, it's worth doing well. Is there a *uniform* 
> workaround which delivers all the GADT functionality cheaply and 
> cleanly? Kind of subjective, I suppose, but I haven't seen anything 
> cheap enough for me.

It seems the existential coding is uniform, if everything is covariant.