Changes between Version 3 and Version 4 of NewAxioms


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