# 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 `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 (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 #

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 = β

## Instances

## Equations

- ⋯ = ⋯

The constant type family

## Equations

- ⋯ = ⋯

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

## Equations

- Lake.toFamily b = cast ⋯ b

## Instances For

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

## Equations

- Lake.ofFamily b = cast ⋯ b