Proposal: Add portable eliminator for Data.Type.Equality
wren romano
winterkoninkje at gmail.com
Tue Nov 15 05:24:42 UTC 2016
On Mon, Nov 14, 2016 at 12:21 PM, David Feuer <david.feuer at gmail.com> wrote:
> 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
More information about the Libraries
mailing list