#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by jstolarek): A nice syntax proposal showed up on Haskell-cafe. The idea is to allow user to actually introduce a variable that names the result: {{{#!hs type family Id a :: (result :: *) | result -> a where type family F a b c :: (d :: *) | d -> a b c type family G a b c :: (foo :: *) | foo-> a b where type family Plus a b :: (sum :: Nat) | sum a -> b, sum b -> a where type family H a b c :: (xyz :: *) | xyz a -> b c, xyz b -> a c }}} No new keywords, so we get full backwards compatibility. I'm only wondering how this would interact with kind signatures for the result, which we allow now. Above I assumed that if a programmer wants to name the result she must supply a kind annotation. This might be a bit inconvenient. On the other hand I think that the range of possible names for type variables and kinds is disjoint, so we may actually guess whether the user means the kind of the result or its name by looking whether the identifier is capitalized. So we could just write: {{{#!hs type family Id a :: result | result -> a where type family F a b c :: d | d -> a b c type family G a b c :: foo | foo-> a b where type family Plus a b :: sum | sum a -> b, sum b -> a where type family H a b c :: xyz | xyz a -> b c, xyz b -> a c }}} The only caveat I see is that user might accidentally write `type family Plus a b :: nat` instead of `type family Plus a b :: Nat` and then get some weird compilation errors if the kind signature was essential to make the code compile. Still, I like this proposal best of all made so far. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:68 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler