[GHC] #8177: Roles for type families
#8177: Roles for type families ------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Now that we have [wiki:Roles roles], it might be helpful to be able to give a role signature for a data/type family. At the moment, data/type family constructors have all parameters conservatively assigned to be role `N`. Thus {{{ data family D a -- Parameter conservatively assumed to be N class C a where op :: D a -> a instance C Int where .... newtype N a = MkN a deriving( C ) -- Rejected }}} The generalised-newtype-deriving clause `deriving( C )` is rejected because `D` might use its parameter at role `N` thus: {{{ data instance D [b] = MkD (F b) -- F is a type function }}} It would be strictly more expressive if we could * '''Declare''' the roles of D's arguments (as we can declare their kinds). E.g. {{{ data family D a@R }}} * '''Check''' that each family instance obeys that role signature. E.g. given the preceding role signature, reject this instance: {{{ data instance D [b] = MkD (F b) -- F is a type function }}} I think there is no technical difficulty here. Just a question of doing it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I would argue that, given the declaration for `D` above, the following instance should also be rejected: {{{ data instance D (Maybe c) = MkD2 c }}} Why should that instance be rejected? Because it pattern-matches on its argument. Before thinking about implementing this (which I agree should be straightforward), we need to agree on the design. Here are a few questions to spur discussion: * What should the default role be for families? Is it different for data and for type families? (I would prefer N for both.) * Am I right that the instance above should be rejected? * Consider {{{ type family Flip x@R y@R type instance Flip x y = (y, x) }}} Is that accepted? I think "yes". Here are some proposed rules: * If a parameter is at role N, its use is unrestricted in instances. * If a parameter is at role R, it cannot be matched against and it must only appear in R (or P) positions in the RHS of instances. * If a parameter is at role P, it cannot be matched against and it must only appear in P positions in the RHS of instances. Thoughts? Let's have the conversation here, and I will put the resolution on the wiki along with writing the implementation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): Harump. You are right. `type` families are the very source of pattern matching so ''of course'' `type` families should have argument of role N. You could argue that there might be a parameter of the family that is never matched. Thus: {{{ type family F a@R b@N type instance F a Int = a -> a type instance F a Bool = (a,a) }}} But it's a bit marginal; in most cases you could re-order the args {{{ type family F b@N :: * -> * }}} and similarly for the instances. I think it's the same for `data` families. For example, it'd be utterly wrong to make a newtype coercion between `(D Age)` and `(D Int)`; so `D`'s parameter must clearly be role N. In short, the main merit of this ticket would be to allow ''parametric'' (non-indexed) parameters to appear before ''index'' parameters. That seems a fairly marginal gain. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I'm not convinced that this is useless, actually. For example, I don't think Simon's last example `F` could be written without role annotations on type families, even if we switch the order of parameters. And, the kind signature trick doesn't work at all with data families: {{{ data family Q1 :: * -> * }}} is equivalent to {{{ data family Q2 a }}} In particular, under the current implementation, instances of `Q1` ''can'' pattern-match on the parameter. Accordingly, `Q1`'s parameter is currently given role N, just like `Q2`'s. So, I do think this idea would yield a real expressiveness gain, and I mused about it while implementing the main chunk of roles. Is it worth the extra complexity? Perhaps. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): A post on #8672 seems more relevant here: Simon PJ says: Richard, two questions. First (Q1), can't a data instance have a representational role inferred? Eg this ought to work. The definition of `g` is currently rejected. {{{ data family T a data instance T [b] = MkT b newtype Age = MkAge Int g :: T [Age] -> T [Int] g x = coerce x }}} Second question (Q2). Are role annotations allowed on data family declarations, where they could indicate which parameters are the indices: {{{ type role T representational nominal -- Only second param can be an index data family T a b data instance T a Bool = ... -- Allowed data instance T Bool b = ... -- Rejected }}} (And similarly for type families.) Similarly are role annotations allowed on data instance declarations, where they would be useful in exactly the same way that they are on data decls {{{ data family T a type role T [a] (a:nominal) data instance T [a] = MkT a }}} Here we are running out of syntax! This isn't supported now because I think all parameters are automatically nominal (see Q1 for why they shouldn't be). Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by goldfire): * owner: => goldfire Comment: Q1: Yes, that's possible. I didn't do it mostly because my stomach lurched when thinking about parsing role annotation concrete syntax for data family instances -- I was going to wait until someone shouted. I considered having data instances go through role inference without allowing for role annotations, but that meant it would be impossible to create a properly abstract data family instance. Q2: That's possible but currently unimplemented (see earlier posts to this bug report). So, if we could just figure out a decent concrete syntax, I could make it all work. The hardest part will be updating the parser and `HsSyn` stuff. The role inference/checking should be almost no work at all. As a strawman syntax, what about {{{ type role instance T [nominal] }}} for the case above. Note the word `instance` to specify that we're talking about the roles on an instance, not on the family `T`. Then, role names would appear wherever type variables appear in the corresponding instance declaration. Underscores would be supported in these positions, as well (like normal role annotations). The corresponding data (or newtype) instance would have to be in the same module, as usual. The appearance of the word `type` (as opposed to `data`) in the role annotation syntax is regrettable, but it conforms to the universal use of the word `type` in all role annotations. Though it makes me want to cry, I suppose we should allow ''associated'' role instance annotations, in class instance definitions alongside associated data/newtype instances. Does anyone out there actually want to use this feature? Eager users would help motivate all this! :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by carter): @goldfire, conflating list syntax seems red flaggy... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by carter): that said, having some way of describing these properties seems important, though i'm not sure if i'm sufficiently sophisticated a library author yet to see a use case for myself as yet -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): But that's the annotation for the instance {{{ data instance T [a] }}} If we had an instance {{{ data instance T (Int, Maybe a) }}} the role annotation would be {{{ type role instance T (Int, Maybe representational) }}} for example. (Though, that particular annotation would be a no-op, as `representational` would be inferred.) I don't believe I'm conflating list syntax here... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by carter): you may be right! I'll reread this ticket when i'm a bit more awake :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): See also [http://www.haskell.org/pipermail/glasgow-haskell- users/2014-May/025000.html this thread on the GHC users list], which offers (I think) another example of the importance of this feature. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by jwlato): I agree that the `vector` issue is related to this feature. In summary, we would like the following to work (greatly simplified from vector WLOG): {{{ class MVectorClass (v :: * -> * -> *) a where basicLength :: v s a -> Int data family MVector s a data instance MVector s Int -- implementation not important newtype Age = Age Int deriving (MVectorClass MVector) -- rejected }}} The deriving is rejected because it generates {{{ basicLength = coerce (basicLength :: MVector s Int -> Int) :: MVector s Age -> Int }}} If my understanding of role inference is correct, allowing {{{ type role instance MVector nominal representational }}} would allow for this coerce to take place. This means that we can't currently derive Unbox instances for vectors of newtypes (see https://github.com/haskell/vector/issues/16), which is rather unfortunate. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by jwlato): * priority: normal => high -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by liyang): * cc: hackage.haskell.org@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by goldfire): * priority: high => normal Comment: Hmm... well, this just got a little more complicated. The full example John just posted would not be solved by fixing this ticket. That's because the data instance for `MVector` ''pattern-matches'' on `Int`. Currently in GHC, it would be sound to have both the instance given and a separate instance ending in `Age`, and have these instances be unrelated. Accordingly, if the `MVector` were declared to have a representational role for its last parameter, the instance given would be rejected for pattern-matching on a representational parameter. What it seems John wants is something new -- a data family that does ''representational'' matching, not nominal matching. Such a beast would consider `data instance MVector s Int` and `data instance MVector s Age` to overlap. Along similar lines, if a `MVector s Age` were requested, GHC would serve up the instance for `MVector s Int`. While I can imagine implementing such a feature (essentially by preventing newtypes from appearing in instance declarations, much like how type families can't appear in instance declarations today... and then normalizing with respect to newtypes at usage sites), the ramifications of the design are far from clear. In particular, what if the constructor of a newtype is not available? It would also mean, for example, that if a library exports a newtype `Foo` abstractly, a user wishing to have an `MVector` instance for `Foo` would need to know `Foo`'s representation type, something that the library author thought was hidden from users. It's all a little murky. So, I'm saying that John's use case does ''not'' qualify for this ticket, and I'll un-bump its priority. John, if in light of my analysis (and if you agree with it!) you still want this feature, create a new feature request with the priority you feel is appropriate. This seems related but quite separable to the features requested in this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by jwlato): It's only outside the scope of this request if you insist on the rule that parameters at role R can't be matched against. I think I agree with Richard's analysis that this would entail a data family that does representational matching. I do think this is a valuable feature as ghc-7.8 broke code some code in the wild, so I'll make a new ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by crockeea): * cc: ecrockett0@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by dmcclean): * cc: dmcclean (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dmcclean): This would be helpful for one implementation that Bjorn Buckwalter and I are working on for the next generation version of the dimensional library. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): dmcclean: can you say more precisely what "this" is? There are various designs floating about in this ticket, and comment:14 indicates that the one in the Ticket Description would not solve the problem identified in comment:11. Better still, can you give a concrete, standalone example of what you want/need? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dmcclean): Yes, my apologies Simon. This is actually going to be an interesting example, perhaps, because I learned something about this since yesterday when I wrote that comment. This example is slightly longer than I would like, I'm eliding a few things but I'm not sure exactly which details (e.g. the data family being associated) matter. {{{ class KnownVariant (var :: Variant) where -- | A dimensional value, either a 'Quantity' or a 'Unit', parameterized by its 'Dimension' and representation. data Dimensional var :: Dimension -> * -> * -- elided: some functions to allow us to introduce and eliminate the quantities or units instance KnownVariant DQuantity where newtype Dimensional DQuantity d v = Quantity' v deriving (Eq, Ord, Enum) -- elided: function implementations instance KnownVariant (DUnit p) where data Dimensional (DUnit p) d v = Unit' UnitName v -- elided: function implementations data Variant = DQuantity | DUnit Prefixability type Quantity = Dimensional DQuantity type Unit p = Dimensional (DUnit p) }}} So I set up all that machinery, and then I was curious whether we could `coerce` in and out of the `Dimensional DQuantity d` newtype. So I thought that the way to find out was by asking GHCi what the role of `Dimensional` was. In concept it's `nominal phantom representational`, but it would be extremely complicated for the compiler to see that because it would have to examine all the (both the) instances and so forth, so I didn't know what to expect. {{{ Numeric.Units.Dimensional.DK> :i Dimensional class KnownVariant (var :: Variant) where type role Dimensional nominal nominal nominal data family Dimensional (var :: Variant) ($a :: Dimension) $b ... }}} So I read that, and thought that it meant we were out of luck. But, unexpectedly to me, but undoubtedly for a reason that is quite obvious to someone, and this is the part I only discovered last night: {{{
let x = 3.7 :: Double x 3.7 let y = (coerce x) :: Mass Double y 3.7 kg let x' = (coerce y) :: Double x' 3.7 }}}
Somehow it even seems to be OK when you abstract over the dimension with RankNTypes, which isn't really a need but is just something I thought to investigate to see if that was the difference between my expectation of how this would work and how it in fact did work. {{{
let f = coerce :: (forall d.Double -> Quantity d Double) (f 3) :: Mass Double 3.0 kg }}}
In conclusion, I now believe that I was too hasty yesterday, and that in fact this ticket doesn't impact me at all. My sincere apologies to everyone copied on this ticket. If someone happened to have the time and knew the answer, it would be awesome if you you could help me fix my understanding about whether this should or shouldn't work and what the interplay with roles is, but otherwise I will merrily go about my business. :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Roles for data families (associated or not) cannot be inferred, because they are open. But, theoretically, they can be declared and then checked. That is the subject of this ticket. So, it conceivable to give the roles you ask for. But, you don't seem to need those roles, because you seem interested in coercing in and out of the newtype, not among different instantiations of the newtype. This is possible as long as the newtype constructor (`Quantity'`) is in scope. Roles aren't a part of the story, in your case. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dmcclean): Hmmm. I was concerned there for a second, because actually `Quantity'` won't be in scope for my users. Its not exported from the module because you can use it to do nefarious things. So I thought that my test in GHCi had been insufficiently thorough, because GHCi doesn't respect the export list and lets you get at unexported things for convenience. So I made a new module to try it. {{{ import Numeric.Units.Dimensional.DK.Prelude import Data.Coerce main = do let x = 3.7 :: Double let y = (coerce x) :: Mass Double putStrLn . show $ y -- putStrLn . show $ Quantity' x -- doesn't compile with this line here }}} It works just fine and prints "3.7 m". With the commented line it doesn't compile, complaining that `Quantity'` is (as I intended) not in scope. (If it had been in scope, it would still fail because the dimension is ambiguous, but that's not the point.) So it seems that whether or not the newtype constructor is in scope is not the determining factor here. If it was intended to be, than this may be a bug? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): That does look fishy, but I don't see a definition of `Mass` so I can be sure. Do you have a minimal test case, or a way I can check this myself? If so, please post that as a new ticket, as it's only very tangentially related to this one. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by rwbarton): Replying to [comment:22 dmcclean]:
Hmmm.
I was concerned there for a second, because actually `Quantity'` won't be in scope for my users. Its not exported from the module because you can use it to do nefarious things.
BTW I'm confused by this comment, because the things you can do with `Quantity'` are just the things you can do with `coerce`, no? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dmcclean): Yes. I was badly confused when I wrote that comment, sorry. See 9580 for where I broke this out as requested by goldfire. It turns out that the rule is indeed supposed to be that you can only do this coercion when `Quantity'` is in scope, which makes sense because that is when you could do it longhand, but that 7.8.3 currently implements a more lenient unintentional rule that also lets you do it (at least sometimes?) when you only have the data family in scope. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by goldfire): * milestone: => ⊥ -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): In trying to sweep up remaining tickets assigned to me before the feature freeze, I came across this one. In comment:5, I ask for real users who want role annotations for type and/or data families (and/or their respective instances) to do real work -- preferably with an example of said real work. Though two people came out of the woodwork and tried to meet this need, neither one really qualifies: - The example from jwlato requires something fundamentally different from this ticket -- the ability to do representational matching on families. That, essentially, has been moved to #9112. The solution there may also require getting this ticket sorted out, but I don't think this ticket is the blocking issue. - The example from dmmclean is also, by dmmclean's own admission, not applicable here. Fixing this would take several days worth of work, and days are precious. So I'm going to let this one slip unless convinced otherwise. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Making a note here to look at `:browse` and `:info` in GHCi if/when we implement this. See also #8672. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by jwlato): Just a quick note to verify that goldfire is entirely correct WRT #9112; I agree that my example doesn't have much bearing on this ticket at this point. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) Comment: goldfire, I do have a need for this in order to do "real work"... at some point in the future after #9123 is fixed :) My use case is laid out in [https://ghc.haskell.org/trac/ghc/ticket/8516#comment:7 this comment] in #8516. I'm interested in using higher-kinded roles to increase the number of datatypes for which you can derive `Generic1` instances by replacing `Functor` constraints with `Representational` constraints (where `Representational` is the typeclass proposed [https://ghc.haskell.org/trac/ghc/ticket/9123#comment:5 here]). Unfortunately, at the moment, my proposed plan would actually //decrease// that number, because there are datatypes defined in terms of type families for which you can declare `Functor` instances. However, type families always default to `nominal` roles for its type arguments, which means they can't be `Representational`! Ack! It definitely seems like //some// type families should be able to have `Representational` (or even `Phantom`!) roles for its arguments. A prime example is from [https://ghc.haskell.org/trac/ghc/ticket/8516#comment:7 this comment]: {{{#!hs type family Id a where Id a = a }}} I have a strong hunch that `a` should be have a `representational` role. Unfortunately, I have no way to inform GHC of this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies 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 glguy): I'd like to share my usecase for wanting this feature Given the following type: {{{#!haskell -- | Family of N-ary operator types. type family Op n a b where Op 'Z a b = b Op ('S n) a b = a -> Op n a b }}} I'd love to be able to {{{#!haskell coerce :: Coercible a b => Op n a c -> Op n b c }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies 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 int-index): I want this feature too. My use case is this: {{{#!hs data family EffDict (eff :: k) (m :: Type -> Type) }}} this data family represents effect methods for some monad `m`. Its data instances match on `eff` only, never on `m`. For example: {{{#!hs data StateEff s data instance EffDict (StateEff s) m = StateDict { _state :: forall a . (s -> (a,s)) -> m a, _get :: m s, _put :: s -> m () } }}} Define a composition of monad transformers as follows: {{{#!hs newtype TComp t1 t2 m a = TComp (t1 (t2 m) a) }}} Then I want to be able to do this: {{{#!hs coerce :: Dict eff (t1 (t2 m)) -> Dict eff (TComp t1 t2 m) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:33 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by int-index): * cc: int-index (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:34 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3662 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * differential: => Phab:D3662 Comment: I've uploaded a rough attempt at implementing support for roles for closed type families at Phab:D3662, although there are still some bugs to work out (for instance, the program in comment:32 doesn't typecheck yet, unfortunately). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:35 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3662 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
I've uploaded a rough attempt at implementing support for roles for closed type families
Great work! But I really would prefer to see a specification first :-). There's a lot of discussion on this thread about what the specification should even be. It's hard to review an implementation without a spec, covering * Syntax * Typing rules (at least in clear English) * Lots of examples Of course, we'd ultimately like a proof of soundness of the rules, but the "Richard thinks this is right" tests is at least a start. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:36 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3662 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Indeed, I will readily admit that I'm mostly parking this Diff here for Richard's sake (when he gets a chance to look at it). However, since you asked politely, I wrote up an (informal) specification of how I envision this would work [https://ghc.haskell.org/trac/ghc/wiki/Roles#Proposal:rolesfortypefamilies here], based on the conversations I've had with Richard about this topic, as well as the commentary in this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:37 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3662 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I've commented on the wiki page (the specification) and on the diff. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:38 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3662 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Thanks for replying, Richard! I'll respond to your comments here (since I don't like using wiki pages as a medium of conversation).
**RAE**: "feels"? Let's prove it! End **RAE**
Hoo boy, I was afraid you were going to demand a proof. I certainly don't have one at the moment.
**RAE**: There is a difference between roles for data families and data instances. And both might usefully have role annotations. For example:
{{{#!hs data family DF a b type role DF nominal representational
data instance DF Int b = MkDFInt b -- NB: No scrutinizing the second parameter. -- Also, b is not used in a nominal context
data instance DF [c] b = MkDFList c b type role DF [nominal] representational
data instance DF (Maybe d) b = MkDFMaybe d b type role DF (Maybe representational) representational }}}
With this, we have `Coercible (DF (Maybe Age) Int) (DF (Maybe Int) Age)` but not `Coercible (DF [Age] Int) (DF [Int] Age)`.
I'm a bit worried about problems with what happens if a type constructor
**RAE**: This works well for closed type families, but is ineffective with open type/data families (associated or not). I propose that open families default to nominal roles. This is quite like how open families' type variables default to kind Type. Edit: I see this addressed below, but
Ah, I think there's a bit of confusion regarding the extent of this design. To be clear, I am not proposing that we give users the power to specify roles the type variables in each //equation//, only the type variables of the parent type family itself. This is because: 1. As your example hints at, we'd need to invent a new syntax for role annotations that match on particular types, and I don't feel anywhere near motivated enough to implement that. 2. The current implementation of role inference does not lend itself well to this design. GHC assigns roles by using a map from `TyCon` names to roles, but type family equations have neither `TyCon`s nor any kind of unique identifier from which we could look up its roles after inference. 3. This kind of power isn't necessary for the kind of stuff I'd want to do anyways. All I really care about is that the second parameter is designated as `representational`. I don't really want the ability to `coerce` between `DF (Maybe Age) Int` and `DF (Maybe Age) Int`. So in your above example: {{{#!hs data family DF a b type role DF nominal representational data instance DF [c] b = MkDFList c b data instance DF (Maybe d) b = MkDFMaybe d b }}} I would propose that the tyvars in any type pattern which saturates `a` should inherit the role of `a`, so `c` and `d` would get role `nominal` in their respective equations. It's not as permissive as it //could// be, but for reasons that I explained above (and I'll make a note of this in the wiki). that appears as part of a type pattern for an instance is actually a newtype with a role annotation -- could we be breaking soundness with this? Need to think harder. I don't understand this point. the opening paragraph for this section mentions inference for open families. **End RAE** Yep, that's my bad. I'll update the intro so as not to mislead readers. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:39 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3662 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:39 RyanGlScott]:
Hoo boy, I was afraid you were going to demand a proof. I certainly don't have one at the moment.
"Demand"? No. But it would be nice if the design could at least update the various relevant judgments in the "Safe coercions" paper (use the JFP version). It shouldn't be terribly much work, and it's likely that the process of doing so will reveal any glaring problems. And once you have the updated judgments, it's also not terribly hard to follow along the JFP proof and see what lemmas have to be updated. I'm always daunted by having to revisit the type safety proof. But every time I go through the process, my brain feels nice, limber, and at peace. It's all very much like a good yoga session: it's hard to find the time to do it, it involves painful contortions, and yet you feel quite good at the end.
Ah, I think there's a bit of confusion regarding the extent of this design. To be clear, I am not proposing that we give users the power to specify roles the type variables in each //equation//, only the type variables of the parent type family itself.
Note that instance-specific roles apply only to ''data'' families, not ''type'' families.
This is because:
1. As your example hints at, we'd need to invent a new syntax for role annotations that match on particular types, and I don't feel anywhere near motivated enough to implement that.
And neither was I, as you'll see in my comment:5.
2. The current implementation of role inference does not lend itself well to this design. GHC assigns roles by using a map from `TyCon` names to roles, but type family equations have neither `TyCon`s nor any kind of unique identifier from which we could look up its roles after inference.
This isn't as bad as you say. Data family instances ''do'' have a `TyCon`. See the `DataFamilyInst` constructor of `FamInstEnv.FamFlavor`.
3. This kind of power isn't necessary for the kind of stuff I'd want to do anyways. All I really care about is that the second parameter is designated as `representational`. I don't really want the ability to `coerce` between `DF (Maybe Age) Int` and `DF (Maybe Age) Int`.
So perhaps you want just roles for ''type'' families for now, not ''data'' families.
So in your above example:
{{{#!hs data family DF a b type role DF nominal representational data instance DF [c] b = MkDFList c b data instance DF (Maybe d) b = MkDFMaybe d b }}}
I would propose that the tyvars in any type pattern which saturates `a`
should inherit the role of `a`, so `c` and `d` would get role `nominal` in their respective equations. It's not as permissive as it //could// be, but for reasons that I explained above (and I'll make a note of this in the wiki). But any time a pattern introduces a new tyvar (that's not just a renaming of the tycon tyvar), then the "parent" tyvar's role is always nominal (because you're doing pattern matching). As you note, this is not as permissive as possible. But, I would argue that if you were as permissive as possible, then you'd have no way of making a fully-abstract data family instance. So your design is self-consistent.
I'm a bit worried about problems with what happens if a type
constructor that appears as part of a type pattern for an instance is actually a newtype with a role annotation -- could we be breaking soundness with this? Need to think harder.
I don't understand this point.
I was worried about something like this: {{{#!hs newtype Inty a = MkInty Int type role Inty representational -- just because I can data family F a type role F nominal data instance F (Inty a) = MkF a type role F (Inty nominal) }}} Is this a good idea? I don't know. Keep in mind that data families are injective. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:40 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3662 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:40 goldfire]:
I'm always daunted by having to revisit the type safety proof.
It's doubly daunting for me because I wouldn't be //re//visiting the proof—I'd be trudging through it for the first time. :) Not to say that I'm not willing to do this at some point, but it will take me a significant amount of time to invest in understanding the terminology (keep in mind I'm far from an expert on the intricacies of System FC), not to mention figuring out how to typeset all of those crazy typing judgments in TeX.
So perhaps you want just roles for ''type'' families for now, not ''data'' families.
But any time a pattern introduces a new tyvar (that's not just a renaming of the tycon tyvar), then the "parent" tyvar's role is always nominal (because you're doing pattern matching). As you note, this is not as permissive as possible. But, I would argue that if you were as
Well, I //do// want to have roles for data families at some point (I started with closed type families since they're considerably easier to implement). I just don't want to worry about the additional baggage that per-data-instance role annotations would entail. permissive as possible, then you'd have no way of making a fully-abstract data family instance. So your design is self-consistent. Absolutely. I'm fine with making `nominal` roles be overly restrictive, since it dodges thorny issues like data abstraction...
I was worried about something like this:
{{{#!hs newtype Inty a = MkInty Int type role Inty representational -- just because I can
data family F a type role F nominal
data instance F (Inty a) = MkF a type role F (Inty nominal) }}}
Is this a good idea? I don't know. Keep in mind that data families are injective.
...and this sort of thing as well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:41 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8177: Roles for type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * differential: Phab:D3662 => -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8177#comment:42 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC