Open Type Families in Lean

This module contains utilities for defining open type families in Lean.

The concept of type families originated in Haskell with the paper Type checking with open type functions by Schrijvers et al. and is essentially just a fancy name for a function from an input index to an output type. However, it tends to imply some additional restrictions on syntax or functionality as opposed to a proper type function.The design here has some such limitations so the name was similarly adopted.

Type families come in two forms: open and closed. A closed type family is an ordinary total function. An open type family, on the other hand, is a partial function that allows additional input to output mappings to be defined as needed.

Lean does not (currently) directly support open type families. However, it does support type class functional dependencies (via outParam), and simple open type families can be modeled through functional dependencies, which is what we do here.

Defining Families

In this approach, to define an open type family, one first defines an opaque type function with a single argument that serves as the key:

opaque FooFam (key : Name) : Type

Note that, unlike Haskell, the key need not be a type. Lean's dependent type theory does not have Haskell's strict separation of types and data and thus we can use data as an index as well.

Then, to add a mapping to this family, one defines an axioms:

axiom FooFam.bar : FooFam `bar = Nat

To finish, one also defines an instance of the FamilyDef type class defined in this module using the axiom like so:

instance : FamilyDef FooFam `bar Nat := ⟨FooFam.bar⟩

This module provides a family_def macro to define both the axiom and the instance in one go like so:

family_def bar : FooFam `bar := Nat

Type Inference

The signature of the type class FamilyDef is

FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : outParam $ Type v) : Prop

The key part being that β is an outParam so Lean's type class synthesis will smartly infer the defined type Nat when given the key of `bar. Thus, if we have a function define like so:

def foo (key : α) [FamilyDef FooFam key β] : β := ...

Lean will smartly infer that the type of foo `bar is Nat.

However, filling in the right hand side of foo is not quite so easy. FooFam `bar = Nat is only true propositionally, so we have to manually cast a Nat to FooFam `barand provide the proof (and the same is true vice versa). Thus, this module provides two definitions, toFamily : β → Fam a and ofFamily : Fam a → β, to help with this conversion.

Full Example

Putting this all together, one can do something like the following:

opaque FooFam (key : Name) : Type

abbrev FooMap := DRBMap Name FooFam Name.quickCmp
def FooMap.insert (self : FooMap) (key : Name) [FamilyDef FooFam key α] (a : α) : FooMap :=
  DRBMap.insert self key (toFamily a)
def FooMap.find? (self : FooMap) (key : Name) [FamilyDef FooFam key α] : Option α :=
  ofFamily <$> DRBMap.find? self key

family_def bar : FooFam `bar := Nat
family_def baz : FooFam `baz := String
def foo := Id.run do
  let mut map : FooMap := {}
  map := map.insert `bar 5
  map := map.insert `baz "str"
  return map.find? `bar

#eval foo -- 5

Type Safety

In order to maintain type safety, a = b → Fam a = Fam b must actually hold. That is, one must not define mappings to two different types with equivalent keys. Since mappings are defined through axioms, Lean WILL NOT catch violations of this rule itself, so extra care must be taken when defining mappings.

In Lake, this is solved by having its open type families be indexed by a Lean.Name and defining each mapping using a name literal name and the declaration axiom Fam.name : Fam `name = α. This causes a name clash if two keys overlap and thereby produces an error.

API

class Lake.FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : semiOutParam (Type v)) : Prop

Defines a single mapping of the open type family Fam, namely Fam a = β. See the module documentation of Lake.Util.Family for details on what an open type family is in Lake.

• family_key_eq_type : Fam a = β

theorem Lake.FamilyDef.family_key_eq_type {α : Type u} {Fam : α → Type v} {a : α} {β : semiOutParam (Type v)} [self : Lake.FamilyDef Fam a β] : Fam a = β

class Lake.FamilyOut {α : Type u} (Fam : α → Type v) (a : α) (β : outParam (Type v)) : Prop

Like FamilyDef, but β is an outParam.

• family_key_eq_type : Fam a = β

@[simp]

theorem Lake.FamilyOut.family_key_eq_type {α : Type u} {Fam : α → Type v} {a : α} {β : outParam (Type v)} [self : Lake.FamilyOut Fam a β] : Fam a = β

instance Lake.instFamilyOutOfFamilyDef : ∀ {α : Type u_1} {Fam : α → Type u_2} {a : α} {β : Type u_2} [inst : Lake.FamilyDef Fam a β], Lake.FamilyOut Fam a β

Equations

• ⋯ = ⋯

instance Lake.instFamilyDef {β : Type u_1} : ∀ {α : Type u_2} {a : α}, Lake.FamilyDef (fun (x : α) => β) a β

The constant type family

Equations

• ⋯ = ⋯

@[macro_inline]

def Lake.toFamily : {α : Type u_1} → {Fam : α → Type u_2} → {a : α} → {β : Type u_2} → [inst : Lake.FamilyOut Fam a β] → β → Fam a

Cast a datum from its individual type to its general family.

Equations

• Lake.toFamily b = cast ⋯ b

@[macro_inline]

def Lake.ofFamily : {α : Type u_1} → {Fam : α → Type u_2} → {a : α} → {β : Type u_2} → [inst : Lake.FamilyOut Fam a β] → Fam a → β

Cast a datum from its general family to its individual type.

Equations

• Lake.ofFamily b = cast ⋯ b

def Lake.familyDef : Lean.ParserDescr

The syntax:

family_def foo : Fam 0 := Nat

Declares a new mapping for the open type family Fam type via the production of an axiom Fam.foo : Data 0 = Nat and an instance of FamilyDef that uses this axiom for key 0.

Equations

• One or more equations did not get rendered due to their size.