How to expose coercions only one way?

Learn
1

Consider this somewhat silly datatype:

type data AllowPrimesOnly = PrimesOnly | AllNumbers

data Number (allowPrimesOnly :: AllowPrimesOnly) where
  One :: Number AllNumbers
  Two :: Number allowPrimesOnly
  Three :: Number allowPrimesOnly
  Four :: Number AllNumbers
  Five :: Number allowPrimesOnly

With this definition, I can then define:

f :: Number allowPrimesOnly -> Int
f = \case
  One -> 1
  Two -> 2
  Three -> 3
  Four -> 4
  Five -> 5

fPrime :: Number PrimesOnly -> Int
fPrime = \case
  Two -> 2
  Three -> 3
  Five -> 5

quite happily, and GHC will give warnings (or no warnings) appropriately.

Note in particular with f, it works with both types. Perhaps there’s some inefficiencies applying f to a Number PrimeOnly because it’s checking branches that never exist but it still works.

But then when I try to do:

g :: Number PrimesOnly -> Number AllNumbers
g = coerce

I get a problem. I can’t coerce between different Number types, because the role of allowPrimesOnly is nominal as Number is a GADT.

Now lets say instead I define Number like this:

data Number (allowPrimesOnly :: AllowPrimesOnly) = One | Two | Three | Four | Five

now:

g :: Number PrimesOnly -> Number AllNumbers
g = coerce

does work. But we’re now getting warnings for fPrime. We can fix that though, with a bit of a hack:

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

The MatchPrimesOnly pattern is a bit of a hack to force the COMPLETE pragma to only apply to Number PrimesOnly.

