check

package
v1.7.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Jan 5, 2026 License: MIT Imports: 7 Imported by: 0

Documentation

Overview

Package check implements bidirectional type checking for the HoTT kernel.

This package is part of the trusted kernel and provides the core type checking algorithm. It uses bidirectional typing with synthesis and checking modes to infer and verify types of terms.

Checker

The Checker type performs type checking against a GlobalEnv: 

globals := check.NewGlobalEnv()
globals.AddAxiom("Nat", ast.Sort{U: 0})
checker := check.NewChecker(globals)

Create checkers with different configurations:

Bidirectional Type Checking

The algorithm operates in two modes:

Synthesis (Synth): infers the type of a term from its structure. Works for variables, globals, applications, projections, sorts. 

ty, err := checker.Synth(ctx, span, term)

Checking (Check): verifies a term has an expected type. Works for lambdas, pairs, and terms that can also be synthesized. 

err := checker.Check(ctx, span, term, expectedType)

Type Errors

Type checking failures return *TypeError with:

  • Span - source location for error reporting
  • Kind - ErrorKind for programmatic handling
  • Message - human-readable description
  • Details - ErrorDetails with structured information

Error kinds include:

Global Environment

GlobalEnv stores global declarations:

  • Axiom - uninterpreted type declarations
  • Definition - defined constants with body
  • Inductive - inductive type families with constructors
  • Primitive - built-in operations

Definitions have Transparency controlling unfolding:

Cubical Features

The checker supports cubical type theory with interval context tracking:

Cubical terms (paths, transport, composition) are checked via bidir_cubical.go.

Inductive Types

Inductive types are checked for strict positivity to ensure consistency. The eliminator (recursor) type is automatically derived. See:

  • GlobalEnv.AddInductive - register inductive type
  • positivity.go - strict positivity checking
  • recursor.go - eliminator type synthesis

Definitional Equality

Type checking uses NbE-based conversion checking from internal/core:

  • Terms are normalized to weak head normal form
  • Normalized terms are compared structurally
  • Optional η-rules for functions and pairs

Package check implements bidirectional type checking for the HoTT kernel.

Bidirectional type checking uses two modes:

  • Synthesis (Synth): infer the type of a term
  • Checking (Check): verify a term has an expected type

This approach provides better error messages by tracking source positions and reduces the annotation burden by propagating type information.

References:

  • Dunfield, J. and Krishnaswami, N. "Bidirectional Typing"
  • Löh, A. et al. "A Tutorial Implementation of a Dependently Typed Lambda Calculus"

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func CheckMutualPositivity added in v1.6.0 

func CheckMutualPositivity(indNames []string, constructors map[string][]Constructor) error

CheckMutualPositivity verifies that mutually recursive inductive types satisfy the strict positivity condition across all types in the mutual block.

For mutual inductives, each type must occur strictly positively in the constructors of ALL types in the mutual block. That is: - For each type T in the mutual block - For each constructor C of any type in the block - T must occur only in strictly positive positions in C

func CheckPositivity 

func CheckPositivity(indName string, constructors []Constructor) error

CheckPositivity verifies that a single inductive type definition satisfies the strict positivity condition. This ensures the inductive is well-founded and prevents logical inconsistencies.

A type T occurs strictly positively in X if: - X does not mention T, OR - X = T (the type itself), OR - X = (a : A) -> B where T does NOT occur in A and occurs strictly positively in B

func GenerateHITRecursorType added in v1.7.0 

func GenerateHITRecursorType(ind *Inductive) ast.Term

GenerateHITRecursorType generates the eliminator type for a HIT. For Circle (S1) with base and loop: 

S1-elim : (P : S1 -> Type)
        -> (pbase : P base)
        -> (ploop : PathP (λi. P (loop @ i)) pbase pbase)
        -> (x : S1) -> P x

The key difference from regular inductives is that path constructors require PathP cases rather than simple function cases.

func GenerateRecursorType 

