Changes between Version 6 and Version 7 of NewAxioms


Ignore:
Timestamp:
Jun 6, 2012 12:35:48 AM (3 years ago)
Author:
sweirich
Comment:

Added comment about not having reflexivity reasoning.

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms

    v6 v7  
    66type family Equal a b :: Bool
    77}}}
    8 so 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 {{{
    10 type instance Equal a a = True
    11 type instance Equal Int Bool = False
    12 type instance Equal Bool Int = False
    13 }}}
    14 but this obviously gets stupid as you add more types.  Nor can you write
     8so that `(Equal t1 t2)` was `True` if `t1`=`t2` and `False` otherwise.  But it isn't. 
     9
     10You can't write
    1511{{{
    1612type instance Equal a a = True
     
    1814}}}
    1915because System FC (rightly) prohibits overlapping family instances. 
     16
     17Expanding this out, you can do it for a fixed collection of types thus:
     18{{{
     19type instance Equal Int Int = True
     20type instance Equal Bool Bool = True
     21type instance Equal Int Bool = False
     22type instance Equal Bool Int = False
     23}}}
     24but this obviously gets stupid as you add more types. 
     25
     26Furthermore, this is not what you want. Even if we restrict the equality function to booleans
     27{{{
     28type family Equal (a :: Bool) (b :: Bool) :: Bool
     29}}}
     30we can't define instances of Equal so that a constraint like this one
     31{{{
     32Equal a a ~ True
     33}}}
     34is satisfiable---the type instances only reduce if a is known to True or False. GHC doesn't reason by cases.  (Nor should it, |Any| also inhabits |Bool|. No kinds really are closed.)
     35
     36The only way to work with this sort of reasoning is to use Overlapping Instances, as suggested in the [http://homepages.cwi.nl/~ralf/HList/ HList paper.]
    2037
    2138== What to do about it ==