So far so good. We’ve got to add a bit of a hack to get the compiler to not warn when we’re only pattern matching against the primes (as just using a {-# COMPLETE Two, Three, Five #-} would allow incomplete matches against Number AllNumbers) but we’ve got a problem now:

g2 :: Number AllNumbers -> Number PrimesOnly
g2 = coerce

works. And it shouldn’t. Note we want the following:

thisShouldCompile :: Number PrimesOnly -> Number AllNumbers
thisShouldCompile = coerce

thisShouldCompileAsWell :: [Number PrimesOnly] -> [Number AllNumbers]
thisShouldCompileAsWell = coerce

butThisShouldFailToCompile :: Number AllNumbers -> Number PrimesOnly
butThisShouldFailToCompile = coerce

I don’t just want to write:

doCoerce :: Number PrimesOnly -> Number AllNumbers
doCoerce = coerce

and expose it as a function, because then I’ll have to also write,

doCoerceHigher :: f (Number PrimesOnly) -> f (Number AllNumbers)
doCoerceHigher = coerce

Because I don’t even know how to write this, and even this doesn’t even cover all the possibilities where coerce can be used.

Anyway to achieve what I’m trying to achieve here?

2

I want this too but it doesn’t seem possible (yet). See also One way Coercible

2 Likes
3

Depend on witch and implement From as needed?

The default impl uses coerce already so you can anyclass derive it in-module where you have ctors in scope inherently.

1 Like
4 
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

import Data.Coerce

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 (f1(Prime)) (f1(Number))
instance OneWay (f2(f1(Prime))) (f2(f1(Number)))
instance OneWay (f3(f2(f1(Prime)))) (f3(f2(f1(Number))))
instance OneWay (f4(f3(f2(f1(Prime))))) (f4(f3(f2(f1(Number)))))
instance OneWay (f5(f4(f3(f2(f1(Prime)))))) (f5(f4(f3(f2(f1(Number))))))
instance OneWay (f6(f5(f4(f3(f2(f1(Prime))))))) (f6(f5(f4(f3(f2(f1(Number)))))))
instance OneWay (f7(f6(f5(f4(f3(f2(f1(Prime)))))))) (f7(f6(f5(f4(f3(f2(f1(Number))))))))
-- you don't really need more :)

main = do
  let prime = MkPrime 2
  let number = MkNumber 4
  print $ (coerce_ prime :: Number)
  print $ (coerce_ [prime, prime, prime] :: [Number])
  print $ (coerce_ (Just prime) :: Maybe Number)
  -- print $ (coerce_ number :: Prime) -- error

BEHOLD!
ONE WAY COERCION!

1 Like
5

[cries in Either Prime a], as the kids say.

3 Likes
6 
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

import Data.Coerce

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 a b => OneWay (f a) (f b)
instance OneWay (f Prime a) (f Number a)
instance {-# INCOHERENT #-} OneWay a b => OneWay (f Prime a) (f Number b)

main = do
  let prime = MkPrime 2
  let number = MkNumber 4
  print $ (coerce_ prime :: Number)
  print $ (coerce_ [prime, prime, prime] :: [Number])
  print $ (coerce_ (Just prime) :: Maybe Number)
  let r1 = Right prime :: Either Int Prime
  print $ (coerce_ r1 :: Either Int Number)
  let l1 = Left prime :: Either Prime Int
  print $ (coerce_ l1 :: Either Number Int)
  let r2 = Right prime :: Either Prime Prime
  print $ (coerce_ r2 :: Either Number Number)

BEHOLD!

1 Like
7

:smiley: Better!

To handle further complications such as Either (Either Prime Int) Int and so on, I’d suggest the following refinement:

instance OneWay Prime Number
instance OneWay a a
instance OneWay a b => OneWay (f a) (f b)
instance {-# INCOHERENT #-} (OneWay a1 b1, OneWay a2 b2) => OneWay (f a1 a2) (f b1 b2)
instance {-# INCOHERENT #-} (OneWay a1 b1, OneWay a2 b2, OneWay a3 b3) => OneWay (f a1 a2 a3) (f b1 b2 b3)
-- ... repeat until bored
1 Like
8

You appear to want subtyping, wherein primes are a subtype of a broader number type. This can be embedded in Haskell via higher rank polymorphism.

type data Sub = S Sub

type Prime :: Sub -> Sub
type Any   :: Sub -> Sub
type Prime s = s
type Any   s = S s

data Number (n :: Sub) where
  One   :: Number (Any   s)
  Two   :: Number (Prime s)
  Three :: Number (Prime s)
  Four  :: Number (Any   s)
  Five  :: Number (Prime s)

type AnyNumber   = forall s. Number (Any   s)
type PrimeNumber = forall s. Number (Prime s)

As a subtype, a PrimeNumber can be used where AnyNumber is expected, giving you your coercion for free:

g :: PrimeNumber -> AnyNumber
g n = n

The other direction is a type error, as is e.g. Four :: PrimeNumber.

Sadly, GHC has trouble realising completeness; the below warns.

fPrime :: PrimeNumber -> Int
fPrime = \case
  Two   -> 2
  Three -> 3
  Five  -> 5

Worse, this pragma doesn’t fix the issue:

{-# COMPLETE Two, Three, Five :: PrimeNumber #-}

It seems we need to guard the polymorphism behind a newtype and set up synonyms:

newtype PrimeNumberC = Complete PrimeNumber

{-# COMPLETE TwoP, ThreeP, FiveP #-}
pattern TwoP, ThreeP, FiveP :: PrimeNumberC
pattern TwoP   = Complete Two
pattern ThreeP = Complete Three
pattern FiveP  = Complete Five

fPrime :: PrimeNumberC -> Int
fPrime = \case
  TwoP   -> 2
  ThreeP -> 3
  FiveP  -> 5

Finally, as a bonus, we obtain the type of monotonically decreasing mappings with respect to the subtyping relation:

type MonoMap :: (Sub -> Type) -> Type
type MonoMap n = forall s. n s -> n s

In this case MonoMap Number allows mappings between Numbers of the same primality, or from non-primes to primes:

h, h' :: MonoMap Number
h  One = One
h' One = Two

but not the reverse (type error):

h'' :: MonoMap Number
h'' Two = One

I developed the technique in this gist: Parametrickery: Subtyping & Monotonicity ¡ GitHub

I was inspired by a MonoMaybe type found in the bowels of some (IIRC @lexi.lambda) library by someone on #haskell (IIRC ncf), though in that case the monotonic mapping was the goal, not the bonus.

6 Likes
9

I’ll try this a different way:

  • module Numbers where

data Number
  = One
  | Two
  | Three
  | Four
  | Five

  •  module Primes where
 import Numbers hiding (One, Four)

 type Prime = Number

  •  module Primechk where
 import Primes

 failing = One :: Prime

Now all going well:

# ghci Primechk.hs
GHCi, version 9.8.2: https://www.haskell.org/ghc/  :? for help
[1 of 3] Compiling Numbers          ( Numbers.hs, interpreted )
[2 of 3] Compiling Primes           ( Primes.hs, interpreted )
[3 of 3] Compiling Primechk         ( Primechk.hs, interpreted )

Primechk.hs:4:14: error: [GHC-88464]
    Data constructor not in scope: One :: Prime
  |
4 |    failing = One :: Prime
  |              ^^^
Failed, two modules loaded.
ghci>

…that is correct. But it does require an extra module (Primes here) for this to work.

10

Unfortunately this can’t possibly be right, due to the lack of constraints on f. For example:

newtype a `FlipArrow` b = MkFlipArrow (b -> a)

flipApply :: a `FlipArrow` b -> b -> a
flipApply (MkFlipArrow f) = f

...

  -- Prints `MkPrime 4`
  print $ (coerce_ (MkFlipArrow (id :: Prime -> Prime))
             :: Prime `FlipArrow` Number)
          `flipApply` MkNumber 4

I don’t think you need the funny recursive structure of S, do you? This seems to be fine:

{-# LANGUAGE TypeData #-}

type data Sub = S

type Prime :: Sub -> Sub
type Any   :: Sub -> Sub
type Prime s = s
type Any   s = S

data Number (n :: Sub) where
  One   :: Number (Any   s)
  Two   :: Number (Prime s)
  Three :: Number (Prime s)
  Four  :: Number (Any   s)
  Five  :: Number (Prime s)

type AnyNumber   = forall s. Number (Any   s)
type PrimeNumber = forall s. Number (Prime s)

g :: PrimeNumber -> AnyNumber
g n = n

In any case, I don’t think this trick, neat as it is, is general enough. For example, you’ll have trouble if you put these numbers inside containers:

-- test28.hs:23:6: error: [GHC-91510]
--     • Illegal polymorphic type: forall (s :: Sub). Number (Prime s)
--     • In the expansion of type synonym ‘PrimeNumber’
--       In the type signature:
--         h :: PrimeNumber -> (PrimeNumber, PrimeNumber)
--     Suggested fix:
--       Perhaps you intended to use the ‘ImpredicativeTypes’ extension
--       You may enable this language extension in GHCi with:
--         :set -XImpredicativeTypes
--    |
-- 23 | h :: PrimeNumber -> (PrimeNumber, PrimeNumber)
--    |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
h :: PrimeNumber -> (PrimeNumber, PrimeNumber)
h x = (x, x)

Even with ImpredicativeTypes it seems like it will be easy to get snagged on other desirable features, such as one-way coercing between PrimeNumber and Identity AnyNumber. The one-way machinery really will need to be aware of newtypes in general, having specific subtypes is not enough.

2 Likes
11

Yes, the recursive parameter to S is redundant in this case. Sub is general purpose—it supports any finite total ordering.

I’m also presuming a willingness to rely upon ImpredicativeTypes (which is fair in modern GHC) or to evade such issues with newtype wrappers.

I confess I didn’t read the latter portion of the OP that closely, but I had thought that e.g. (\x -> x) :: [PrimeNumber] -> [AnyNumber] would just work, and that less direct coercions could be constructed by manual composition:

weaken :: PrimeNumber -> AnyNumber
weaken = \p -> p

co :: PrimeNumber -> Identity AnyNumber
co = coerce . weaken

Sadly it seems I was wrong about the former, but sadness comes hand in hand with unsafe magic:

type Repr :: (k1 -> k2) -> Constraint
type Repr f = forall a b. Coercible a b => Coercible (f a) (f b)

fsub :: (Functor f, Repr f) => f PrimeNumber -> f AnyNumber
fsub fp = unsafeCoerce fp
1 Like
12

Perhaps I’m telling you something you already know (I didn’t follow quite what you were saying) but this defeats the purpose since co is not a coercion. It is a function which may not be erased.

13

I don’t think the distinction matters here; co is practically guaranteed to be erased in simplification.

14

Doesn’t it matter very much, and indeed is the whole point of the Coercible mechanism? Occurrences of co p may very well be rewritten to p, but what about (map . contramap . map . map . contramap) co p. Is that practically guaranteed to be rewritten to p?

15

co will be erased, just like coerce. fmap co will not be erased, just like fmap coerce. So yes, the distinction really doesn’t matter for co.

For the more general coercions you appear to be envisioning, you’d need to build them from magical primitives like fsub above and fcontrasub :: (Contravariant f, Repr f) => f AnyNumber -> f PrimeNumber, perhaps using newtypes to rearrange type parameters.

It’s not ergonomic or universal, but them’s the breaks.

16

It really does matter, because the point is you don’t use fmap coerce :: C a -> C b, you just use coerce :: C a -> C b!

17

Please note the emphasis on for co.

My second paragraph also addressed the equivalent of "just us[ing] coerce :: [...]" with fsub/fcontrasub.

18

Well, I still don’t understand, because fsub and fcontrasub are not coercions either, they’re functions, and thus subject to the same non-erasure. Perhaps you could give an example of how you envisage this working, say coercing from

(a -> b) -> (b -> a)

to

(b -> a) -> (a -> b)

using OneWay a b. Of course one possibility is

\f k a -> oneWay (f (\a' -> oneWay (k (oneWay a'))) (oneWay a))

but that’s not a coercion: it’s not zero-cost. So what’s the zero-cost way?

19

fsub :: C PrimeNumber -> C AnyNumber is zero-cost; coerce . fcontrasub . coerce . fsub . coerce is zero-cost; et cetera. They’re not literal coercions, but their expected runtime cost is equally trivial.

Your lambda is probably the same. If oneWay is either coerce or equivalent to id in a way visible to the simplifier, then conj f = oneWay . f . oneWay will reduce to conj f = f. Similarly for conj2 f = conj . f . conj, where conj2 equals what you wrote.

20

Let’s have a look at it from a different angle. If what you are saying is true about one-way coercions then it’s true of two-way coercions (because they’re just a pair of one-way coercions). So it seems your approach obviates the need for Coercible machinery in GHC at all. Is that right? If so, how can that be?

Perhaps your point is that you need “enough” magical primitives like fsub and fcontrasub, and if there’s a corner where you seem to get stuck, it’s just because you haven’t written enough magical primitives yet. Well, I would guess you’d “get stuck” on basically every newtype, wouldn’t you? Wouldn’t you need a “magical primitive” for every newtype? If that’s what you’re saying then I agree it would technically work.