Re: Proposal: Add portable eliminator for Data.Type.Equality

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

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
wrote: On Nov 15, 2016 12:24 AM, "wren romano"
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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
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
wrote: On Nov 15, 2016 12:24 AM, "wren romano"
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
participants (2)
-
David Feuer
-
Oleg Grenrus