func GenerateRecursorType(ind *Inductive) ast.Term

GenerateRecursorType generates the type of the eliminator for an inductive type.

For an inductive T with constructors c1, ..., cn, the recursor has type: 

T-elim : (P : T -> Type_j) -> case(c1) -> ... -> case(cn) -> (t : T) -> P t

For parameterized inductives like List : Type -> Type: 

listElim : (A : Type) -> (P : List A -> Type) -> case_nil -> case_cons -> (xs : List A) -> P xs

For indexed inductives like Vec : Type -> Nat -> Type: 

vecElim : (A : Type) -> (P : (n : Nat) -> Vec A n -> Type) ->
          case_vnil -> case_vcons -> (n : Nat) -> (xs : Vec A n) -> P n xs

where case(ci) provides the elimination principle for constructor ci:

  • Non-recursive args pass through as-is
  • Recursive args (of type T) get an induction hypothesis (ih : P indices arg)

The universe j for the motive is derived from the inductive's type.

func GenerateRecursorTypeSimple 

func GenerateRecursorTypeSimple(ind *Inductive) ast.Term

GenerateRecursorTypeSimple generates a recursor (eliminator) type for an inductive definition.

A recursor encodes the induction principle for an inductive type, allowing dependent elimination (proving properties) and recursion (defining functions). The generated type has the form: 

elimT : (P : T → Type) → case₁ → ... → caseₙ → (t : T) → P t

where each caseᵢ corresponds to a constructor with appropriate induction hypotheses for recursive arguments.

For example, the recursor for Nat (with zero and succ) has type: 

natElim : (P : Nat → Type)
        → P zero                           ; base case
        → ((n : Nat) → P n → P (succ n))   ; step case with IH
        → (n : Nat) → P n

This function provides hand-crafted types for common inductives (Nat, Bool) for clarity and correctness, falling back to GenerateRecursorType for other inductives.

See also: GenerateRecursorType for the general algorithm handling indexed types.

func IsRecursiveArg 

func IsRecursiveArg(indName string, argType ast.Term) bool

IsRecursiveArg checks if a constructor argument type contains a reference to the inductive type being defined.

This function is used during recursor generation to identify which constructor arguments are recursive. Recursive arguments require induction hypotheses (IH) in the recursor's case types.

For example, given: 

Nat : Type
zero : Nat
succ : Nat → Nat

In the succ constructor, the Nat argument is recursive (IsRecursiveArg returns true), so natElim's step case has type (n : Nat) → P n → P (succ n), where P n is the IH.

Non-recursive arguments (like the A parameter in cons : A → List A → List A) simply pass through to the case type without generating an IH.

func OccursIn 

func OccursIn(name string, ty ast.Term) bool

OccursIn checks if a global name occurs anywhere in a term.

This function performs a recursive traversal of the term structure to determine whether the specified global name appears. It is used during strict positivity checking to detect occurrences of the inductive type being defined, and by IsRecursiveArg to identify recursive constructor arguments.

The function conservatively returns false for unknown term types, which is safe because the positivity checker will catch unknown types separately.

Example: For an inductive type List with constructor cons : A → List A → List A, OccursIn("List", consType) returns true because List appears in the argument type.

Types

type Axiom 

type Axiom struct {
	Name string
	Type ast.Term
}

Axiom represents a postulated constant with only a type.

type CannotInferDetails 

type CannotInferDetails struct {
	Term ast.Term
}

CannotInferDetails provides information about terms whose type cannot be inferred.

type Checker 

type Checker struct {
	// contains filtered or unexported fields
}

Checker performs bidirectional type checking.

func NewChecker 

func NewChecker(globals *GlobalEnv) *Checker

NewChecker creates a new type checker with the given global environment.

func NewCheckerWithEta 

func NewCheckerWithEta(globals *GlobalEnv) *Checker

NewCheckerWithEta creates a checker with eta-equality enabled.

func NewCheckerWithPrimitives 

func NewCheckerWithPrimitives() *Checker

