Function fungi_lang::normal::normal_type

source · 
pub fn normal_type(ctx: &Ctx, typ: &Type) -> Type
Expand description

Normalize types (expand definitions and reduce applications).

To normalize types, we generally need to expand definitions of user-defined types, and apply them to type or index arguments.

Example:

Suppose the user defines NmOp := foralli X:NmSet. 1 + Nm[X] in the context. Then, NmOp [{@1}] normalizes to 1 + Nm[{@1}], by using the body of the definition of NmOp, and reducing the type-index application.

Reducible forms (not head normal form)

The following type forms are reducible:

  1. user(_) / Ident(_) – user-defined identifiers (each reduces to its definition)
  2. (foralli a:g. A) [i] – type-index application
  3. (forallt a:K. A) B – type-type application

Normal forms (irreducible forms)

The following forms are “normal” (irreducible); they each have intro/elim forms in the core language’s program syntax:

  1. Base types, sums, products
  2. Ref, Thk, Nm, (Nm->Nm)[_],
  3. exists
  4. forallt, foralli
  5. rec
  6. type variables, as introduced by forallt and rec (note: not the same as user-defined type names, which each have a known definition)
  7. type applications in head normal form.