Changes between Version 16 and Version 17 of InjectiveTypeFamilies


Ignore:
Timestamp:
Oct 14, 2014 1:59:09 AM (5 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • InjectiveTypeFamilies

    v16 v17  
    267267Even 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'''
    268268
     269'''RAE's examples'''
     270
     271Here are some examples that I've come up with that show some tricky points:
     272
     273{{{#!hs
     274type family E1 a = r | r -> a where
     275  E1 Int = Int
     276  E1 a   = a
     277}}}
     278
     279According to the algorithm above, this would be rejected as non-injective. This is because clause (c) of the closed type family check says that if an equation is not subsumed by a previous equation, yet the RHSs unify, the family is flagged as non-injective. Yet, `E1` ''is'' injective.
     280
     281Here's another one:
     282
     283{{{#!hs
     284type family E2 (a :: Bool) = r | r -> a where
     285  E2 False = True
     286  E2 True  = False
     287  E2 a     = False
     288}}}
     289
     290A 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.
     291
    269292'''Discussion'''
    270293