Version 15 (modified by danbst, 5 years ago) (diff)

possible typo?

Pattern-matching axioms

This page describes an extension to type families that supports overlap.

  • 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 ghc-axioms for development work.
  • See also the Discussion Page added May 2012, for comment/suggestions/requests for clarification/alternative solutions, to explore the design space.
  • We'll need some concrete syntax for the discussion, so we'll follow the cached pdf, but note that the syntax there is not final.

Status (Jan 12): the groundwork is done, in HEAD; mainly making CoAxiom a more fundamental data type. Not yet started on the details.


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't write

type instance Equal a a = True
type instance Equal a b = False

because System FC (rightly) prohibits overlapping family instances.

Expanding this out, you can do it for a fixed collection of types thus:

type instance Equal Int Int = True
type instance Equal Bool Bool = True
type instance Equal Int Bool = False
type instance Equal Bool Int = False

but this obviously gets stupid as you add more types.

Furthermore, this is not what you want. Even if we restrict the equality function to booleans

type family Equal (a :: Bool) (b :: Bool) :: Bool

we can't define instances of Equal so that a constraint like this one

Equal a a ~ True

is 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.)

The only way to work with this sort of reasoning is to use Overlapping Instances, as suggested in the HList paper.

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. Here's the idea, but do look at the Latex document pointed to from the top of this page for details.

  • A type instance declaration can define multiple equations, not just one:
    type instance Equal where
      Equal a a = True
      Equal a b = False
  • Patterns within a single type instance declaration (henceforth "group") may overlap, and are matched top to bottom.
  • A single type family may, as now, have multiple type instance declarations:
    type family F a :: *
    type instance F where
      F [Int] = Int
      F [a]   = Bool
    type instance F where
      F (Int,b) = Char
      F (a,b)   = [Char]
  • The groups for F may not overlap. That is, there must be no type t such that (F t) matches both groups.
  • The groups do not need to be exhaustive. If there is no equation that matches, the call is stuck. (This is exactly as at present.)
  • It would perhaps be possible to emit warnings for equations that are shadowed:
    type instance F where
      F (a,b)   = [Char]
      F (Int,b) = Char
    Here the second equation can never match.
  • The equations do not need to share a common pattern:
    type instance F where
      F Int = Char
      F (a,b) = Int
  • Optional extra: It would make sense to allow the type family and type instance declaration to be combined into one, in cases where all the equations can be given at the definition site. For example:
    type family Equal a b :: Bool where
      Equal a a = True
      Equal a b = False
    type family Member (a :: k) (b :: '[k]) :: Bool where
      Member a '[] = False                      -- (not overlapping)
      Member a ( a ': bs ) = True
      Member a ( b ': bs ) = Member a bs

Questions of syntax

What should the "header" look like?

(A)      type instance where      -- Use "where"
            F (a,b)   = [Char]
            F (Int,b) = Char
            F Bool    = Char

(B)      type instance of         -- Use "of" (yuk)
            F (a,b)   = [Char]
            F (Int,b) = Char
            F Bool    = Char

(C)      type instance F where     -- Redundantly mention F in the header
            F (a,b)   = [Char]
            F (Int,b) = Char
            F Bool    = Char

We need one of the existing "layout herald" keywords (of, let, where) to smoothly support the nested block of equations. It's not clear whether or not it is useful to mention the name of the function in the header.

Attachments (1)

  • axioms.pdf (212.0 KB) - added by goldfire 5 years ago. Description of FC extension to support overlapping type family instances

Download all attachments as: .zip