Changes between Version 23 and Version 24 of InjectiveTypeFamilies
 Timestamp:
 Sep 3, 2015 4:45:13 AM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

InjectiveTypeFamilies
v23 v24 1 1 = Injective type families 2 2 3 This page summarizes the design behind injective type families (#6018). For the latest information about implementation progress see [[https://phabricator.haskell.org/D202D202]]. ETA: based on current progress I estimate that this should be completed around March 2015. This means injective type families will be available in GHC 7.12. 4 5 Person responsible for this page and the implementation: Jan Stolarek (just so 6 you now who is meant by "I"). 7 8 My current implementation is located on GitHub: 9 10 * https://github.com/jstolarek/ghc/tree/T6018injectivetypefamilies 11 * https://github.com/jstolarek/haddock/tree/T6018injectivetypefamilies 12 13 Note that you need to update the haddock submodule as well. Since it's a work in progress things might be broken. Also, I tend to do upstream rebases with these branches so beware when using `git pull`. 3 This page summarizes the design of injective type families (#6018). 4 Implementation discussion and progress was recorded in 5 [[https://phabricator.haskell.org/D202Phab D202]]. 6 7 As of September 2015 injective type families are merged into HEAD and will be 8 available in the next stable GHC release (8.0). 9 10 Person responsible for this page is Jan Stolarek (just so you now who is meant 11 by "I"). I am also responsible for most of the implementation. Simon Peyton 12 Jones and Richard Eisenberg participated in the development of theory behind 13 injective type families, so whenever I say "we" I mean the three of us. For 14 full discussion of injective type families see Haskell Symposium 2015 paper 15 "Injective type families for Haskell" (henceforth referred to as the 16 "injectivity paper"). 14 17 15 18 == Forms of injectivity 16 19 17 20 The idea behind #6018 is to allow users to declare that a type family is 18 injective. So far we have identified these forms of injectivity:21 injective. We have identified three forms of injectivity: 19 22 20 23 A. Injectivity in all the arguments, where knowing the result (righthand … … 53 56 {{{#!hs 54 57 type family Plus a b where 55 Plus Z 56 Plus (S m 57 }}} 58 59 Here knowing the RHS and any single argument uniquely determines the60 remainingargument.58 Plus Z n = n 59 Plus (S m) n = S (Plus n m) 60 }}} 61 62 Here knowing the RHS and the first argument uniquely determines the remaining 63 argument. 61 64 62 65 {{{#!hs … … 70 73 about `a` or `b`. 71 74 72 73 75 In the following text I will refer to these three forms of injectivity as A, B 74 76 and C. 75 77 76 '''Note that at the moment we only have practical use cases for injectivity of 77 form A. Because of that I propose that we implement only this form of injectivity.''' 78 We can implement B and C when somebody comes up with compelling use cases. 78 Currently GHC implements injectivity of type B (and therefore of type A as well, 79 since A is a subset of B). 79 80 80 81 == Proposed syntax 81 82 82 Two important things to consider when deciding on a concrete syntax are: 83 84 * '''Backwards compatibility''': at the moment no decision has been made on 85 whether injectivity will become a part of existing `TypeFamilies` extension 86 or if we create a new `InjectiveTypeFamilies` extension that implies 87 `TypeFamilies`. If we choose the former then we need to come up with syntax 88 that is backwards compatible. (Perhaps this is the other way around: if we 89 end up having backwards incompatible syntax then we must create a new 90 language extension). 91 92 * '''Future extensibility''': if we only implement A we still want to be able 93 to add B and C in the future without breaking A. 94 95 We decided to use syntax similar to functional dependencies. The injectivity 96 declaration begins with `` following type family declaration head. `` is 97 followed by a list of commaseparated injectivity conditions. Each injectivity 98 condition has the form: 99 100 {{{#!hs 101 A > B 102 }}} 103 104 where `A` and `B` are nonempty lists of type variables declared in type family 105 head. Things on the left and right of `>` are called LHS and RHS of an 106 injectivity condition, respectively. The user must be able to name the result of 107 a type family. To achieve that we extend syntax of type family head by allowing 108 to write `= tyvar` or `= (tyvar :: kind)` annotations in addition to already 83 When deciding on a concrete syntax our two main design goals were: 84 85 * '''Backwards compatibility''': injective type families are automatically 86 enabled with the `TypeFamilies` language extension. This means that the 87 proposed syntax had to be backward compatible, ie. not break any existing 88 code that uses type families. 89 90 * '''Future extensibility''': currently we we only implemented injectivity A 91 and B but we still want to be able to implement injectivity C in the future 92 without breaking A and B. 93 94 We decided to use syntax borrowed from functional dependencies. First of all 95 the user must be able to introduce a variable that names the result of a type 96 family. To achieve that we extend syntax of type family head by allowing to 97 write `= tyvar` or `= (tyvar :: kind)` annotations in addition to already 109 98 allowed `:: kind` annotation. In other words all these declaration are 110 99 wellformed: … … 118 107 119 108 but the third or fourth form is required if the user wants to introduce 120 injectivity declaration. Here are examples of injectivity declarations using 121 proposed syntax: 122 123 {{{#!hs 124 type family Id a = result  result > a where 125 type family F a b c = d  d > a b c 126 type family G a b c = foo  foo > a b where 109 injectivity annotation. The injectivity annotation itself begins with `` 110 following the result type variable. `` is followed by an injectivity 111 condition. Injectivity condition has the form: 112 113 {{{#!hs 114 A > B 115 }}} 116 117 where `A` is the result type variable and `B` is a nonempty lists of type 118 variables declared in type family head. Things on the left and right of `>` are 119 called LHS and RHS of an injectivity condition, respectively. If a type family 120 is injective in a given argument respective type variable must be mentioned in 121 the RHS of an injectivity condition. Variables may be skipped if a type family 122 is not injective in a given argument. 123 124 Here are examples of injectivity declarations using proposed syntax: 125 126 {{{#!hs 127 type family Id a = result  result > a where { ... } 128 type family F a b c = d  d > c a b 129 type family G a b c = foo  foo > a b where { ... } 130 }}} 131 132 This syntax can be easily extended in the future if we want to implement 133 injectivity of type C. First required change is that there may be many 134 commaseparated injectivity conditions. Second change is that LHS of 135 injectivity condition can mention type variables that name the arguments, not 136 just the result. With this extended syntax we could write: 137 138 {{{#!hs 127 139 type family Plus a b = (sum :: Nat)  sum a > b, sum b > a where 128 140 type family H a b c = xyz  xyz a > b c, xyz b > a c 129 141 }}} 130 142 131 Note that above examples demonstrate all three types of injectivivity but for 132 now we only plan to implement injectivity A. 133 134 Pros: 135 136 * natural reading: `res a > b` reads as "knowing res and a determines b". 137 138 * extensible for the future 139 140 * backwards compatible 141 142 Cons: 143 144 * since we only plan to implement injectivity of form A we require that there 145 is only one injectivity condition, its LHS contains only a type variable 146 naming the result and its RHS contains all type variables naming the 147 arguments to a type family. This might be a bit annoying. 148 149 150 == Reallife use cases 151 152 ''If you can supply more examples (type family declarations + their usage that 153 currently doesn't work but should work with injectivity) please add them here.'' 154 155 '''Example 1''' 156 157 {{{#!hs 158 type family F a = result  result > a where 159 F Char = Bool 160 F Bool = Char 161 F a = a 162 163 idChar :: (F a ~ Bool) => a > Char 164 idChar a = a 165 166 idDouble :: (F b ~ Double) => b > Double 167 idDouble a = a 168 }}} 169 170 GHC should infer that `a` is in fact `Char` and `b` is `Double`. Right now this program is rejected. 171 172 '''Example 2''' (taken from [ticket:6018#comment:5]) 173 174 {{{#!hs 175 data Nat 176 = Zero 177  Suc Nat 178 179 data CoNat 180 = Co Nat 181  Infinity 182 183 type family Succ (t :: CoNat) :: CoNat 184 type instance Succ (Co n) = Co (Suc n) 185 type instance Succ Infinity = Infinity 186 }}} 187 188 GHC can't infer `Succ n ~ Succ m => n ~ m` because it can't see that `Succ` is injective. 189 190 '''Example 3''' (taken from [ticket:6018#comment:26]) 191 192 {{{#!hs 193 class Manifold' a where 194 type Field a 195 type Base a 196 type Tangent a 197 type TangentBundle a 198 type Dimension a :: Nat 199 type UsesMetric a :: Symbol 200 project :: a > Base a 201 unproject :: Base a > a 202 tangent :: a > TangentBundle a 203 cotangent :: a > (TangentBundle a > Field a) 204 205  this works 206 id' :: forall a. ( Manifold' a ) => Base a > Base a 207 id' input = project out 208 where 209 out :: a 210 out = unproject input 211 212  but this requires injective type families 213 id' :: forall a. ( Manifold' a ) => Base a > Base a 214 id' = project . unproject 215 216 }}} 143 Note that for open and closed type families it is correct to declare a type 144 variable that names the result but skip the injectivity annotation. That is 145 not the case for associated types. If you name the result but ignore the 146 injectivity annotation GHC will interpret this as an associated type default. 217 147 218 148 == Implementation outline 219 149 220 === Verifying correctness of user's injectivity declaration 150 === Verifying correctness of injectivity annotation 151 152 Before checking that a type family is indeed injective, as declared by the user, 153 GHC needs to check the correctness of injectivity annotation itself. This 154 includes checking that: 155 156 * only inscope type variables are used. For example 157 `type family F a = r  r > b` should result with "not in scope: b" error. 158 159 See test T6018rnfail in the testsuite for more examples of invalid declarations. 160 161 === Verifying that type family equations agree with injectivity annotation 221 162 222 163 Once the user declares type family to be injective GHC must verify that this 223 declaration is correct, ie. type family really is injective. Below is an outline 224 of the algorithm. It is then follow with a discussion and rationale. ''Note: I 225 am not too familiar with GHC's type checking so please tell me if I'm making any 226 wrong assumptions here. Also, I might be using incorrect terminology. If so 227 please complain or fix.'' 228 229 '''Important''': this algorithm is only for the injectivity of type A. RHS 230 refers to the righthand side of the type family being checked for 231 injectivity. LHS refers to the arguments of that type family. 232 233 '''Algorithm''' 234 235 1. If a RHS contains a call to a type family we conclude that the type family is 236 not injective. I am not certain if this extends to selfrecursion  see 237 discussion below. 238 239 Open type families: 240 241 2. When checking equation of an open type family we try to unify its RHS with 242 RHSs of all equations we've seen so far. If we succeed then LHSs of unified 243 equations must be identical under that substitution. If they are not identical 244 then we declare that a type family is not injective. 245 246 '''RAE:''' I believe this would also have to check that all variables mentioned in the LHS are mentioned in the RHS. Or, following along with Simon's idea in comment:76:ticket:6018, those variables that appear in the injectivity annotation must be mentioned in the RHS. '''End RAE''' 247 248 Closed type families 249 250 3. If a type family has only one equation we declare it to be injective (unless 251 case 1 above applies). '''RAE''' or there are variables missing from the RHS '''End RAE''' 252 253 4. If a type family has more equations then we check them one by one. Checking 254 each equation consists of these steps: 255 256 0) verify 1) for the current equation. 257 258 a) attempt to unify RHS with RHSs of all previous equations. If this does not 259 succeed proceed to next equation. If this was the last equation then type 260 family is injective. 261 262 b) if unification in a) succeeds and no substitutions are required then type 263 family is not injective and we report an error to the user. By "no 264 substitution" I mean situation when there are no type variables involved 265 ie. both sides declare the same concrete type (eg. Int). '''RAE''' This seems to be a straightforward special case of (c). Omit? '''End RAE''' 266 267 c) if unification succeeds and there are type variables involved we substitute 268 unified type variables on the LHS and check whether this LHS overlaps with 269 any of the previous equations. If it does we proceed to the next equation 270 (if this was the last equation then type family is injective). If it 271 doesn't then type family is not injective and we report an error to the 272 user. See examples and discussion below for more details. 273 274 '''RAE:''' We have to be careful with the word ''overlap'' here. I think we want "overlaps" to be "is subsumed by". 275 276 Even subtler, it's possible that certain values for type variables are excluded if the current LHS is reachable (for example, some variable `a` couldn't be `Int`, because if `a` were `Int`, then a previous equation would have triggered). Perhaps these exclusions can also be taken into account. Thankfully, forgetting about the exclusions is conservative  the exclusions can only make ''more'' families injective, not ''fewer''. '''End RAE''' 277 278 '''RAE's examples''' 279 280 {{{#!hs 281 type family E2 (a :: Bool) = r  r > a where 282 E2 False = True 283 E2 True = False 284 E2 a = False 285 }}} 286 287 A naive injectivity check here would conclude that `E2` is not injective, because the RHS of the last equation unifies with the RHS of a previous equation, and the LHS of the last equation is not subsumed by any previous equation. But, noting that `a` (as used in the last equation) can neither be `True` nor `False`, `E2 is in fact injective. These are the "exclusions" I talk about above. 288 289 '''Discussion''' 290 291 Case 1 above is conservative and may incorrectly reject injectivity declaration 292 for some type families. For example type family `I`: 293 294 {{{#!hs 295 type family I a = r  r > a where 296 I a = Id a  Id defined earlier 297 }}} 298 299 is injective but restriction in case 1 will reject it. Why such a restriction? 300 Consider this example. Let us assume that we have type families `X` and `Y` that 301 we already know are injective, and type constructors `Bar :: * > *` and 302 `Baz :: * > * > *`. Now we declare: 303 304 {{{#!hs 305 type family Foo a = r  r > a where 306 Foo (Bar a) = X a 307 Foo (Baz a b) = Y a b 308 }}} 309 310 Here we would need to check whether results of `X a` and `Y a b` can overlap and 311 I don't see a good way of doing this once the RHS has nested calls to type 312 families. Second of all if we see `Foo a ~ Bool` during type checking GHC can't 313 solve that without trying each equation one by one to see which one returns 314 `Bool`. This takes a lot of guessing and I believe GHC should refuse to do that. 315 See also #4259. 316 317 What about selfrecursion? Consider this type family: 318 319 {{{#!hs 320  assumes promoted Maybe and Nat 321 type family NatToMaybe a = r  r > a where 322 NatToMaybe Z = Nothing 323 NatToMaybe (S n) = Just (NatToMaybe n) 324 }}} 325 326 Using Case 4a we will infer correctly that this type family is injective. Now 327 consider this: 328 329 {{{#!hs 330 type family Ban a = r  r > a where 331 Ban Z = Z 332 Ban (S n) = Ban n 333 }}} 334 335 To verify injectivity in this case we need to ask whether `Z ~ Ban n` (case 4a 336 above). We can only answer such question when a type family is injective. Here 337 we have not confirmed that `Ban` is injective so we may rightly refuse to answer 338 `Z ~ Ban n` and conclude (correctly) that this type family is not injective. So it 339 seems to me that we could allow selfrecursion  I have not yet identified any 340 corner cases that would prevent us from doing so. 341 342 '''RAE:''' But it seems that, under this treatment, any selfrecursion would automatically lead to a conclusion of "not injective", just like any other use of a type family. For example: 343 344 {{{#!hs 345 type family IdNat n = r  r > a where 346 IdNat Z = Z 347 IdNat (S n) = S (IdNat n) 348 }}} 349 350 `IdNat` is injective. But, following the algorithm above, GHC would see the recursive use of `IdNat`, not know whether `IdNat` is injective, and then give up, concluding "not injective". Is there a case where the special treatment of selfrecursion leads to a conclusion of "injective"? '''End RAE''' 351 352 Here's an example of case 4c in action: 353 354 {{{#!hs 355 type family Bak a = r  r > a where 356 Bak Int = Char 357 Bak Char = Int 358 Bak a = a 359 }}} 360 361 Equation 2 falls under case 4a. When we reach equation 3 we attempt to verify 362 it's RHS with each RHS of the previous equations. Attempt to unify `a` with 363 `Char` succeeds. Since unification was successful we substitute `Char` on the LHS 364 of the 3rd equation and get `Bak Char`. Now we must check if this equation 365 overlaps with any of the previous equations. It does overlap with the second 366 one, so everything is fine: we know that 3rd equation will never return a `Char` 367 (like 1st equation) because this case will be caught by the 2nd equation. We 368 know repeat the same steps for the second equations and conclude that 3rd 369 equation will never produce an `Int` because this will be caught by the 1st 370 equation. We thus conclude that `Bak` is injective. 371 372 === Other implementation details 373 374 The implementation needs to check the correctness of injectivity conditions 375 declarations. This includes checking that: 376 377 * only inscope type variables are used. For example 378 `type family F a  result > b` should result with "not in scope: b" error. 164 declaration is correct, ie. type family really is injective. Below are the 165 rules we follow when checking for injectivity of a type family. For full details 166 and rationale behind them see the injectivity paper, Section 4.2. 167 168 '''Important''': these rules are only for the currently implemented injectivity 169 of types A and B. RHS refers to the righthand side of the type family equation 170 being checked for injectivity. LHS refers to the arguments of that type family 171 equation. Term "type family equation" can refer to equations of both open and 172 closed type families, unless stated otherwise. 173 174 '''Rules for checking injectivity''' 175 176 A general idea is that if we find at least one equation (bullets (1), (2) and 177 (3)) or a pair of equations (bullets (4) and (5)) that violate injectivity 178 annotation then we conclude that a type family is not injective in a way user 179 claims and we report an error. 180 181 1. If a RHS of a type family equation is a type family application we conclude 182 that the type family is not injective. 183 184 2. If a RHS of a type family equation is a bare type variable we require that 185 all LHS variables (including implicit kind variables) are also bare. In 186 other words, this has to be a sole equation of that type family and it has to 187 cover all possible patterns. If the patterns are not covering we conclude 188 that the type family is not injective. 189 190 3. If a LHS type variable that is declared as injective is not mentioned on 191 injective position in the RHS we conclude that the type family is not 192 injective. By "injective position" we mean argument to a type constructor or 193 argument to a type family on injective position. 194 195 __Open type families (including associated types)__ 196 197 Open type families are typechecked incrementally. This means that when a module 198 is imported type family instances contained in that module are checked against 199 instances present in already imported modules. In practice this is done by 200 checking equations pairwise (a new equation against all already checked 201 equations  modulo optimisations). 202 203 4. When checking a pair of an open type family equations we attempt to unify 204 their RHSs. If they don't unify this pair does not violate injectivity 205 annotation. If unification succeeds with a substitution (possibly empty) 206 then LHSs of unified equations must be identical under that substitution. If 207 they are not identical then we conclude that a type family is not injective. 208 209 Note that we use a special variant of the unification algorithm that treats type 210 family applications as possibly unifying with anything. 211 212 __Closed type families__ 213 214 In a closed type family all equations are ordered and in one place. Equations 215 are also checked pairwise but this time an equation has to be paired with all 216 the preceeding equations. Of course a singleequation closed type family is 217 trivially injective (unless (1), (2) or (3) above holds). 218 219 5. When checking a pair of closed type family equations we try to unify their 220 RHSs. If they don't unify this pair does not violate injectivity annotation. 221 If the RHSs can be unified under some substitution (possibly empty) then 222 either the LHSs unify under the same substitution or the LHS of the latter 223 equation is subsumed by earlier equations. If neither condition is met we 224 conclude that a type family is not injective. 225 226 Again, we use a special variant of the unification algorithm. 227 228 === Source code tour 229 230 Below is a list of primary source code locations that implement injectivity: 231 232 * [[GhcFile(compiler/rename/RnSource.hs)]].`rnInjectivityAnn`: checks 233 correctness of injectivity annotation (mostly variable scoping). 234 235 * [[GhcFile(compiler/typecheck/FamInst.hs)]].`checkForInjectivityConflicts` is 236 an entry point for injectivity check of open type families. 237 238 * [[GhcFile(compiler/typecheck/TcTyClsDecls.hs)]].`checkValidClosedCoAxiom` is 239 an entry point for injectivity check of closed type families. 240 241 * [[GhcFile(compiler/types/FamInstEnv.hs)]].`injectiveBranches` checks that a 242 pair of type family axioms does not violate injectivity annotation. 243 244 * [[GhcFile(compiler/types/FamInstEnv.hs)]].`lookupFamInstEnvInjectivityConflicts` 245 implements condition (4) of injectivity check. 246 247 * [[GhcFile(compiler/typecheck/TcTyClsDecls.hs)]].`checkValidClosedCoAxiom.check_injectivity.gather_conflicts` 248 implements condition (5) of injectivity check. 249 250 * [[GhcFile(compiler/types/Unify.hs)]].`tcUnifyTyWithTFs` is our special 251 variant of a unification algorithm. 252 253 * [[GhcFile(compiler/typecheck/FamInst.hs)]].`makeInjectivityErrors` checks 254 conditions (1), (2) and (3) of the injectivity check. It also takes as an 255 argument results of check (4) or (5) and constructs error messages, if 256 necessary. 257 258 * [[GhcFile(compiler/typecheck/TcInteract)]], functions 259 `improveLocalFunEqs.do_one_injective` and `improve_top_fun_eqs` implement 260 typechecking improvements based on injectivity information. 261 262 Relevant source code notes are: 263 264 * `Note [FamilyResultSig]` in [[GhcFile(compiler/hsSyn/HsDecls.hs)]] 265 * `Note [Injectivity annotation]` in [[GhcFile(compiler/hsSyn/HsDecls.hs)]] 266 * `Note [Injective type families]` in [[GhcFile(compiler/types/TyCon.hs)]] 267 * `Note [Renaming injectivity annotation]` in [[GhcFile(compiler/rename/RnSource.hs)]] 268 * `Note [Verifying injectivity annotation]` in [[GhcFile(compiler/types/FamInstEnv.hs)]] 269 * `Note [Type inference for type families with injectivity]` in [[GhcFile(compiler/typecheck/TcInteract.hs)]] 270 271 272 == Injectivity for polykinded type families 273 274 With ''PolyKinds'' extension enabled it is possible to declare kind variables as 275 injective. Moreover, if a type variable is declared as injective its associated 276 kind variable is also considered injective. See section 6 of the injectivity 277 paper for full details. 278 279 == Connection with functional dependencies 280 281 In the course of our work it turned out that there is a close correspondence 282 between injective type families and functional dependencies. Section 7 of 283 the injectivity paper discusses this connection. 284 285 == Future plans and ideas 286 287 === Type C injectivity 288 289 Our plan for the nearest future is to implement injectivity of type C. This 290 will give injective type families expressive power identical to this of 291 functional dependencies. 292 293 If we decied to implement injectivity of type C checking injectivity annotation 294 would become more complicated as we would have to check for things like: 295 296 * `type family F a b = r  r > a, r > b`. This is technically correct but we 297 could just say `result > a b`. 379 298 380 299 * there are no identical conditions (this wouldn't hurt, but the user deserves … … 382 301 383 302 * type variables are not repeated on either LHS or RHS of the injectivity 384 condition. For example `r esulta a > ...` or `... > a b a` should generate303 condition. For example `r a a > ...` or `... > a b a` should generate 385 304 a warning. Note that it probably is OK to have the same variable both on the 386 305 LHS and RHS of an injectivity condition: in the above examples it is true … … 391 310 `result > a`). This probably deserves a warning. 392 311 393 I am not certain at the moment how to treat these injectivity conditions394 declarations:395 396 * `result > a, result > b` is technically correct but we could just say397 `result > a b`. Do the two separate declarations have the same power as the398 combined one?399 400 312 === Inferring injectivity 401 313 402 314 [ticket:6018#comment:45 Here] it was suggested by Simon that we could infer 403 injectivity for closed type families. This is certainly possible for injectivity 404 A, but not for B or C, where the number of possible injectivity conditions is 405 exponential in the number of arguments. I personally am against inferring 406 injectivity. The reasons are: 407 408 * Before 7.10 comes out there will already be some code in the wild that uses 315 injectivity for closed type families. I initially argued that, while inferring 316 injectivity of type A should be simple, inferring injectivity of type B would be 317 exponential in the numer of arguments to a type family. I take back that claim 318 as I now believe the algorithm can be made linear in the number of 319 arguments. Say we have a closed type family: 320 321 {{{#!hs 322 type family F a b c ... n = r where 323 }}} 324 325 Since there are n arguments there are 2^n possible injectivity annotations. 326 That's why I believed that we have to check every possible annotationton. I now 327 believe that instead checking every possible annotation we should only check 328 whether knowing the RHS allows to infer each argument independently. In other 329 words when inferring injectivity we would check whether annotations `r > a`, `r 330 > b`, `r > c` ... `r > n` hold true. If we learn for example that knowing `r` 331 allows to infer `a`, `c` and `n` but not the other argumenst we infer the 332 annotation `r > a c n`. 333 334 There are several concerns to consider before implementing this: 335 336 * Before GHC 8.0 comes out there will already be some code in the wild that uses 409 337 closed type families introduced in GHC 7.8. None of these type families 410 338 require injectivity to work because GHC 7.8 does not support injectivity. If … … 416 344 417 345 * I believe that requiring explicit injectivity annotations is a valuable 418 source code documentation for the programmer. 419 420 * Annotations also make it explicit which code will compile with GHC 7.10 and 421 which will not. 346 source code documentation for the programmer. This is very subjective, but 347 the truth is injectivity is very subtle and can easily be broken by slight 348 modifications of type family definition. It is much better to be explicit 349 about relying on injectivity. 350 351 * Annotations also make it explicit which code compiles with GHC 8.0 and 352 which does not. If we infer injectivity the code that works with 8.0 might 353 result in typing errors for earlier GHC versions. Of course requiring 354 annotations will also prevent that code from compiling but I believe that it 355 will be easier for the programmer to track the source of the problem when 356 she gets syntax errors rather than typing errors. 422 357 423 358 * I don't like the idea of mismatch between open type families and closed type 424 359 families, meaning that injectivity of open type families would be openly 425 360 documented whereas for closed type families it would be hidden. 426 427 == Injectivity for polykinded type families 428 429 (based on Richard's comments on Phab) 430 431 Current implementation of injectivity only works over *type* variables, ignoring *kind* variables. This is OK because all kind variables have to have type variables dependent on them, and if a type family is injective in its type variables, it then must be injective in its kind variables. But, if/when we allow partial injectivity annotations, this might require some more thought. Consider 432 433 {{{ 434 type family Foo (a :: k) (b :: *) = (r :: k)  r > b 435 }}} 436 437 That family is injective in `k`, but you have to be careful to discover this fact. And, what about 438 439 {{{ 440 type family Bar (a :: k) = r  r > a 441 }}} 442 443 Here, the family is still injective in `k`, but you need to make sure to note it when recording the partial injectivity. 444 445 Currently we disallow: 446 447 {{{ 448 type family Baz (a :: k) = r  r > k 449 }}} 450 451 But such a thing is reasonable to want! You're saying that result determines the kind of the input, though perhaps not the type. 452 453 454 == Other notes 455 456 * This page does not mention anything about associated types. The intention is 457 that injectivity will also work for those. I just haven't thought about the 458 details yet. 459 460 * [ticket:6018#comment:48 Here] Richard mentions headinjectivity used by 461 Agda. We don't plan to follow that direction. 462 463 * I'm not yet sure what is the exact scope of things we want to do with 464 injectivity. Certainly if we have `F a ~ F b` and `F` is injective then we 465 can declare `a ~ b`. (Note: Simon remarks that in such case `a` must be a 466 skolem constant and `b` a unification variable. I don't know the difference 467 between the two). Moreover if we have `F a ~ Int` then we can infer `a`. But 468 what if we also have injective type family `G` and see a constraint like 469 `F a ~ G b c`? For injective type families there exists at most one solution 470 but I think that GHC should refuse to solve such riddles. 361 Counterargument: there is already a mismatch between open and closed type 362 families, since the latter have kind inference. 363 364 * If we ever implement injectivity of type C it might not be possible to infer 365 injectivity annotation of type C. I think that this time the algorithm will 366 really be exponential. 367 368 == Example use cases 369 370 In the injectivity paper we presented two practical use cases for injectivity. 371 If you have more uses cases to demonstrate please add them here. 372