Proposal: Add portable eliminator for Data.Type.Equality

[David Feuer]

On Nov 15, 2016 12:24 AM, "wren romano" <winterkoninkje at gmail.com> wrote:
> > 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.

Yes, we will, but those can be written using `subst` and one or more
auxiliary types without additional "primitive" eliminators (see below).

> 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)

We can write

newtype Flip f x y = Flip { unFlip :: f y x }

subst2 :: a :~: b -> f a x -> f b x
subst2 eq = unFlip . subst eq . Flip

The subst2 function will work on the left side of Either.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20161115/c3cd1f23/attachment-0001.html>