Proposal: Add portable eliminator for Data.Type.Equality
David Feuer
david.feuer at gmail.com
Mon Nov 14 20:21:54 UTC 2016
Most of Data.Type.Equality can be supported by any Haskell
implementation with Rank2Types and TypeOperators, using, for example,
the well-known definition
newtype a :~: b = Equality { subst :: forall f . f a -> f b }
(The parts that can't be supported so are the gcastWith function, the
~~ constraint, and the == type family.)
What's most prominently missing is the ability to *use* equality for
anything beyond castWith without leaning on GHC's equality
constraints.
I propose that we add the eliminator subst as a function:
subst :: a :~: b -> f a -> f b
subst Refl x = x
Note that we already have an introduction rule
Control.Category.id :: a :~: a
David Feuer
More information about the Libraries
mailing list