max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

docs: touch-up of Lake.Util.Family comments

Browse source
This commit is contained in:
tydeu 2022-07-23 22:07:34 -04:00
parent d68029092a
commit abe8e8b1f8
1 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
Lake/Util/Family.lean
View file

@ -11,11 +11,11 @@ import Lean.Parser.Command
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*](https://doi.org/10.1145/1411204.1411215)
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 checking with open type functions*][1] 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.
@ -27,6 +27,8 @@ 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.
[1]: https://doi.org/10.1145/1411204.1411215
## Defining Families
In this approach, to define an open type family, one first defines an `opaque`
@ -116,15 +118,16 @@ 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
`Name` and defining each mapping using a name literal `name` and the
`Lean.Name` and defining each mapping using a name literal `name` and the
declaration ``axiom Fam.name : Fam `name = α`` thus causing a name clash
if two keys overlap and thereby producing an error.
-/
open Lean
namespace Lake
/-! ## API Documentation -/
/-! ## API -/
/--
Defines a single mapping of the **open type family** `Fam`, namely `Fam a = β`.