wiki:NewAxioms

Version 4 (modified by simonpj, 2 years ago) (diff)

--

Pattern-matching axioms

Background

One might imagine that it would be a simple matter to have a type-level 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 source-language 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:

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 goldfire 20 months ago. Description of FC extension to support overlapping type family instances

Download all attachments as: .zip