Haskellers, there is some discussion going on at the moment about implementing injective type families in GHC [1]. I'd like to hear your opinions on proposed syntax for this new feature. == Problem == Currently GHC assumes that type families are not injective. This is of course conservative and the idea behind implementing injective type families is to allow the programmer to explicitly declare that a type family has the injectivity property (which GHC will of course verify). == Forms of injectivity == Injectivity can take forms more complicated than just determining the LHS from RHS: A. RHS determines all arguments on the LHS. Example: type family Id a where Id a = a Here the RHS uniquely determines LHS. B. RHS determines some but not all arguments on the LHS. Example (contrieved): type family G a b c where G Int Char Bool = Bool G Int Char Int = Bool G Bool Int Int = Int Here RHS uniquely determines `a` and `b` but not `c`. C. RHS and some LHS arguments uniquely determine some LHS arguments. Example: type family Plus a b where Plus Z m = m Plus (S n) m = S (Plus n m) Here knowing the RHS and one of LHS arguments uniqely determines the other LHS argument. At the moment we've only seen use cases for A, which means that we will most likely only implement A. If someone comes up with compelling examples of either B or C we will revise and consider implementing these more involved forms of injectivity. == Syntax == So the most important decission to make is what syntax do we want for this new feature :-) One of the features we would like is extensibility, ie. if we only implement injectivity of type A we still want to be able to add injectivities B and C sometime in the future without breaking A. When thinking about syntax an important (and open) question is whether injectivity becomes part of TypeFamilies language extension or do we add a new InjectiveTypeFamilies extension for this feature. The problem with incorporating injectivity into existing TypeFamilies is that we would have to come up with syntax that is fully backwards compatible with what we have now. Below is a list of proposals that have come up until now in the discussion between developers. Note that all proposals are given for closed type families. For open type families things would be identical except that the `where` keyword would be skipped. === Proposal 1 === Use syntax similar to functional dependencies. The injectivity declaration begins with `|` following type family declaration head. `|` is followed by a list of comma-separated injectivity conditions. Each injectivity condition has the form: {{{ result A -> B }}} where `A` is a possibly-empty list of type variables declared in type family head and `B` is non-empty list of said type variables. Things on the left and right of `->` are called LHS and RHS of an injectivity condition, respectively. `result` becomes a restricted word that cannot be used as a type variable's identifier in a type family head. Examples: type family Id a | result -> a where type family G a b c | result -> a b where type family Plus a b | result a -> b, result b -> a where Pros: * has natural reading: `result a -> b` reads as "knowing the result and the type variable a determines b". * extensible for the future Cons: * steals `result` identifier in the type family head. This means it would be illegal to have a type variable named `result` in a type family. * the above also makes this proposal backwards incompatible with TypeFamilies extension. Further proposals are based on this one in an attempt to solve the problem of stealing syntax and backwards incompatibility. === Proposal 2 === Use `Result` instead of `result`: type family Id a | Result -> a where type family G a b c | Result -> a b where type family Plus a b | Result a -> b, Result b -> a where Pros: * has natural reading * extensible for the future * allows to have type variables named `result` (does not steal syntax) Cons: * all other keywords in Haskell are lowercase. This would be the first one that is capitalized. * confusion could arise if we have a type `Result` and use it in the type family head. Unknowns (for me): * not sure if it would be possible to avoid name clash between `Result` and type of the same name. If not then this proposal would also be backwards incompatible with TypeFamilies. === Proposal 3 === Use `type` instead of `result`: type family Id a | type -> a where type family G a b c | type -> a b where type family Plus a b | type a -> b, type b -> a where Pros: * extensible for the future * no syntax stealing Cons: * no natural reading * usage of `type` here might seem unintuitive === Proposal 4 === Use name of the type family instead of `result`: type family Id a | Id -> a where type family G a b c | G -> a b where type family Plus a b | Plus a -> b, Plus b -> a where Pros: * extensible for the future * no syntax stealing Cons: * writing something like `Plus a` might be confusing. It looks as if Plus could be partially applied. == Further discussion == I'd like to hear what you think about these proposals. Neither of them is perfect so perhaps someone can come with something better. You can also check out the GHC Trac ticket [1] and the GHC Wiki page [2] (which repeats most of this but has some more details as well). [1] https://ghc.haskell.org/trac/ghc/ticket/6018 [2] https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies Janek