Version 4 (modified by 6 years ago) (diff)  ,

Patternmatching axioms
Background
One might imagine that it would be a simple matter to have a typelevel function
type family :: Equal a b :: Bool
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:
type instance Equal a a = True type instance Equal Int Bool = False type instance Equal Bool Int = False
but this obviously gets stupid as you add more types. Nor can you write
type instance Equal a a = True type instance Equal a b = False
because System FC (rightly) prohibits overlapping family instances.
What to do about it
So the deficiency is in System FC, and it seems fundamental. We've been working on an extension to System FC, with a corresponding sourcelanguage extension, that does allow overlapping type families, with care. You would write something like this:
type instance where Equal a a = True Equal a b = False
This wiki page is a stub:
 See this Github repo for a Latex draft of the design
 Here is a cached pdf of the current state
 We'll use GHC branch
ghcaxioms
for development work.
Status (Jan 12): the groundwork is done, in HEAD; mainly making CoAxiom
a more fundamental data type. Not yet started on the details.
Attachments (1)

axioms.pdf (212.0 KB)  added by 5 years ago.
Description of FC extension to support overlapping type family instances
Download all attachments as: .zip