Proposal: Add portable eliminator for Data.Type.Equality
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
Further support for my proposal: we already have the analogous partial version
Data.Typeable.gcast :: forall a b c. (Typeable a, Typeable b) => c a
-> Maybe (c b)
On Mon, Nov 14, 2016 at 3:21 PM, David Feuer
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
On Mon, Nov 14, 2016 at 12:21 PM, David Feuer
I propose that we add the eliminator subst as a function:
subst :: a :~: b -> f a -> f b subst Refl x = x
I'm all for adding this function, but do note that the type is suboptimal since GHC lacks general functions (and higher-order pattern matching) at the type level. Which means we'll actually end up wanting a family of different "subst" functions to cover all the (relevant) cases the definition above would cover in a language like Agda, Coq, etc. E.g., Prelude> let x :: Either Bool Int; x = Right 42 Prelude> :t (`subst` x) (`subst` x) :: Int :~: b -> Either Bool b When I might've really wanted/meant (Bool :~: b -> Either b Int) -- Live well, ~wren
participants (2)
-
David Feuer -
wren romano