check

package
v1.6.0 Latest Latest
Warning

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

 Go to latest Published: Dec 8, 2025 License: MIT Imports: 6 Imported by: 0

Documentation

Overview

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 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 simpler recursor type without complex index manipulation. This is an alternative implementation that's easier to understand but may have subtle bugs.

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.

func OccursIn 

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

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

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) 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) 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)
}

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 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.