Changes between Version 5 and Version 6 of InjectiveTypeFamilies


Ignore:
Timestamp:
Jul 15, 2014 8:36:13 AM (6 years ago)
Author:
jstolarek
Comment:

Formatting, fix broken links

Legend:

Unmodified
Added
Removed
Modified
  • InjectiveTypeFamilies

    v5 v6  
    1111  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.
    1212
    13   Example 1:
     13  '''Example 1'''
    1414{{{
    1515type family F a b c
     
    2121  2. Injectivity in some of the arguments, where knowing the RHS of a type family determines only some of the arguments on the LHS.
    2222
    23   Example 2:
     23  '''Example 2'''
    2424{{{
    2525type family G a b c
     
    3232  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.
    3333
    34   Example 3:
     34  '''Example 3'''
    3535{{{
    3636type family H a b c
     
    4040  Here knowing the RHS and any single parameter uniquely determines the remaining two parameters.
    4141
    42   Example 4:
     42  '''Example 4'''
    4343{{{
    4444type family J a b c
     
    8484Step 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.
    8585
    86 == Examples?
     86== Examples
    8787
    8888''If you can supply more examples (type family declarations + their usage that currently doesn't work but should work with injectivity) please add them here.''
    8989
    90 Example A:
     90'''Example A'''
    9191{{{
    9292type family F a | result -> a where
     
    100100GHC should infer that `a` is in fact `Char`. Right now this program is rejected.
    101101
    102 Example B: (taken from 6018#comment:5)
     102'''Example B''' (taken from [ticket:6018#comment:5])
    103103{{{
    104104data Nat
     
    114114type instance Succ Infinity         = Infinity
    115115}}}
    116 Mokus complains that GHC can't infer `Succ n ~ Succ m => n ~ m` because it can't see that `Succ` is injective.
     116GHC can't infer `Succ n ~ Succ m => n ~ m` because it can't see that `Succ` is injective.
    117117
    118 Example C: (taken from 6018#comment:26)
     118'''Example C''' (taken from [ticket:6018#comment:26])
    119119{{{
    120120class Manifold' a where