Changes between Version 6 and Version 7 of NewAxioms


Ignore:
Timestamp:
Jun 6, 2012 12:35:48 AM (23 months 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 ==