@maxdeliso/typed-ski@0.6.0

Built and signed on GitHub Actions

Built and signed on GitHub Actions

Primary hash-consing arena evaluator used throughout the project.

Public function. Converts an untyped lambda expression (UntypedLambda) into an SKI expression.

Creates a Church-encoded numeral from an integer.

Full TripLang pipeline: parse → index → elaborate → resolve → typecheck.

Compiles a single TripLang source string to a TripCObject.

Compiles a single TripLang source string to a serialized .tripc object file.

Returns an empty System F context.

Transforms a well–typed System F term into a simply typed lambda term.

Erases type annotations from a simply typed lambda expression.

Collects all free (external) term and type references appearing inside a TripLang value.

Extracts the value part of a TripLang definition.

The I combinator terminal node.

Builds a symbol table for a TripLang program, ensuring all term and type names are unique.

Runs a simplified version of Algorithm W over the given untyped term. Returns a pair of the typed term and its inferred type.

The K combinator terminal node.

Represents an import declaration in a module.

Parses an input string into an untyped lambda term.

Parses an input string containing an SKI expression into its AST representation.

Parses an input string into a System F term with EOF checking.

Parses a TripLang program source string into a TripLangProgram AST.

Parses an input string into a typed lambda term. Uses parseWithEOF to ensure the entire input is consumed.

A polymorphic (System F) term definition.

Returns the string representation of a SKI expression.

Pretty-prints a System F term using λ for term abstraction and Λ for type abstraction.

Pretty prints a System F type.

Renders a base type as a compact UTF-8 string using ∀ and →.

Pretty-prints a simply typed lambda expression.

Pretty-prints an untyped lambda expression using λ and parentheses.

Resolves all external references across a program using the provided symbol table.

Resolves external references inside a single top-level definition.

Resolves a polymorphic definition by name from a typechecked program.

The S combinator terminal node.

Compilation error specific to the single-file compiler

An SKI expression is either a terminal symbol (S, K, I) or an application node.

Represents a terminal symbol in an SKI expression.

SKI terminal symbol definitions.

A System F term represents expressions in the polymorphic lambda calculus (System F).

Represents the complete object file structure for a compiled TripLang module.

Root AST node for a TripLang program.

A top-level TripLang definition or directive.

Typechecks a System F term. Returns just the type (discarding the final context).

Infers the type of a simply typed lambda calculus term under an empty context.

A simply-typed lambda term definition.

A named base or arrow/forall type definition.

This recursive type represents the legal terms of the simply typed lambda calculus.

Evaluates a Church numeral SKI expression to a JavaScript bigint using the optimized native path.

The union type representing all possible untyped lambda calculus terms. Includes variables, abstractions, and applications.