Changes between Initial Version and Version 1 of InjectiveTypeFamilies


Ignore:
Timestamp:
Jul 14, 2014 11:11:22 AM (6 years ago)
Author:
jstolarek
Comment:

First draft

Legend:

Unmodified
Added
Removed
Modified
  • InjectiveTypeFamilies

    v1 v1  
     1= Injective type families
     2
     3This page summarizes the design behind injective type families (#6018). It is a work in progress. This page will evolve to reflect the progress made.
     4
     5Person responsible for this page and the implementation: Jan Stolarek (just so you now who is meant by "I").
     6
     7== Outline
     8
     9The idea behind #6018 is to allow users to declare that a type family is injective. The plan is to allow several kinds of injectivity:
     10
     11  1. Injectivity in all the arguments, where knowing the result (right-hand side) of a type family determines all the arguments on the left-hand side.
     12
     13  Example 1:
     14{{{
     15type family F a b c
     16type instance F Int  Char Bool = Bool
     17type instance F Char Bool Int  = Int
     18type instance F Bool Int  Char = Char
     19}}}
     20
     21  2. Injectivity in some of the arguments, where knowing the RHS of a type family determines only some of the arguments on the LHS.
     22
     23  Example 2:
     24{{{
     25type family G a b c
     26type instance G Int  Char Bool = Bool
     27type instance G Int  Char Int  = Bool
     28type instance G Bool Int  Int  = Int
     29}}}
     30  Here knowing the RHS allows us to determine first two arguments, but not the third one.
     31
     32  3. Injectivity in some of the arguments, where knowing the RHS of a type family and some of the LHS arguments determines other (possibly not all) LHS arguments.
     33
     34  Example 3:
     35{{{
     36type family H a b c
     37type instance H Int  Char   Double = Int
     38type instance H Bool Double Char   = Int
     39}}}
     40  Here knowing the RHS and any single parameter uniquely determines the remaining two parameters.
     41
     42  Example 4:
     43{{{
     44type family J a b c
     45type instance J Int  Char   Double = Int
     46type instance J Bool Double Double = Int
     47}}}
     48  Knowing the RHS and either `a` or `b` allows to uniquely determine the remaining two parameters, but knowing the RHS and `c` gives us no information about `a` or `b`.
     49
     50Note that examples above are shown for open type families but the implementation will work for both open and closed type families.
     51
     52== Proposed syntax
     53
     54The proposed syntax for injectivity declaration is based on functional dependencies syntax. 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:
     55
     56{{{
     57result A -> B
     58}}}
     59where `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 ans RHS of an injectivity condition, respectively. `result` becomes a restricted word that cannot be used as a type variables identifier in a type family declaration (neither in declaration head nor in the equations). This is identical to how the `role` word is treated.
     60
     61The examples given in the "Outline" section could have the following injectivity conditions:
     62
     63{{{
     64type family F a b c | result -> a b c
     65type family G a b c | result -> a b
     66type family H a b c | result a -> b c, result b -> a c, result c -> a b
     67type family J a b c | result a -> b c, result b -> a c
     68}}}
     69For closed type families each of the above lines would be appended with the `where` keyword.
     70
     71== Plan of attack
     72
     73My plan is to divide implementation of this feature into smaller steps, each of which will provide a working set of features usable to the end users of GHC. These are the steps:
     74
     75  1. Implement injective type families that are:
     76
     77     a) injective in all the arguments (Example 1 above)
     78
     79     b) only admit RHS that is a concrete type or a call to a type constructor or a type variable introduced by the LHS or a recursive call to self. This means that calls to another type family will result in compilation error for type families declared as injective.
     80
     81  2. Lift restriction a) ie. allow type families injective only in some arguments (Examples 2-4 above)
     82  3. Lift restriction b) ie. allow injective type families to call other type families?
     83
     84Step 3 of the above outline is in fact more in the lines of #4259 so it will most likely not be implemented as part of #6018.
     85
     86== Examples?
     87
     88''I was unable to come up with compelling examples, ie. such examples that are both real-life and short enough to demonstrate on the wiki. If anyone can supply such examples (type family declarations + their usage that currently doesn't work but should work with injectivity) please add them here. Below are toy examples.''
     89
     90Example A:
     91{{{
     92type family F a | result -> a where
     93    F Char = Bool
     94    F Bool = Int
     95    F Int  = Char
     96
     97idChar :: (F a ~ Bool) => a -> Char
     98idChar a = a
     99}}}
     100GHC should infer that `a` is in fact `Char`. Right now this program is rejected.
     101
     102== Implementation outline
     103
     104''This section outlines '''what''' will be done in the implementation, without giving specific details '''how''' it will be done. Details on the implementation within GHC will be added as work progresses.''
     105
     106The implementation needs to check the correctness of injectivity conditions declarations. This includes checking that:
     107
     108  - only in-scope type variables are used. For example `type family F a | result -> b` should result with "not in scope: b" error.
     109  - there are no identical conditions (this wouldn't hurt, but the user deserves a warning about this)
     110  - type variables are not repeated on either LHS or RHS of the injectivity condition. For example `result a a -> ...` or `... -> a b a` should generate a warning. Note that it probably is OK to have the same variable both on the LHS and RHS of an injectivity condition: in the above examples it is true that `type family G a b c | result c -> a b c`. The question is whether this has any practical relevance.
     111  - injectivity conditions don't overlap (eg. `result -> a b` overlaps `result -> a`). This probably deserves a warning.
     112
     113I am not certain at the moment how to treat these injectivity conditions declarations:
     114
     115  - `result -> a, result -> b` is technically correct but we could just say `result -> a b`. Do the two separate declarations have the same power as the combined one?
     116
     117Of course the implementation needs to verify that injectivity conditions specified for a type family really hold.
     118
     119== Questions without an answer (yet)
     120
     121  1. Is there a point in allowing injectivity declarations for associated types?