NewCheckerWithPrimitives creates a checker with built-in Nat and Bool types.

func (*Checker) Check 

func (c *Checker) Check(ctx *tyctx.Ctx, span Span, term ast.Term, expected ast.Term) *TypeError

Check verifies that a term has the expected type. Returns nil on success. If ctx is nil, an empty context is used.

func (*Checker) CheckIVar 

func (c *Checker) CheckIVar(ix int) bool

CheckIVar validates an interval variable index against the current context. Returns true if valid, false if invalid or outside a path context.

func (*Checker) CheckIsType 

func (c *Checker) CheckIsType(ctx *tyctx.Ctx, span Span, term ast.Term) (ast.Level, *TypeError)

CheckIsType verifies that a term is a well-formed type. Returns the universe level and nil error on success. If ctx is nil, an empty context is used.

func (*Checker) Globals 

func (c *Checker) Globals() *GlobalEnv

Globals returns the global environment.

func (*Checker) ICtxDepth 

func (c *Checker) ICtxDepth() int

ICtxDepth returns the current interval context depth (0 if not tracking).

func (*Checker) InferAndCheck 

func (c *Checker) InferAndCheck(ctx *tyctx.Ctx, span Span, term ast.Term, expected ast.Term) *TypeError

InferAndCheck is a convenience that synthesizes a type and checks it against expected. If ctx is nil, an empty context is used.

func (*Checker) PushIVar 

func (c *Checker) PushIVar() func()

PushIVar extends the interval context by one and returns a cleanup function. Call the returned function when leaving the scope (via defer).

func (*Checker) Synth 

func (c *Checker) Synth(ctx *tyctx.Ctx, span Span, term ast.Term) (ast.Term, *TypeError)

Synth synthesizes (infers) the type of a term. Returns the inferred type and nil error on success. If ctx is nil, an empty context is used.

type Constructor 

type Constructor struct {
	Name string
	Type ast.Term
}

Constructor represents an inductive type constructor.

type ConstructorError 

type ConstructorError struct {
	IndName     string
	Constructor string
	Message     string
}

ConstructorError represents an error in constructor validation.

func (*ConstructorError) Error 

func (e *ConstructorError) Error() string

type Definition 

type Definition struct {
	Name         string
	Type         ast.Term
	Body         ast.Term
	Transparency Transparency
}

Definition represents a defined constant with type and body.

type ErrorDetails 

type ErrorDetails interface {
	// contains filtered or unexported methods
}

ErrorDetails provides additional context for specific error kinds.

type ErrorKind 

type ErrorKind int

ErrorKind categorizes type errors for programmatic handling. 

const (
	ErrUnboundVariable ErrorKind = iota
	ErrTypeMismatch
	ErrNotAFunction
	ErrNotAPair
	ErrNotAType
	ErrUnknownGlobal
	ErrCannotInfer
	ErrOccursCheck
)

func (ErrorKind) String 

func (k ErrorKind) String() string

String returns the error kind name.

type GlobalEnv 

type GlobalEnv struct {
	// contains filtered or unexported fields
}

GlobalEnv holds all global declarations in dependency order.

func NewGlobalEnv 

func NewGlobalEnv() *GlobalEnv

NewGlobalEnv creates an empty global environment.

func NewGlobalEnvWithPrimitives 

func NewGlobalEnvWithPrimitives() *GlobalEnv

NewGlobalEnvWithPrimitives creates a global environment with Nat and Bool.

func (*GlobalEnv) AddAxiom 

func (g *GlobalEnv) AddAxiom(name string, ty ast.Term)

AddAxiom adds an axiom to the environment.

func (*GlobalEnv) AddDefinition 

func (g *GlobalEnv) AddDefinition(name string, ty, body ast.Term, trans Transparency)

AddDefinition adds a definition to the environment.

func (*GlobalEnv) AddHITs added in v1.7.0 

func (g *GlobalEnv) AddHITs()

