🥮 mooncakes.io
README

#Types

The HOL type language. Types form the simply-typed layer that classifies every term in the system.

Depends on: foundation (for Subst)

#The Type Enum

///|
enum Type {
  TyVar(String) // type variable: enables polymorphism
  TyApp(String, Array[Type]) // type constructor applied to arguments
}

  • TyVar("'a") is a type variable -- polymorphic constants like equality are parameterized over these.
  • TyApp("bool", []) is the Boolean type (propositions).
  • TyApp("fun", [A, B]) is the function type A -> B.
  • TyApp("list", [A]) would be A list (once registered with new_type).

#Type Registry

The set of valid type constructors and their arities lives in a mutable registry (type_table). Initially it contains two primitives:

ConstructorArityMeaning
bool0propositions
ind0individuals (needed for the axiom of infinity)

The function type constructor fun is built-in (hardcoded arity 2) and does not appear in the registry.

mk_type enforces arities: you cannot write TyApp("bool", [x]) because bool was registered with arity 0.

///|
test "types: basic construction and pretty-printing" {
  @types.Type::reset_table()
  let bool_ty = @types.bool_ty()
  let a = @types.mk_var("'a")
  let b = @types.mk_var("'b")
  assert_eq(@types.Type::pprint(bool_ty), "bool")
  assert_eq(@types.Type::pprint(a), "'a")
  assert_true(a.is_var())
  assert_false(bool_ty.is_var())

  // Function types: 'a -> 'b
  let fun_ty = @types.mk_fun(a, b)
  assert_eq(@types.Type::pprint(fun_ty), "'a --> 'b")
  assert_true(fun_ty.is_fun())
  let (dom, rng) = fun_ty.dest_fun()
  assert_true(dom == a)
  assert_true(rng == b)
}

#Registering New Type Constructors

new_type(name, arity) extends the registry. checkpoint_defs / reset_table support snapshot/rollback for tests:

///|
test "types: registering a new type constructor" {
  @types.Type::reset_table()
  @types.Type::new_type("list", 1)
  let a = @types.mk_var("'a")
  let list_a = @types.Type::mk_type("list", [a])
  assert_eq(@types.Type::pprint(list_a), "'a list")
}

#Type Substitution

ty.subst(sigma) replaces type variables according to the substitution sigma. This is how polymorphic constants get specialized (e.g., = : 'a -> 'a -> bool becomes = : nat -> nat -> bool).

///|
test "types: substitution replaces type variables" {
  @types.Type::reset_table()
  @types.Type::new_type("list", 1)
  let a = @types.mk_var("'a")
  let b = @types.mk_var("'b")
  let list_a = @types.Type::mk_type("list", [a])

  // Substitute 'a := bool
  let sigma : @types.TypeSubst = Subst(pairs=[(a, @types.bool_ty())])
  assert_eq(@types.Type::pprint(list_a.subst(sigma)), "bool list")

  // Substitute in a function type
  let sigma2 : @types.TypeSubst = Subst(pairs=[
    (a, @types.bool_ty()),
    (b, @types.ind_ty()),
  ])
  assert_eq(
    @types.Type::pprint(@types.mk_fun(a, b).subst(sigma2)),
    "bool --> ind",
  )
}

#Type Matching

Type::match_type(pattern, observation, state) finds a substitution S such that subst(S, pattern) == observation. The state carries (S, ids) where ids is the set of type variables bound to themselves (identity bindings).

The algorithm walks the pattern and observation in lockstep:
  • TyVar vs anything: bind or check consistency
  • TyApp(c, args) vs TyApp(c, args): recurse into children
  • Mismatch: abort

///|
test "types: matching finds a substitution" {
  @types.Type::reset_table()
  let a = @types.mk_var("'a")
  let bool_ty = @types.bool_ty()

  let empty_state : @types.TypeMatchState = { subst: Subst(), tyvars: [] }

  // Match 'a against bool  =>  { 'a := bool }
  let s = a.match_type(bool_ty, empty_state).subst
  assert_true(s.lookup(a) == Some(bool_ty))

  // Match ('a -> 'a) against (bool -> bool)  =>  { 'a := bool }
  let s2 = @types.mk_fun(a, a).match_type(
      @types.mk_fun(bool_ty, bool_ty),
      empty_state,
    ).subst
  assert_true(s2.lookup(a) == Some(bool_ty))

  // Match ('a -> 'b) -> 'c against (bool -> bool) -> ind
  // Tests that the observation tail (rest_obs) is tracked independently of
  // the pattern tail (rest_pats) when recursing into nested App children.
  let b = @types.mk_var("'b")
  let c = @types.mk_var("'c")
  let ind_ty = @types.ind_ty()
  let pat = @types.mk_fun(@types.mk_fun(a, b), c)
  let ob = @types.mk_fun(@types.mk_fun(bool_ty, bool_ty), ind_ty)
  let s3 = pat.match_type(ob, empty_state).subst
  assert_true(s3.lookup(a) == Some(bool_ty))
  assert_true(s3.lookup(b) == Some(bool_ty))
  assert_true(s3.lookup(c) == Some(ind_ty))
}

