[Haskell-cafe] Regular Expressions without GADTs
ross at soi.city.ac.uk
Wed Oct 19 16:02:32 EDT 2005
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):
:: 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.
More information about the Haskell-Cafe