[GHC] #8185: Change role annotation syntax
#8185: Change role annotation syntax ----------------------------------------------+---------------------------- Reporter: goldfire | Owner: Type: feature request | goldfire Priority: normal | Status: new Component: Compiler | Milestone: 7.8.1 Keywords: | Version: 7.7 Architecture: Unknown/Multiple | Operating System: Difficulty: Moderate (less than a day) | Unknown/Multiple Blocked By: | Type of failure: Related Tickets: | None/Unknown | Test Case: | Blocking: ----------------------------------------------+---------------------------- Currently, role annotations look like this: {{{ data Foo a@N = ... }}} I've received several criticisms of this syntax: * It is not backward compatible. If a library wishes to use role annotations and remain compilable with earlier versions of GHC, preprocessor commands are necessary. * It is inscrutable for someone not well-versed in roles. * It reminds people of as-patterns, which it is unrelated to. * It is conceivable that it would conflict with type-level as-patterns. For these reasons, I propose the following: {{{ data Foo a {-# ROLE Nominal #-} = ... }}} This syntax, while verbose, eliminates these concerns, considering that the new syntax is easily searchable for someone who doesn't know it. I have proposed something similar on ghc-devs, with no response, so I will implement it shortly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by rwbarton): Sorry for last-minute bikeshedding but don't GHC pragmas usually precede the thing they attach to, when there may be ambiguity? E.g. consider {{{ data X = X !Int {-# UNPACK #-} !Int data Foo a {-# ROLE Nominal #-} b = ... }}} I know `data Foo {-# ROLE Nominal #-} a = ...` is ugly but... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by hvr): +1 to rwbart's [comment:1 comment] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by goldfire): Yes, very much agreed with rwbarton: {{{ data Foo {-# ROLE Nominal #-} a = ... }}} is the plan for labeling `a` with role `Nominal`. Also as part of this plan is to prefer writing out role names in full (e.g., "Nominal" not "N") to help with understanding and searching. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by simonpj): Thus far, pragmas have always been optional; that is, the program will compile ok without them. Eg INLINE pragmas, deprecations, SPECIALISE etc. This is different: the program won't typecheck without the pragma, and that is new. It's a bit like we put type signatures in pragmas. To me these role annotations are just like kind annotations. Why don't we put kind annotations in pragmas? Role annotations really are part of the ''language''. I'm ok with a noisy notation; it's only the pragma-brackets that bug me. Shall we explore some alternatives first? (Remember that whatever we do must be compatible with also having a kind annotation.) For example {{{ data Foo [Nominal] a = ... data Foo ([Nominal] a :: *) = ... data Foo [role Nominal] a = ... -- Or postfix versions data Foo a [Nominal] = ... data Foo a [role Nominal] = ... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by goldfire): Role annotations can appear for one of two reasons: * The writer of some datatype wishes to restrict its use and prevent `GeneralizedNewtypeDeriving` over classes that use that datatype. This type of role annotation can make only '''fewer''' programs type-check. Thus, it is '''never''' necessary, thus conforming to Simon's dictum about pragmas always being optional. * Types declared in hs-boot files must match the types in the base hs files. If the body of the type of omitted, a role annotation is sometimes necessary to make things match up. (Roles in hs-boot files default to Representational, which is the common case. This defaulting mechanism is documented in the hs-boot section of the manual.) This type of annotation is sometimes necessary, so it violates Simon's dictum. Given the second use of role annotations above, we may want to consider a non-pragma syntax, in order to keep pragmas as optional. (Though, it's worth noting that `LANGUAGE` pragmas are surely ''not'' optional.) I favor including the word "role" in the notation (for easy searching of an esoteric topic). I would also prefer using `{ }` over `[ ]` in a notation like Simon's suggestion -- braces are never used like that, and it avoids the appearance of talking about lists. I do have to say I'm not totally convinced that using a pragma is a bad idea. Not only are `LANGUAGE` pragmas required, but also `SOURCE` pragmas. Other thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by carter): Theres really two types of code folks will be writing in 7.8 1. Code that should be backwards compatible with prior GHCs, and in some cases even be (essentially) Haskell98 2. code that is unconditionally using ghc features only available in 7.8 and newer. It sounds like theres sound arguments for both the Pragma approach, and a clear "its part of the type, lets embrace that" approach. Having both would create its own complexity, but is that perhaps the best approach? terrible strawman that probably is a bad idea : a simpler solution is just to use the GHC CPP pass and have a different data / type declaration for the with vs without roles codes. This might result in a A LOT of CPP though for certain libraries. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by goldfire): It might be worth stressing that I expect role annotations to be very rare in practice. All of GHC uses exactly 0 role annotations. There are currently two in `base` (for `Ptr` and `FunPtr`) and I expect only a handful more once I ask `libraries@haskell.org` to think about roles. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by goldfire): In a conversation with several interested parties this morning, we came up with the following leading proposals: * Separate declaration, such as {{{ type roles Map nominal representational data Map a b = ... }}} Variants: Always use `type`? Or use `data` or `newtype` or `class`. * Use a `where` clause: {{{ data Map a b = ... where roles Map nominal representational }}} The role annotation would appear in the existing `where` clause for GADT-style declarations and for classes. A new `where` clause would be permitted for non-GADT-style data/newtype declarations. Variant: drop the redundant `Map`. It was decided that using a `{-# PRAGMA #-}` is a bad idea because roles are properly part of the language, not something outside it. Thus, whatever we do will not be backwards-compatible, and that desideratum is discarded. Though not brought up in the conversation, I would like to propose an alternative syntax for an inline annotation: {{{ data Map (a ::*, {nominal}) (b :: {representational}) = ... }}} Here, the role annotation is but in `{ }` along with a kind annotation. They are, of course, optional. A role annotation would also be accepted without a kind annotation -- the role would be distinguished by the `{ }`. Variant: add the word `role` in the braces. In any case, I would like to make a decision on this by early next week, to give me time to implement the change before 9/14. Thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Changes (by ekmett): * cc: ekmett@… (added) Comment: Simon, While I can respect the fact that other pragmas are forgettable without changing the compilability of the program, the big issue to me here is that by introducing Roles we're forcing users to choose between backwards compatibility and compatibility with other compilers, correctness under GHC and doing the right thing and putting on annotations when they need invariants. With a ```{-# ROLE #-}``` pragma users can at least write code that could work with other compilers without requiring an ```#ifdef``` block around every container type that provides invariants. I expect these to be a lot more common than Richard seems to, given that almost any sort of `Map`, `Set`, `Fingertree` or `Heap`-like data structure makes use of some invariant about its contents. I've been compiling a mental checklist of my own packages that will break when this goes in and it isn't a small list. It seems to me that this means any package that provides basically any sort of container is going to have to compile with `#ifdef`, which is a really ugly consequence of the current syntax. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by simonpj): I hate the idea of permanently messing up the language to secure backward compatibility. Maybe we can split into two questions: * What "should" it look like? * How can we secure backward compat? For the latter we might argue that of these two: {{{ {-# ROLES Map nominal representational #-} and #ifdef GHC >= 7.8 roles Map nominal representational #endif }}} that the former is so much better than the latter that we should support pragma syntax. (To me it's a bit moot, but I'll go with the flow.) But it still smells wrong to me to ''only'' have pragma syntax. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by goldfire): In a late afternoon conversation, Stephanie and I seemed to make some progress here. Of the three main alternatives I presented a few days ago, we agreed that the first was best, but with `type role` instead of `type roles`, to be consistent with the wealth of other, singular keywords. Why? * It makes the most sense with the different declaration forms that it affects. In particular, anything involving a `where` clause is awkward with non-GADT datatype declarations. We also toyed around with using a `deriving` clause, but that's awkward in general and in particular with classes. We even considered a `roles` clause that would syntactically be like `deriving`, but that would have to make `roles` a keyword. * Stephanie was very against my idea of including the role within the kind, because a role is really quite separate from a kind. The "include with kind" idea also makes using CPP for compatibility control rather painful. * Having separate role declarations makes dealing with backward compatibility more palatable, as a library author can lump all of a module's role declarations in one place, cordon the place off with an `#if`, and move on. Not quite as seamless as a pragma, but not so bad, either. * As Iavor pointed out in an email to me, having a separate declaration allows roles to be declared for promoted types. It's not clear to me what the value of this is, exactly, but it certainly won't hurt anyone. Knowing this community, someone will find a use for this feature. So, concretely, I propose the following form: A role declaration looks like {{{ type role <typename> <roles> }}} where `<typename>` is the name of the type being decorated (operators put in parentheses as usual). `<roles>` will be spelled out and in lowercase: {{{ type role Map nominal representational }}} The first word of the line will always be `type`, regardless of whether the actual declaration is a `data` or a `class`. (Separately (#8234), it has been decided to retract role annotations on type synonyms as too fragile.) If a role is to be inferred, it can be left out with `_`: {{{ type role Map' nominal _ }}} The number of roles given in a declaration must exactly match the number of (type, not kind) parameters in the real type declaration, including unnamed parameters in a GADT-style declaration. Role declarations are allowed for `data` and `class` types, and for promoted types, but not for families or other type-level declarations. How does this sound? Once implementation is under way, I'll add this proposal to [wiki:Roles] on the wiki. And, of course, I'll add notes in the user manual. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by simonpj): That's ok with me. So all we are left with is the choice about whether to support {{{ {-# ROLE Map nominal representational #-} }}} as alternative syntax for those who want to use a noisier syntax that allows the same module to be compiled with older role-ignorant GHCs, without #ifdefs. Personally I think that an #ifdef is clearer. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: new Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by hvr): Btw, older GHCs would warn (given the right warning flags) about the unknown `{-# ROLE ... #-}` pragma; `#ifdef`s however avoid that issue. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8185: Change role annotation syntax
----------------------------+----------------------------------------------
Reporter: | Owner: goldfire
goldfire | Status: new
Type: feature | Milestone: 7.8.1
request | Version: 7.7
Priority: normal | Keywords:
Component: | Architecture: Unknown/Multiple
Compiler | Difficulty: Moderate (less than a day)
Resolution: | Blocked By:
Operating System: | Related Tickets:
Unknown/Multiple |
Type of failure: |
None/Unknown |
Test Case: |
Blocking: |
----------------------------+----------------------------------------------
Comment (by Richard Eisenberg
#8185: Change role annotation syntax ----------------------------+---------------------------------------------- Reporter: | Owner: goldfire goldfire | Status: closed Type: feature | Milestone: 7.8.1 request | Version: 7.7 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: fixed | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8185#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC