Proposal: Add portable eliminator for Data.Type.Equality

[David Feuer]

Yes, gcastWith is certainly "more general" than subst. Exporting subst
from Data.Type.Equality would allow programmers to write code that
doesn't *care* how :~: is represented.

On Tue, Nov 15, 2016 at 4:13 AM, Oleg Grenrus <oleg.grenrus at iki.fi> wrote:
> 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
>