#Collecting Type Variables

Type::vars_in(ty) returns all type variables occurring in ty, sorted and deduplicated. Used by defineTypeOp to determine how many type parameters a new type operator needs.

///|
test "types: vars_in collects type variables" {
  @types.Type::reset_table()
  let a = @types.mk_var("'a")
  let b = @types.mk_var("'b")
  let fun_ty = @types.mk_fun(a, @types.mk_fun(b, a))
  let vars = @types.Type::vars_in(fun_ty)
  // Should contain exactly 'a and 'b (sorted, deduplicated)
  assert_eq(vars.length(), 2)
}

#Type Aliases

AliasExpands to
TypeSubstSubst[Type, Type]
TypeMatchState{ subst: TypeSubst, tyvars: Array[Type] }

#
Env

source

Type-constructor environment mapping names to their arities.

#
TypeSubst

source

A substitution mapping type variables to types.

#
Type

source
pub enum Type {
  TyVar(String)
  TyApp(String, Array[Type])
} derive(Compare, Eq, 
Debug)

HOL types: a simply-typed lambda calculus type language with type variables (Var) and type constructor applications (App).
impl Show for Type

#
Type::checkpoint_defs

source
fn Type::checkpoint_defs() -> Unit

Save the current type table as a checkpoint for later restoration via reset_table.

#
Type::dest_fun

source
fn Type::dest_fun(self : Type) -> (Type, Type)

Decompose a function type into its domain and range; aborts on non-function types.

#
Type::dest_type

source
fn Type::dest_type(self : Type) -> (String, Array[Type])

Decompose a type constructor application into its name and arguments; aborts on a type variable.

#
Type::dest_var

source
fn Type::dest_var(self : Type) -> String

Extract the name from a type variable; aborts on a type constructor application.

#
Type::domain

source
fn Type::domain(self : Type) -> Type

Extract the domain (argument type) of a function type; aborts on non-function types.

#
Type::is_fun

source
fn Type::is_fun(self : Type) -> Bool

Return true if this type is a function type (App("fun", [_, _])).

#
Type::is_type

source
fn Type::is_type(self : Type) -> Bool

Return true if this type is a constructor application (App).

#
Type::is_var

source
fn Type::is_var(self : Type) -> Bool

Return true if this type is a type variable (Var).

#
Type::match_type

source
fn Type::match_type(self : Type, ob : Type, state : TypeMatchState) -> TypeMatchState raise

Match self as a pattern against ob, extending state with bindings so that applying the resulting substitution to the pattern yields ob.

#
Type::mk_type

source
fn Type::mk_type(name : String, args : Array[Type]) -> Type

Construct a type constructor application, checking that the argument count matches the registered arity.

#
Type::new_type

source
fn Type::new_type(name : String, arity : Int) -> Unit

Register a new type constructor with the given name and arity in the global type table.

#
Type::pprint

source
fn Type::pprint(self : Type) -> String

Pretty-print the type using conventional mathematical notation (e.g., 'a --> bool).

#
Type::range

source
fn Type::range(self : Type) -> Type

Extract the range (return type) of a function type; aborts on non-function types.

#
Type::reset_table

source
fn Type::reset_table() -> Unit

Reset the type table to its last checkpointed state.

#
Type::serialize

source
fn Type::serialize(self : Type) -> String

Serialize the type into a human-readable string representation that mirrors the AST structure.

#
Type::subst

source

Apply a type substitution, replacing type variables according to the given mapping.

#
Type::vars_in

source
fn Type::vars_in(self : Type) -> Array[Type]

Collect all type variables occurring in this type, sorted and deduplicated.

#
TypeMatchState

source
pub(all) struct TypeMatchState {
  subst : 
Subst[Type, Type]
  tyvars : Array[Type]
}

The state carried during type matching: a pair of the current substitution and the list of identity-bound type variables.

#
bool_ty

source
fn bool_ty() -> Type

Return the built-in Boolean type (TyApp("bool", [])).

#
ind_ty

source
fn ind_ty() -> Type

Return the built-in individual type (App("ind", [])), used for the axiom of infinity.

#
mk_fun

source
fn mk_fun(t1 : Type, t2 : Type) -> Type

Construct the function type t1 -> t2 (i.e., App("fun", [t1, t2])).

#
mk_var

source
fn mk_var(name : String) -> Type

Construct a type variable from a name (e.g., Var("'a")).

Source Files

Powered by MoonBit

Site sourceReport issuePackagesBuild queueSkillsStatistics

© 2026 mooncakes.io