Proposal: Add portable eliminator for Data.Type.Equality
David Feuer
david.feuer at gmail.com
Tue Nov 15 05:37:17 UTC 2016
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>
More information about the Libraries
mailing list