# Open Type Families in Lean #

This module contains utilities for defining open families in Lean.

The concept of 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, the concept implies some additional restrictions on the syntax and/or functionality versus a proper function. The design here has similar limitations, hence the adaption of the name.

Families come in two forms: open and closed. A closed family is an ordinary total function. An open family is a partial function that allows additional input to output mappings to be defined as needed.

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

## Defining Families #

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

    opaque FooFam (idx : Name) : Type

Note that, unlike Haskell, the index need not be a type. Lean's dependent type theory does not have Haskell's strict separation of types and data, enabling this generalization.

Similarly, the output of a family need not be a type. In such a case, though, the family must be marked `noncomputable`:

    noncomputable opaque fooFam (idx : Name) : Name

To add a mapping to a family, one first defines an axiom:

    axiom FooFam.bar : FooFam `bar = Nat

Then defines an instance of the `FamilyDef` type class using the axiom:

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

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

    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 index part being that `β` is an `outParam` so Lean's type class synthesis will smartly infer the defined type `Nat` when given the index of ``bar`. Thus, if we have a function define like so:

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

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 `bar`and 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 (idx : Name) : Type

    abbrev FooMap := Std.DTreeMap Name FooFam Name.quickCmp
    def FooMap.insert (self : FooMap) (idx : Name) [FamilyOut FooFam idx α] (a : α) : FooMap :=
      Std.DTreeMap.insert self idx (toFamily a)
    def FooMap.get? (self : FooMap) (idx : Name) [FamilyOut FooFam idx α] : Option α :=
      ofFamily <$> Std.DTreeMap.get? self idx

    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.get? `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 indices. 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 indices overlap and thereby produces an error.

## API #

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

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

- fam_eq : f a = b

Instances

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

Like `FamilyDef`, but `b` is an `outParam`.

- fam_eq : f a = b

Instances

source
instance Lake.instFamilyOutOfFamilyDef {α✝ : Type u_1} {β✝ : Type u_2} {f : α✝ → β✝} {a : α✝} {b : β✝} [FamilyDef f a b] :
FamilyOut f a b
source
@[instance 0, defaultInstance 0]
instance Lake.instFamilyDef {α✝ : Type u_1} {β✝ : Type u_2} {f : α✝ → β✝} {a : α✝} :
FamilyDef f a (f a)

The identity relation.

source
instance Lake.instFamilyDef_1 {β✝ : Type u_1} {b : β✝} {α✝ : Type u_2} {a : α✝} :
FamilyDef (fun (x : α✝) => b) a b

The constant type family.

source
@[macro_inline]
def Lake.toFamily {α✝ : Type u_1} {F : α✝ → Sort u_2} {a : α✝} {β : Sort u_2} [FamilyOut F a β] (b : β) :
F a

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

Equations

- Lake.toFamily b = cast ⋯ b

Instances For

source
@[macro_inline]
def Lake.ofFamily {α✝ : Type u_1} {F : α✝ → Sort u_2} {a : α✝} {β : Sort u_2} [FamilyOut F a β] (b : F a) :
β

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

Equations

- Lake.ofFamily b = cast ⋯ b

Instances For

source
def Lake.familyDef :
Lean.ParserDescr

The syntax:

    family_def foo : Fam 0 := Nat

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

Equations

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

Instances For