Proposal: Add gcoerceWith to Data.Type.Coercion

In Data.Type.Equality, we have both castWith :: (a :~: b) -> a -> b and gcastWith :: (a :~: b) -> (a ~ b => r) -> r But in Data.Type.Coercion we only have coerceWith :: Coercion a b -> a -> b It seems to me that for the sake of consistency, we should add gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r gcoerceWith Coercion a = a David Feuer

No objection here. +1
-Edward
On Fri, Jul 22, 2016 at 1:18 AM, David Feuer
In Data.Type.Equality, we have both
castWith :: (a :~: b) -> a -> b
and
gcastWith :: (a :~: b) -> (a ~ b => r) -> r
But in Data.Type.Coercion we only have
coerceWith :: Coercion a b -> a -> b
It seems to me that for the sake of consistency, we should add
gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r gcoerceWith Coercion a = a
David Feuer _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

I have wanted this exact function before. +1
On Fri, 22 Jul 2016, 12:27 a.m. Edward Kmett,
No objection here. +1
-Edward
On Fri, Jul 22, 2016 at 1:18 AM, David Feuer
wrote: In Data.Type.Equality, we have both
castWith :: (a :~: b) -> a -> b
and
gcastWith :: (a :~: b) -> (a ~ b => r) -> r
But in Data.Type.Coercion we only have
coerceWith :: Coercion a b -> a -> b
It seems to me that for the sake of consistency, we should add
gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r gcoerceWith Coercion a = a
David Feuer _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

+1 I'm not sure why that was left out.
On Jul 22, 2016, at 4:58 AM, Oliver Charles
wrote: I have wanted this exact function before. +1
On Fri, 22 Jul 2016, 12:27 a.m. Edward Kmett,
mailto:ekmett@gmail.com> wrote: No objection here. +1 -Edward
On Fri, Jul 22, 2016 at 1:18 AM, David Feuer
mailto:david.feuer@gmail.com> wrote: In Data.Type.Equality, we have both castWith :: (a :~: b) -> a -> b
and
gcastWith :: (a :~: b) -> (a ~ b => r) -> r
But in Data.Type.Coercion we only have
coerceWith :: Coercion a b -> a -> b
It seems to me that for the sake of consistency, we should add
gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r gcoerceWith Coercion a = a
David Feuer _______________________________________________ Libraries mailing list Libraries@haskell.org mailto:Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________ Libraries mailing list Libraries@haskell.org mailto:Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
participants (4)
-
David Feuer
-
Edward Kmett
-
Oliver Charles
-
Richard Eisenberg