Changes between Version 3 and Version 4 of NewAxioms


Ignore:
Timestamp:
Jan 16, 2012 2:09:18 PM (2 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms

    v3 v4  
    1 GHC branch: `ghc-axioms` 
     1= Pattern-matching axioms = 
    22 
    3 See https://github.com/dreixel/New-axioms for a draft of the design ([https://docs.google.com/open?id=0B1pOVvPp4fVdOTdjZjU0YWYtYTA5Yy00NmFkLTkxMWUtZmI0NmNhZTQwYzVl cached pdf]). 
     3== Background ==  
     4One might imagine that it would be a simple matter to have a type-level function 
     5{{{ 
     6type family :: Equal a b :: Bool 
     7}}} 
     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: 
     9{{{ 
     10type instance Equal a a = True 
     11type instance Equal Int Bool = False 
     12type instance Equal Bool Int = False 
     13}}} 
     14but this obviously gets stupid as you add more types.  Nor can you write 
     15{{{ 
     16type instance Equal a a = True 
     17type instance Equal a b = False 
     18}}} 
     19because System FC (rightly) prohibits overlapping family instances.   
     20 
     21== What to do about it == 
     22 
     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: 
     24{{{ 
     25type instance where 
     26  Equal a a = True 
     27  Equal a b = False 
     28}}} 
     29 
     30This wiki page is a stub: 
     31 * See [https://github.com/dreixel/New-axioms this Github repo] for a Latex draft of the design 
     32 * Here is a [https://docs.google.com/open?id=0B1pOVvPp4fVdOTdjZjU0YWYtYTA5Yy00NmFkLTkxMWUtZmI0NmNhZTQwYzVl cached pdf] of the current state 
     33 * We'll use GHC branch `ghc-axioms` for development work. 
     34 
     35Status (Jan 12): the groundwork is done, in HEAD; mainly making `CoAxiom` a more fundamental data type.  Not yet started on the details.