[GHC] #14362: Allow: Coercing (a:~:b) to (b:~:a)
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: roles | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Is there *any* sensible way to enable coercing [https://hackage.haskell.org/package/base-4.10.0.0/docs/Data-Type- Equality.html#t::-126-: (:~:)] swapping its arguments {{{#!hs coerce :: a:~:b -> b:~:a }}} Same for [https://hackage.haskell.org/package/base-4.10.0.0/docs/Data- Type-Coercion.html#t:Coercion Coercion] {{{#!hs coerce :: Coercion a b -> Coercion b a }}} Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Where the compiler knows constraints (`(~)` and `Coercible`) are symmetric -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Is it not ultimately about implication of constraints ([https://www.reddit.com/r/haskell/comments/6me3sv/quantified_class_constraint... quantified constraints]) {{{#!hs -- 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 {{{#!hs type family ToConstraint (kind :: Type) = (res :: Type) | res -> kind where ToConstraint Type = Constraint ToConstraint (a -> b) = a -> ToConstraint b type family Underlying (dataty :: kind) :: ToConstraint kind where Underlying (Dict ctx) = ctx Underlying Coercion = Coercible Underlying (:~:) = (~) Underlying (:~~:) = (~~) }}} we can could write these in a more general form: {{{#!hs instance (Underlying thing => Underlying thing') => Coercible thing thing' instance (Underlying thing a => Underlying thing' a') => Coercible (thing a) (thing' a') instance (Underlying thing a b => Underlying thing' a' b') => Coercible (thing a b) (thing' a' b') }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): A user defined type with "no represented value arguments" could generate an `Underlying` type instance {{{#!hs 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 }}} So depending how smart our constraint solver is, we can coerce {{{#!hs coerce :: LessThanEq a b -> LessThanEq a (10 + b) coerce :: LessThanEq a b -> GreaterThanEq b a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): But what is the most general type of `convert Refl = Refl`? We cannot write {{{#!hs -- 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 have to be deduce `a' ~ b'` from the given context `a ~ b`, which is this? {{{#!hs convert :: ((a~b) => (a'~b')) => (a :~: b) -> (a' :~: b') convert Refl = Refl }}} so I would expect `coerce` to have that type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 {{{#!hs 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 {{{#!hs 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#`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:9 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 [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1013&context=compsci_pubs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14362: Allow: Coercing (a:~:b) to (b:~:a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC