14 Nov
2016
14 Nov
'16
3:21 p.m.
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