Opened 2 years ago

Last modified 2 years ago

#14362 new feature request

Allow: Coercing (a:~:b) to (b:~:a)

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: roles Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Is there *any* sensible way to enable coercing (:~:) swapping its arguments

coerce :: a:~:b -> b:~:a

Same for Coercion

coerce :: Coercion a b -> Coercion b a

Thanks!

Change History (11)

comment:1 Changed 2 years ago by Iceland_jack

Where the compiler knows constraints ((~) and Coercible) are symmetric

comment:2 Changed 2 years ago by simonpj

Reminder

data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

data a :~: b where 
  Refl :: a :~: a

So you want to be able to prove

[W] (a :~: b)      ~R#  (b :~: a)
[W] Coercible a b  ~R#  Coercible b a

Once could imagine special cases in the compiler, these are really perfectly ordinary data type declarations. What makes these representational type equalities true?

Well, representationally speaking

  • Refl :: (a ~# b) => a :~: b has no represented value arguments. I suppose that for such types it's true that (a :~: b) ~R# (c :~: d) for any a, b, c, d. Is that right?

Let's think about that first; I expect that once we figure this one out, Coercible will follow.

Richard?

comment:3 Changed 2 years ago by Iceland_jack

Is it not ultimately about implication of constraints (quantified constraints)

-- Witness Constraint
data Dict :: Constraint -> Type where
  Dict :: ctx => Dict ctx

instance (ctx           => ctx')            => Coercible (Dict ctx)     (Dict ctx')
instance (Coercible a b => Coercible a' b') => Coercible (Coercion a b) (Coercion a' b')
instance ((a ~ b)       => (a' ~ b'))       => Coercible (a:~:b)        (a':~:b')

In the case of symmetry,

  • To coerce :: a:~:b -> b:~:a we need to show
    • a ~ b => b ~ a
  • To coerce :: Coercion a b -> Coercion b a we need to show
    • Coercible a b => Coercible b a

If we think of the class of data types witnessing an Underlying constraint

type family
  Underlying (dataty :: Type) :: Constraint where
  Underlying (Dict ctx)     = ctx
  Underlying (Coercion a b) = Coercible a b
  Underlying (a :~:  b)     = a ~  b
  Underlying (a :~~: b)     = a ~~ b

we can could write these in a more general form:

instance (Underlying thing => Underlying thing') => Coercible thing thing'
Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:4 Changed 2 years ago by Iceland_jack

A user-defined type with "no represented value arguments" will automatically generate an Underlying type instance

type Cat obj = obj -> obj -> Type

data LessThanEq :: Cat Nat where
  LessThanEq :: a <= b => LessThanEq a b

data GreaterThanEq :: Cat Nat where
  GreaterThanEq :: a >= b => GreaterThanEq a b

type instance Underlying (LessThanEq    a b) = a <= b
type instance Underlying (GreaterThanEq a b) = a >= b

In the magic future, we can coerce

-- ((a <= b) => (a <= 10+b)) => Coercible (LessThanEq a b) (LessThanEq a (10+b))
coerce :: LessThanEq a b -> LessThanEq a (10 + b)

-- ((a <= b) => (b >= a)) => Coercible (LessThanEq a b) (GreaterThanEq b a)
coerce :: LessThanEq a b -> GreaterThanEq b a
Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:5 Changed 2 years ago by simonpj

Is it not ultimately about implication of constraints?

I don't thuink so. Take :~:. Could I write this function?

convert :: (a :~: b) -> (b :~: a)

Sure! Thus

convert Refl = Refl

Plus, the two represntationns are the same. So yes, they should be coercible. No quantification stuff. I think.

comment:6 Changed 2 years ago by Iceland_jack

But what is the most general type of convert Refl = Refl?

We cannot write

-- Could not deduce: a' ~ b'
-- from the context: a  ~ b
convert :: (a :~: b) -> (a' :~: b')
convert Refl = Refl

note how type checking this depends on the ‘underlying constraint’ of (:~:): (~).

We must be able to deduce a' ~ b' from the given context a ~ b, which is this?

convert :: ((a~b) => (a'~b')) => (a :~: b) -> (a' :~: b')
convert Refl = Refl

so I would expect coerce to have that type.

Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:7 Changed 2 years ago by simonpj

But I don't want the most general type of convert! The general principle of Coercible is that it simply automates what you could do by hand. E.g

newtype Age = MkAge Int

convert :: [Int] -> [Age]
convert xs = map MkAge xs

And back. So we can reasonably claim Coercible [Age] [Int].

It's the same with Coercible (a :~: b) (b :~: a), which is what you asked for. I can do it by hand (with convert); using coerce just automates it.

comment:8 Changed 2 years ago by goldfire

I'm not really sure what this ticket is about. The relation ~R# defines representational equality. The rules for this are written in the Coercible paper. There are several other tickets floating about talking about things that are provably ~R#, but that GHC's solver can't figure it out. This ticket is different, though: it seems to propose new rules for ~R#.

(Note: Coercible is defined as

class a ~R# b => Coercible a b
instance a ~R# b => Coercible a b

)

According to the rules for ~R#, we don't have (a :~: b) ~R# (b :~: a): the parameters to :~: both have a nominal role. (Note that role inference looks at constraints as well as other data members, so the a ~ b constraint in the type of Refl is what induces the nominal roles.)

It's conceivable that we could have newtype-GADTs, like

newtype a :~: b where
  Refl :: a ~ b => a :~: b

With a newtype-GADT, we could imagine forming (a :~: b) ~R# (b :~: a) by unwrapping, using sym and then wrapping using the newtype constructor. (I'm unsure how the solver would work here... but at least it's possible in Core.) Of course, we don't have newtype-GADTs.

And I'm afraid I don't understand what's going on in comment:3 and comment:4. How do these ideas relate to the definition of ~R#?

comment:9 Changed 2 years ago by simonpj

I'm not really sure what this ticket is about.

It's about the following questions:

  • Is (a :~: b) ~R# (b :~: a) sound?
  • And if so, what would be its evidence?

Remember we are talking only of when a value of type (a :~: b) can be coerced to one of type (b :~: a), ust as we speak of coercing a value of type [Int] to one of type [Age]. Curiuosly, the paper doesn't actually articulate the circumstances under which such a coercion is OK -- instead it describes role inference. My sanity check (again not articulated explicitly in the paper) is this: it's sound to coerce a value of type t1 into a value of type t2, and vice versa, if

  • I could write code of type t1 -> t2 and t2 -> t1
  • The runtime representations of the two are identical

Both properties hold for (a :~: b) and (b :~: a), regardless of a and b, don't they? So I claim that (a :~: b) ~R# (b :~: a) is sound.

But (a :~: a) ~R# (a :~: b) obviously must not hold, else I could write

good :: forall a. a :~: a
good = Refl

bad :: forall a b. a -> b
bad x = case (coerce (good @ a)) :: a :~: b of
           Refl -> x

(And, returning to the sanity check, I could not write a function of type (a :~: a) -> (a :~: b).)

So how could we prove (a :~: b) ~R# (b :~: a)? We have two ways to prove Coercible:

  • Decomposition on (T ts1) ~R# (T ts2), using the roles of T. That isn't going to work here because it loses the crucial connection bettween ts1 and ts2.
  • Newtype-unwrapping on (N ts1) ~R# t2. And (you are way ahead of me as usual), we could do that here if only :~: was a newtype. But, even leaving aside that we don't have newtype GADTs (I think we could maybe fix that), after decomposing both sides we'd have (a ~ b) ~R# (b ~ a). And now we are back to the original problem: what would be the evidence for such an equality?

comment:10 in reply to:  9 Changed 2 years ago by goldfire

Replying to simonpj:

  • Is (a :~: b) ~R# (b :~: a) sound?

You have described in your comment a new specification for representational equality: that two types are representationally equal when they are isomorphic and have identical runtime representations. It's too bad we never said that in the paper, because I agree with that specification. The paper then describes an incomplete "implementation" of that specification in its rules for representational equality. This is not the only source of incompleteness. See Appendix A.1 of the extended version of the original ICFP paper.

So, to your question: Is such a thing sound? It would appear to be so, yes. But until we have a full theory that allows such a coercion without breaking something else, I can't be sure.

  • And if so, what would be its evidence?

We don't have any representation. And you're right that even if we had newtype-GADTs (which would give a new challenge to the Constraint-vs-Type debate, because they're somewhat the converse of newtype-classes), we couldn't pull this off. (I was wrong on this point, above.) The question is whether (a ~# b) ~# (b ~# a). Right now, the answer is "no" because we can decompose (~#). However, Stephanie's new theory can handle such things, because it was designed not to be able to decompose (~#). I'm not intimately familiar with that end of her work, though. (In particular, I know it's forward-compatible with these ideas, but I don't know whether this end of the theory has been worked out in detail.)

My bottom line: GHC's notion of representational equality is useful, but still quite limited. There are lots of ways of expanding it. This is one of them.

comment:11 Changed 2 years ago by simonpj

My bottom line: GHC's notion of representational equality is useful, but still quite limited. There are lots of ways of expanding it. This is one of them.

Agreed. I'm meantally "parking" this.

Note: See TracTickets for help on using tickets.