Changes between Version 3 and Version 4 of NewAxioms

Jan 16, 2012 2:09:18 PM (3 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.