Function fungi_lang::bitype::normal_type
[−]
[src]
pub fn normal_type(ctx: &Ctx, typ: &Type) -> Type
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:
user(_)
/Ident(_)
-- user-defined identifiers (each reduces to its definition)(foralli a:g. A) [i]
-- type-index application(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:
- Base types, sums, products
Ref
,Thk
,Nm
,(Nm->Nm)[_]
,exists
forallt
,foralli
rec
- type variables, as introduced by
forallt
andrec
(note: not the same as user-defined type names, which each have a known definition) - type applications in head normal form.