Technically yes, we don’t need Coercible—it’s purpose is to bring the magic into the compiler’s domain and offer some automation.
However, I’m explicitly using this approach on top of Coercible, not replacing it. There’s no reason to “get stuck” anywhere that coerce already does the job.
It’s not just some automation. It’s a lot of automation. It automates instances for parametric data types and for newtypes, and it automates the construction of witness terms. It’s also a guarantee of zero cost whilst maintaining type safety.
If you’re not convinced by the examples I gave above, consider Bluefin’s mapHandle (the method of the type class Handle):
mapHandle :: e :> es => h e -> h es
Morally this should be
mapHandle :: e :> es => Dict (OneWayCoercible (h e) (h es))
Does it matter? Won’t everything get “inlined and simplified away”? Maybe, maybe not. Consider runHandleReader:
runHandleReader
:: (e1 :> es, Handle h)
=> h e1
-> (forall (e :: Effects). HandleReader h e -> Eff (e :& es) r)
-> Eff es r
Unless h is statically known (due to specialization, say) runHandleReader can’t inline mapHandle, so will be calling a function at run time: that’s not zero cost. In many cases h will be statically known – great! But in some it won’t. And for those cases we really do need a true one-way equivalent of the Coercible machinery.
I don’t understand this. Coercible is not suitable for use to implement OneWayCoercible. If I have
data T e = MkT (H e) (H' e)
then I get
(Coercible (H e) (H e'),
Coercible (H' e) (H' e')) =>
Coercible T e
But that’s no good. I can’t provide the needed Coercible instances. I only have OneWay (H e) (H e') and OneWay (H' e) (H' e').
Yeah. The conclusion:
newtype Number = MkNumber Int deriving (Show)
newtype Prime = MkPrime Int deriving (Show)
class OneWay a b where
coerce_ :: Coercible a b => a -> b
coerce_ = coerce
instance OneWay Prime Number
instance OneWay [Prime] [Number]
instance OneWay (Maybe Prime) (Maybe Number)
instance OneWay (Either a Prime) (Either a Number)
instance OneWay (Either Prime a) (Either Number a)
instance OneWay (Either Prime Prime) (Either Number Number)
instance OneWay (FlipArrow Prime a) (FlipArrow Number a)
Rather than spending hours automating the impossible and playing find the constraint you can spend 5 minutes writing the exact use case. If you need another particular instance, you add it and move on.
You can amass a big collection of used types in your project (like , Maybe, Identity, Const, etc.) and write Template Haskell to generate all instances for the things you want to coerce (so you don’t have to maintain a separate PotatoToBanana) within these types. But the more you have to fine tune it (e.g PrimeToNumber applies to FlipArrow but for some reason PotatoToBanana doesn’t) the easier copying and pasting becomes to manage the instances.
Note that the MkPrime constructor can’t be exposed from the module in which it is defined, otherwise encapsulation would be broken. Therefore you don’t have Coercible Prime Number outside of the module of definition, and therefore you can’t use coerce_.
I was using ‘some’ pretty neutrally; I’m aware of what instances it generates and that there’s a lot of engineering behind it.
The real issue here is the reliance on an unspecialised typeclass method in performance critical (?) code. Rather than the non-zero-cost but still ~trivial runtime call, I would be more concerned about the barrier to optimisation imposed by its opacity to the simplifier.
Regardless, as the author of bluefin, you’re the one who’s in a position to determine what new coercion primitives the library should utilise to be performant, and which can be exposed without compromising the safety of the interface. One rather direct candidate would be:
coerceHandle :: (Handle h, e :> es) => h e -> h es
coerceHandle h = unsafeCoerce h
The original typeclass method would then be treated like a compile-time “proof”; it can be renamed, hidden in an opaque newtype, given a -Wx-not-for-direct-use warning, whatever.
Coercible is mandatorily symmetric. This could pose some difficulties if you’re trying to implement asymmetric coercions by restricting it from within. It does not when building atop.
You’ve already seen me at it, composing one-way coercions with coerce, or using Coercible constraints as evidence in fsub—it’s just another source of magic primitives.
Regardless, since this discussion has gone on rather too long and code speaks louder than words, I’ve elected to write up a full implementation of how I might actually approach this in the general case: Generalised Coercible · GitHub
Presumably @clinton would also be interested. I’ll conclude by quoting myself, since it seems to bear repeating:
We could obviously do better if the magic and automation were baked into GHC, and perhaps one day it will be. In the mean time, we have to make do with something on this level.
You are right. I have to pop the Coercible outside the signature so the constructors remain in sight. So it works like this:
Test.hs:
module Test (
Number,
makeNumber,
Prime,
makePrime,
coerce_
) where
import Data.Coerce
newtype Number = MkNumber Int deriving (Show)
newtype Prime = MkPrime Int deriving (Show)
makeNumber :: Int -> Number
makeNumber n = MkNumber n
makePrime :: Int -> Maybe Prime
makePrime n = if n == 2 then Just (MkPrime n) else Nothing
class Coercible a b => OneWay a b where
coerce_ :: a -> b
coerce_ = coerce
instance OneWay Prime Number
Main.hs:
import Test
main :: IO ()
main = do
let (Just prime) = makePrime 2
print (coerce_ prime :: Number)
Unfortunately that still leaks:
import Test
import Data.Coerce
data Dict c where
Dict :: c => Dict c
oneWayOfCoercible :: OneWay a b => Dict (Coercible a b)
oneWayOfCoercible = Dict
main :: IO ()
main = do
let number = makeNumber 4
print (case oneWayOfCoercible @Prime @Number of
Dict -> coerce number :: Prime)
I got:
Not in scope: type constructor or class `OneWay'
oneWayOfCoercible :: OneWay a b => Dict (Coercible a b)
It leaks if I export OneWay. So I guess don’t export it and copy paste it / Template Haskell it?
Each module can have its own secret magic OneWay.
Sure, you need to export that from Test.hs.
If I don’t export it and let the magic stay inside then it’s fine?
Sort of, but then I don’t see the point of the type class.
At this point it gives you a single function name for all possible instances you will need as you go (coerce_ vs coerce1, coerce2, coerce3, coerce4…).
And as you add more coerces you need to update the module export list.
You can totally give more unique names (like primeToNumber, primeListToNumberList) to the coerces without the typeclass approach (or with it, too).
So it’s a matter of taste.
You can also make a collection of Internal modules with just one Internal.OneWay typeclass and all constructors exposed between them so you can define all the cross coercion instances you want and hide the OneWay typeclass from the public API.
A (similar) trick for subtyping was used in GUI libraries (wxHaskell).
Thanks for all the replies all! I have read through all of the discussion, and I think I see the main reason why we coercions have to be symmetric, is if we allowed one way coercions say from Prime -> Number, then we can do naughty things like coercing:
Prime -> Int
to
Number -> Int
By requiring coercions to be both ways we avoid this problem. If we want to allow one way coercions, then the type system needs to know things about covariance and contravariance. This may seem relatively trivial in the function case, but it gets complicated, for example, consider a type like:
data Codec a b = ...
instance Profunctor Codec
so the first parameter is contravariant. Again, here Codec Prime a → Codec Number a is invalid.
So actually getting co/contravariance in the type system is non-trivial and I suspect would require extra role annotations along with many other wormy cans.
So I think with my purposes I’m just going to just hide the constructor and just expose explicit coercion functions as needed.
But it still raises one question, the hack for the complete pragma. I would like to be able to do this:
{-# COMPLETE Two, Three, Five :: Number PrimesOnly #-}
but this doesn’t work.
I instead have done this:
view :: Number PrimesOnly -> Maybe Void
view = const Nothing
pattern MatchPrimesOnly :: Void -> Number PrimesOnly
pattern MatchPrimesOnly x <- (view -> Just x)
{-# COMPLETE Two, Three, Five, MatchPrimesOnly #-}
fPrime :: Number PrimesOnly -> Int
fPrime = \case
Two -> 2
Three -> 3
Five -> 5
MatchPrimesOnly x -> Void.absurd x
Which is a bit of a hack but at least does work, and adding an extra pattern that’s never matched whilst annoying isn’t a huge burden. I guess the other approach would be:
pattern TwoP :: Number PrimesOnly
pattern TwoP = Two
pattern ThreeP :: Number PrimesOnly
pattern ThreeP = Three
pattern FiveP :: Number PrimesOnly
pattern FiveP = Five
{-# COMPLETE TwoP, ThreeP, FiveP #-}
which I guess works as as well. Is there anything cleaner than both of these approaches?
@Leary seems to be suggesting that Functor (and by implication Contravariant) are all you need to get the variance correct for one way coercions. That seems plausible to me.
EDIT: In fact, now I come to think of it, it’s the analogue of this idea, which also seems plausible. This approach strikes the best balance that I know of of safety, performance and convenience. Thanks @Leary!