Proposal: Add portable eliminator for Data.Type.Equality
Oleg Grenrus
oleg.grenrus at iki.fi
Tue Nov 15 09:13:12 UTC 2016
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>
More information about the Libraries
mailing list