Proposal: Add portable eliminator for Data.Type.Equality

[Oleg Grenrus]

I’m -1

λ Prelude Data.Type.Equality > :t (`gcastWith` x) :: b :~: Bool -> Either b Int
(`gcastWith` x) :: b :~: Bool -> Either b Int
  :: b :~: Bool -> Either b Int

gcastWith :: (a :~: b) -> (a ~ b => r) -> r

That type “unifies" with subst :: (a :~: b) -> c a -> c b (and is more “general”), if stare at it for long enough.

- Oleg

P.S. FWIW there is PR [1] to `eq` [2], if you want to play with Leibniz equality definition.

- [1]: http://hackage.haskell.org/package/eq
- [2]: https://github.com/ekmett/eq/pull/9/files

> On 15 Nov 2016, at 07:37, David Feuer <david.feuer at gmail.com> wrote:
> 
> 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.
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20161115/19963a53/attachment.sig>