AddHITs adds built-in Higher Inductive Types to the environment. These include: - S1 (Circle): base point and loop path - Trunc (Propositional Truncation): inc and squash - Susp (Suspension): north, south, and merid - Int (Integers): pos, neg, and zeroPath - Quot (Set Quotient): quot and eq

func (*GlobalEnv) AddInductive 

func (g *GlobalEnv) AddInductive(name string, ty ast.Term, numParams int, paramTypes []ast.Term, numIndices int, indexTypes []ast.Term, constrs []Constructor, elim string, mutualGroup []string)

AddInductive adds an inductive type to the environment without validation. For validated addition, use DeclareInductive or DeclareMutual.

func (*GlobalEnv) DeclareHIT added in v1.7.0 

func (g *GlobalEnv) DeclareHIT(spec *ast.HITSpec) error

DeclareHIT validates and registers a Higher Inductive Type. It validates: - The inductive type signature is well-formed - All point constructors are well-formed and return the HIT type - All path constructors are well-formed with proper boundaries - Strict positivity is satisfied for both point and path constructors It also generates and registers the eliminator with path cases.

func (*GlobalEnv) DeclareInductive 

func (g *GlobalEnv) DeclareInductive(name string, ty ast.Term, constrs []Constructor, elim string) error

DeclareInductive validates and adds a single inductive type to the environment. This is a convenience wrapper around DeclareMutual for non-mutual inductives.

func (*GlobalEnv) DeclareMutual added in v1.6.0 

func (g *GlobalEnv) DeclareMutual(specs []MutualInductiveSpec) error

DeclareMutual validates and adds mutually recursive inductive types. For a single inductive, use DeclareInductive for convenience.

It checks: - Each inductive type is well-formed (Sort or Pi chain ending in Sort) - Each constructor type is well-formed (can reference any type in the mutual block) - Each constructor returns its inductive type applied to params/indices - The definition satisfies strict positivity across all mutual types It also generates and registers eliminators for each type.

func (*GlobalEnv) Has 

func (g *GlobalEnv) Has(name string) bool

Has returns true if the name is defined in the environment.

func (*GlobalEnv) LookupDefinitionBody 

func (g *GlobalEnv) LookupDefinitionBody(name string) (ast.Term, bool)

LookupDefinitionBody returns the body of a definition if transparent.

func (*GlobalEnv) LookupType 

func (g *GlobalEnv) LookupType(name string) ast.Term

LookupType returns the type of a global name, or nil if not found.

func (*GlobalEnv) Order 

func (g *GlobalEnv) Order() []string

Order returns the declaration order.

type ICtx added in v1.6.0 

type ICtx struct {
	// contains filtered or unexported fields
}

ICtx tracks interval variable bindings for cubical type checking. Interval variables are tracked separately from term variables.

func NewICtx added in v1.6.0 

func NewICtx() *ICtx

NewICtx creates an empty interval context.

func (*ICtx) CheckIVar added in v1.6.0 

func (ic *ICtx) CheckIVar(ix int) bool

CheckIVar checks if an interval variable index is valid.

func (*ICtx) Extend added in v1.6.0 

func (ic *ICtx) Extend() *ICtx

Extend adds an interval binding and returns the new context.

type Inductive 

type Inductive struct {
	Name         string
	Type         ast.Term
	NumParams    int        // Number of parameters (uniform across constructors)
	ParamTypes   []ast.Term // Types of each parameter
	NumIndices   int        // Number of indices (vary per constructor)
	IndexTypes   []ast.Term // Types of each index (under param binders)
	Constructors []Constructor
	Eliminator   string   // Name of the elimination principle
	MutualGroup  []string // Names of other types in mutual block (nil for single inductives)

	// HIT-specific fields (for Higher Inductive Types)
	PathCtors []ast.PathConstructor // Path constructors (level >= 1)
	IsHIT     bool                  // True if has path constructors
	MaxLevel  int                   // Highest constructor level (1 = paths, 2 = paths of paths, etc.)
}

