Changes between Version 3 and Version 4 of NewAxioms

Jan 16, 2012 2:09:18 PM (4 years ago)



  • NewAxioms

    v3 v4  
    1 GHC branch: `ghc-axioms`
     1= Pattern-matching axioms =
    3 See for a draft of the design ([ cached pdf]).
     3== Background ==
     4One might imagine that it would be a simple matter to have a type-level function
     6type family :: Equal a b :: Bool
     8so that `(Equal t1 t2)` was `True` if `t1`=`t2` and `False` otherwise.  But it isn't.  You can do  it for a fixed collection of types thus:
     10type instance Equal a a = True
     11type instance Equal Int Bool = False
     12type instance Equal Bool Int = False
     14but this obviously gets stupid as you add more types.  Nor can you write
     16type instance Equal a a = True
     17type instance Equal a b = False
     19because System FC (rightly) prohibits overlapping family instances. 
     21== What to do about it ==
     23So the deficiency is in System FC, and it seems fundamental.  We've been working on an extension to System FC, with a corresponding source-language extension, that does allow overlapping type families, with care. You would write something like this:
     25type instance where
     26  Equal a a = True
     27  Equal a b = False
     30This wiki page is a stub:
     31 * See [ this Github repo] for a Latex draft of the design
     32 * Here is a [ cached pdf] of the current state
     33 * We'll use GHC branch `ghc-axioms` for development work.
     35Status (Jan 12): the groundwork is done, in HEAD; mainly making `CoAxiom` a more fundamental data type.  Not yet started on the details.