Terms and Types

Terms and Types

Mathematical Objects

We implement (homotopy) type theory foundations in scala. Thus,

• essentially all mathematical objects are terms.
• each term has a type, usually unique.
• types are themselves terms.

In scala terms, these translate to:

• a trait Term
• a trait Typ extending term (with an additional type parameter as we see later).
• an abstract method typ in the trait Term, giving the type.

Rules

Foundations specify certain kinds, of rules, namely,

• formation rules for terms (including types).
• determining the type of a term.
• determining when two terms are definitionally equal.
• (for non-closed terms) result of substituting a term for another of the same type in a given term.

In scala, these are implemented as

• (case) classes for forming terms and types.
• implementations of the typ method.
• the equality method -- overridden in some cases.
• a method subs for terms, inherited from a trait Subs.

Refined types

• There are some refinements to the traits and their sub-classes. These are so that the scala type (which is seen by the compiler) has some information of the underlying HoTT type of terms - which a priori are just given by the typ method, and so are purely at runtime.

• Specifically, we have types corresponding to (among others)

  • (dependent) functions: as scala functions
  • types: as a scala trait.
  • pairs: as a scala trait, which relates these to scala pairs.
  • recursive combinations of these.

• Dually, the trait Typ, actually Typ[+U <: Term] has

  • a type parameter U giving an upper bound on terms having this HoTT typ.
  • an inner typ Obj in general refining U.

Scala Representations

For efficiency, many terms can be represented as scala objects. Formally these are additional constants.