Inductive represents an inductive type definition.

type InductiveError 

type InductiveError struct {
	IndName string
	Message string
}

InductiveError represents an error in inductive type validation.

func (*InductiveError) Error 

func (e *InductiveError) Error() string

type MutualInductiveSpec added in v1.6.0 

type MutualInductiveSpec struct {
	Name         string
	Type         ast.Term
	Constructors []Constructor
	Eliminator   string
}

MutualInductiveSpec specifies one inductive type in a mutual block.

type NotAFunctionDetails 

type NotAFunctionDetails struct {
	Actual ast.Term
}

NotAFunctionDetails provides information when a non-function is applied.

type NotAPairDetails 

type NotAPairDetails struct {
	Actual ast.Term
}

NotAPairDetails provides information when projecting from a non-pair.

type NotATypeDetails 

type NotATypeDetails struct {
	Actual ast.Term
}

NotATypeDetails provides information when a type was expected.

type PathConstructorError added in v1.7.0 

type PathConstructorError struct {
	IndName     string
	Constructor string
	Message     string
}

PathConstructorError represents an error in path constructor validation.

func (*PathConstructorError) Error added in v1.7.0 

func (e *PathConstructorError) Error() string

type PiArg 

type PiArg struct {
	Name string
	Type ast.Term
}

PiArg represents a single argument in a Pi type chain.

type Polarity 

type Polarity int

Polarity tracks whether we're in a positive or negative position. 

const (
	Positive Polarity = iota
	Negative
)

func (Polarity) Flip 

func (p Polarity) Flip() Polarity

Flip returns the opposite polarity.

func (Polarity) String 

func (p Polarity) String() string

type Pos 

type Pos struct {
	Line   int // 1-indexed line number
	Column int // 1-indexed column number
	Offset int // 0-indexed byte offset
}

Pos represents a position in source code.

type PositivityError 

type PositivityError struct {
	IndName     string
	Constructor string
	Position    string
	Polarity    Polarity
}

PositivityError represents a strict positivity violation.

func (*PositivityError) Error 

func (e *PositivityError) Error() string

type Primitive 

type Primitive struct {
	Name string
	Type ast.Term
}

Primitive represents a built-in type with special evaluation rules.

type Span 

type Span struct {
	File  string // Source file name (empty for REPL/tests)
	Start Pos
	End   Pos
}

Span represents a range in source code.

func NewSpan 

func NewSpan(file string, startLine, startCol, endLine, endCol int) Span

NewSpan creates a span from start and end positions.

func NoSpan 

func NoSpan() Span

NoSpan returns an empty span for generated terms or tests.

func (Span) IsEmpty 

func (s Span) IsEmpty() bool

IsEmpty returns true if this is a zero-value span.

func (Span) String 

func (s Span) String() string

String returns a human-readable representation of the span.

type Transparency 

type Transparency int

Transparency controls whether a definition can be unfolded during conversion. 

const (
	Opaque      Transparency = iota // Never unfold
	Transparent                     // Always unfold during conversion
)

type TypeError 

type TypeError struct {
	Span    Span
	Kind    ErrorKind
	Message string
	Details ErrorDetails
}

TypeError represents a type checking error with location and details.

func (*TypeError) Error 

func (e *TypeError) Error() string

Error implements the error interface.

type TypeMismatchDetails 

type TypeMismatchDetails struct {
	Expected ast.Term
	Actual   ast.Term
}

TypeMismatchDetails provides information about type mismatches.

type UnboundVariableDetails 

type UnboundVariableDetails struct {
	Index int
}

UnboundVariableDetails provides information about unbound variables.

type UnknownGlobalDetails 

type UnknownGlobalDetails struct {
	Name string
}

UnknownGlobalDetails provides information about unknown global names.

type ValidationError 

type ValidationError struct {
	Msg string
}

ValidationError represents a validation error during inductive declaration.

func (*ValidationError) Error 

func (e *ValidationError) Error() string

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.