Opened 3 years ago
Closed 3 years ago
#13140 closed feature request (fixed)
Handle subtyping relation for roles in Backpack
Reported by: | ezyang | Owned by: | ezyang |
---|---|---|---|
Priority: | normal | Milestone: | 8.4.1 |
Component: | Compiler (Type checker) | Version: | 8.1 |
Keywords: | backpack hs-boot | Cc: | RyanGlScott |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | Phab:D3123 | |
Wiki Page: |
Description
If I understand correctly, GHC's three currently supported roles follow the following subtyping relation: phantom <: representational <: nominal
. So it would make sense to adjust Backpack and hs-boot
files to handle this subtyping relation appropriately. Here's my proposal.
- Today, roles in signature files default to representational. Let's change the default to nominal, as this is the most flexible implementation side. If a client of the signature needs to coerce with a type, the signature can be adjusted to have more stringent requirements.
- If a parameter is declared as nominal in a signature, it can be implemented by a data type which is actually representational.
- When merging abstract data declarations, we take the smallest role for every parameter. The roles are considered fix once we specify the structure of an ADT.
I actually don't know if the proofs about roles actually say anything about this subtyping relation.
Change History (15)
comment:1 Changed 3 years ago by
Differential Rev(s): | → Phab:D3123 |
---|---|
Status: | new → patch |
comment:2 Changed 3 years ago by
comment:3 Changed 3 years ago by
Blah, that's terrible.
I'm trying to think how to solve this problem, because role mismatches in Backpack signatures are actually a problem in practice, that can't be easily worked around (speaking from experience Backpack'ing the reflex library). Let's leave aside hs-boot for now, where I think the current design works reasonably well.
Here is my proposal: let's introduce a new "abstract" role which is a blend of the phantom and nominal roles:
- Like phantom roles, we want
a ~A b
(where A is the abstract role) to hold for all choices a and b. Then, because the Co_Nth rule says that ifH a ~R H b
, thena ~ρ b
(where ρ is the role of the first type parameter of H), when H's role is abstract, we learn nothing about a and b. This is sufficient to cause your example to fail to typecheck.
- Like nominal roles, we should only have
H a ~R H b
ifa ~N b
; we would adjust the Co_TyConApp rule to always require nominal equality whenever we are at an abstract role type parameter.
Since there are no rules where you can use a ~A b
to derive another form of equality (in particular, we modified Co_TyConApp
to require nominal equality), the existing safety proof should go through without modification.
How does this sound?
comment:4 Changed 3 years ago by
If, from your perspective, the added complexity is worth it, then this looks OK to me.
What's frustrating here is that we don't really need a new Abstract
equality relation: the current Phantom
one works fine. All we need is a new role annotation. Is it worth creating a new data RoleAnnotation = Abstract | Concrete Role
? Perhaps. You would also then need to be careful about uses of tyConRoles
and tyConRolesX
, as they are currently used both for construction and decomposition -- up until this proposal, both directions were happy with the same roles.
I do agree that your approach is type safe. But I have to wonder if there isn't a simpler solution somehow, as I'm hesitant to advocate yet another wrinkle to the role system.
comment:5 Changed 3 years ago by
I'm not convinced the complexity is worth it. I think at least for GHC 8.2 we ought not to put in any of this, and we'll see if the role problems really cause people problems.
comment:6 Changed 3 years ago by
Milestone: | 8.2.1 → 8.4.1 |
---|
Alright, if I understand correctly nothing will be happing on this front until 8.4 at the earliest.
comment:7 Changed 3 years ago by
On SPJ's request: here are concrete examples showing that no choice of existing role is suitable for being "abstract":
- Suppose we pick
nominal
to be abstract. LetT
benominal
in its first argument: if we haveT a ~R T b
, we can derivea ~N b
. Now setT
tophantom
, then we haveInt ~P Bool
and consequentlyT Int ~R T Bool
. This lets us deriveInt ~N Bool
, bad!
- Suppose we pick
phantom
to be abstract. LetT
bephantom
in its first argument: then we haveT Int ~R T Bool
for all a and b. Now setT
tonominal
; ifT a ~R T b
, thena ~N b
; thus we haveInt ~N Bool
. Bad!
- Suppose we pick
representational
to be abstract. LetT
berepresentational
in its first argument: then we have that ifT a ~R T b
, thena ~R b
. Now setT
tophantom
, then we haveInt ~P Bool
and consequentlyT Int ~R T Bool
. But this impliesInt ~R Bool
, bad! (You can also do the other proof on this one.)
Another question was this: why doesn't subroling break this way? Subroling says that if we have a type variable a
at some role ρ, we can use it at role ρ' so long as ρ <= ρ'. (N is a subrole of everything). So for example, the following is acceptable:
data T a = MkT a type role S nominal data S a = MkS (T a)
In S, a is at role nominal, but we can pass it to a T which has a at role representational. What we are afraid of is having T a ~R T b
imply a ~N b
by using S. But from the hypothesis we get is a ~R b
, which does NOT imply S a ~R S b
(S is nominal!).
Another interesting observation is how we treat a polymorphic type constructor, e.g., m in forall m. m a -> m a
. Via the Co_App rule, to show m a ~ρ m' b
we must show m ~N m'
and a ~ρ b
(like the nominal role). Via the Co_Left rules, we can only say a ~N b
if m a ~N m' b
(just like the phantom role, we learn nothing when m a ~R m' b
). So the "abstract" role implicitly falls out of the way the coercion formation rules handle type variables!
All of this seems like evidence that adding an abstract role annotation is "the right thing to do."
comment:8 Changed 3 years ago by
Cc: | RyanGlScott added |
---|
comment:9 Changed 3 years ago by
The Right Thing to do is to go back in time and erase the idea of roles from our brains... and reimplement GeneralizedNewtypeDeriving
in terms of a generated blob of source code that gets type-checked (instead of the magical implementation it used to have).
Barring that, I can't find an argument against a new abstract role other than to groan.
comment:10 Changed 3 years ago by
After spending some time thinking through the proofs, I realized that goldfire's counterexample isn't actually valid, and we only need to do something complicated if we want to augment roles with a more fine-grained notion of injectivity.
First, let's see how GHC rejects goldfire's example today, via hs-boot files:
-- A.hs-boot {-# LANGUAGE RoleAnnotations #-} module A where data T a type role T nominal -- B.hs {-# LANGUAGE FlexibleContexts, RoleAnnotations #-} module B where import {-# SOURCE #-} A import Data.Coerce foo :: Coercible (T a) (T b) => a -> b foo x = x -- A.hs -- Doesn't really matter, but this will do: {-# LANGUAGE RoleAnnotations #-} module A where import B type role T nominal newtype T a = T Int
When we compile, we get:
B.hs:6:9: error: • Could not deduce: a ~ b from the context: Coercible (T a) (T b) bound by the type signature for: foo :: Coercible (T a) (T b) => a -> b at B.hs:5:1-38 ‘a’ is a rigid type variable bound by the type signature for: foo :: forall a b. Coercible (T a) (T b) => a -> b at B.hs:5:1-38 ‘b’ is a rigid type variable bound by the type signature for: foo :: forall a b. Coercible (T a) (T b) => a -> b at B.hs:5:1-38 • In the expression: x In an equation for ‘foo’: foo x = x • Relevant bindings include x :: a (bound at B.hs:6:5) foo :: a -> b (bound at B.hs:6:1)
This is because GHC only applies the Co_Nth rule if the TyCon in question is *injective*, and abstract types are NOT injective. In fact, they're obviously not because I can implement an abstract data type with a newtype (as I do in my example), and as was demonstrated in the roles paper, it is unsound to Co_Nth on newtypes. So, all we have to do is make sure Backpack abstract data types are not injective (and indeed, they're not) and there's no problem.
During our phone call, SPJ noticed that we could just unconditionally disable the Co_Nth rule if the TyCon was abstract or not (I didn't realize that they would already have been disabled), but we decided that the "abstract" strategy made more sense because you might *want* to say, "Hey, actually, I really do want you to be able to use Co_Nth on this parameter." Maybe it is worth investigating this, but for now I think it should be OK to merge Phab:D3123.
Since I've been thinking about this, let us talk about Co_Nth on newtypes. Consider the following program:
newtype T a = MkT a
Given T a ~R T b
, I might like to infer that a ~R b
. If T were a data type, I could do this directly, but with newtypes, since Co_Nth doesn't apply, I have to take a roundabout route: I show T a ~R a
and T b ~R b
(by the newtype axiom) and then apply transitivity to pop out the final coercion.
Under what situations would it be safe to apply Co_Nth here? Intuitively, the problem is that ascribed role for the parameter of T might not accurately describe how a is actually used in the body of the newtype, because it may have been weakened by subroling. That's bad news for Co_Nth, which really needs subroling to go "in the other direction."
I conjecture the following system would be sound:
- Associate every declaration with two sets of roles: one set that is applied in Co_TyConApp (call this the app-roles) and one that is applied for Co_Nth (call this the proj-roles). For data types, these are always the same.
- For newtypes, the app-roles are specified by the existing role assignment rules. However, the proj-roles are specified by the role assignment rules with the subroling relationship *flipped*: i.e., phantom is a subrole of nominal (not the other way around.)
- Proj-roles can be inferred like app-roles, but they are always consistent with proj-roles, and the subroling relationship is flipped.
Here are a few examples:
type app role T representational type proj role T representational newtype T a = MkT a -- T a ~R T b implies a ~R b type app role T nominal type proj role T representational -- NB: type proj role T nominal is NOT ALLOWED newtype T a = MkT a -- T a ~R T b implies a ~R b, BUT -- a ~R b is insufficient to prove T a ~R T b (you need a ~N b) type app role T nominal type proj role T phantom -- (representational and nominal not allowed) newtype T a = MkT Int -- T a ~R T b implies a ~P b (i.e. we don't learn anything) -- a ~N b implies T a ~R T b
To relate this back to the "abstract" role, what I have been calling an abstract role is actually a nominal app-role but phantom proj-role (i.e., the most flexible role of them all.) I ran into trouble trying to figure out how to infer abstractness, but I think if you make the language more expressive, that solves the problem.
comment:11 Changed 3 years ago by
I like comment:10.
I had forgotten that abstract types were not injective w.r.t. representational equality. Is this because GHC 8.0 (and below) allows an hs-boot file to say data
where the implementing module says newtype
? I can't think of another reason. In any case, this is a happy ending to your story.
As for the app-roles vs. proj-roles: very interesting. Currently, the solver runs into a problem when proving, say, N a ~R N b
, where N
is a newtype whose constructor is in scope: should we unwrap the newtype? Or use decomposition? (Note that this is somewhat the converse problem to the discussion above. Here we're trying to prove N a ~R N b
; previous discussion assumed N a ~R N b
and was trying to learn about a
and b
.) I forget exactly what happens here -- it's all in the paper. But I do remember that the resolution was dissatisfyingly incomplete in the case of recursive newtypes. Perhaps Edward's idea in comment:10 -- separate out two sets of roles -- provides a better way forward.
comment:12 Changed 3 years ago by
Is this because GHC 8.0 (and below) allows an hs-boot file to say data where the implementing module says newtype?
Yep.
Currently, the solver runs into a problem when proving, say, N a ~R N b, where N is a newtype whose constructor is in scope: should we unwrap the newtype? Or use decomposition?
Ah, this is very interesting (also, thank you for telling me about the journal paper; I didn't realize you had both an extended mix and a journal copy).
What we would like to do is two things:
- Allow decomposition on newtype givens (currently disallowed because Co_Nth doesn't work on newtypes). If we use the proj-roles here, that should solve the soundness problem.
- Do decomposition BEFORE unwrapping, so that if we hit
FixEither Age ~R FixEither Int
, we immediately jump toAge ~R Int
, rather than uselessly infinite loop on the newtype unwrapping.
(2) is a bit trickier. Suppose when you have something like this:
type app role T nominal type proj role T phantom newtype T a = MkT a
What "roles" should I use in the decomposition here, if I am trying to prove T Int ~R T Age
? Clearly, the only sound and complete choice is representational. Ignoring proj-roles for a moment, the reason we must flatten before we decompose, even today, is because if we decomposed the constraint above, we would end up with Int ~N Age
which is unsolvable.
So, it seems to me, that eager decomposition will go wrong (from a completeness perspective) UNLESS you know the "exact" roles of the newtype (the role computation without any subroling). The subroling doesn't affect soundness but it does affect completeness if your constraint solver doesn't backtrack (which ours does not.)
I'm also not sure if just (2) is guaranteed to get us to the point where newtype decomposition will actually apply, but the simple examples I thought of seemed to work (including the one in the paper.) Actually, (2) is not quite enough: if we have newtype S = MkS S
, then we can infinite loop when trying to solve S ~R T S
. But this seems to only be a problem when there is no intervening data type; if there is an intervening data type then unwrapping will stop at the data type, we'll unwrap the other side to the data type, we'll do a data decomposition, and NOW newtype decomposition applies.
comment:14 Changed 3 years ago by
Here's another way to think about app-roles and proj-roles.
Previously, we thought of roles as a single thing you ascribe to a type parameter. But it would be more accurate to say that a type parameter is given a role range, which specifies the possible set of underlying roles that the type may be implemented with. For example, the range "phantom to nominal" says that the type could be implemented in a way that treats the type variable phantom, representationally, or nominally: this is the most flexible for the implementor and gives the least information to the client. Or you can say that it is "exactly" nominal: this gives the most information to the client. type role T nominal; newtype T a = MkT a
gets "representational to nominal": the annotation sets the upper bound, but the lower bound has to actually include the true role which a is used at.
Of course, when I say lower bound, I mean proj-role, and when I say upper-bound, I mean app role. (I also apologize for flipping the subroling order.)
comment:15 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | patch → closed |
I'm marking this ticket as fixed but I'll open another ticket about role ranges.
Sorry for not piping up sooner, but this change would be unsound. Consider this accepted program:
You can see that, if
T
were abstract, instantiatingT
with a concrete datatype that had a phantom role would be Wrong. While there is a sub-roling relationship, it does not induce a sub-typing relationship like the one you seek.