How the typeExpr Macro Constructs Lambda-Calculus Type Expressions from Scala Types

The typeExpr macro uses compile-time Scala reflection to recursively decompose arbitrary Scala types into an algebraic TypeExpr AST, mapping functions to implications, case classes to named conjunctions, and sealed traits to disjunctions.

The typeExpr macro serves as the primary bridge between Scala's native type system and the Curry-Howard theorem prover in the chymyst/curryhoward library. By transforming Scala types into lambda-calculus type expressions at compile time, it enables automatic synthesis of Scala code that satisfies given type signatures. This article examines the complete implementation path from the public API through the macro expansion logic in Macros.scala.

Macro Entry Point and Public API

In src/main/scala/io/chymyst/ch/package.scala (lines 108‑110), the typeExpr method is declared as a whitebox macro:

def typeExpr[U]: TypeExpr = macro Macros.typeExprImpl[U]

When the compiler encounters typeExpr[T], it triggers macro expansion by invoking Macros.typeExprImpl[T]. This entry point captures the compile-time type T and initiates the translation process.

Core Implementation in Macros.scala

The heavy lifting occurs in src/main/scala/io/chymyst/ch/Macros.scala. The typeExprImpl method (lines 37‑46) obtains the compile-time type representation and delegates structural analysis to buildTypeExpr:

def typeExprImpl[T: c.WeakTypeTag]: c.Expr[TypeExpr] = {
  val typeT: c.Type = c.weakTypeOf[T]
  val s1 = buildTypeExpr(typeT)
  import LiftedAST._
  c.Expr[TypeExpr](q"$s1")
}

Here, c.WeakTypeTag allows the macro to work with types that may contain unresolved type parameters. The buildTypeExpr method returns a TypeExpr tree, which LiftedAST lifts via quasiquotes (q"$s1") to produce a literal value in the generated code.

The buildTypeExpr Translation Algorithm

The private buildTypeExpr method (lines 63‑71 and 85‑124 in Macros.scala) recursively walks the Scala type structure. It accepts three parameters: the givenType being analyzed, a tMap sequence for type parameter substitution, and a typesSeen set to detect recursive references.

The algorithm first dealiases the type and extracts its symbol name and type arguments. It then pattern-matches on the type name to construct the appropriate TypeExpr node.

Mapping Scala Constructs to TypeExpr Nodes

Scala construct	λ‑calculus representation (TypeExpr)
A => B (function)	ConjunctT(A) ->: B (implication)
((A,B) => C) (arity > 1)	ConjunctT(A,B) ->: C
Primitive (e.g., Int)	BasicT("Int")
Unit	UnitT("Unit")
Nothing	NothingT("Nothing")
Type parameter X	TP("X")
Recursive reference	RecurseT(name, args)
Case class	NamedConjunctT(constructor, tParams, accessors, wrapped)
Sealed trait with case subclasses	DisjunctT(constructor, tParams, parts)
General constructor (e.g., Seq[Int])	ConstructorT("Seq", List(BasicT("Int")))

Handling Function Types

For single-argument functions, the macro creates a direct implication using the #-> (or ->:) operator:

case "scala.Function1" | "Function1" ⇒ matchedTypeArgs.head ->: matchedTypeArgs(1)

For higher arities (Function2 through Function22), the macro groups the first N‑1 arguments into a ConjunctT and forms an implication to the result type:

case name if name matches "(scala\\.)?Function[1-9][0-9]*" ⇒
  ConjunctT(matchedTypeArgs.slice(0, matchedTypeArgs.length - 1)) ->: matchedTypeArgs.last

This encoding mirrors the standard λ‑calculus currying of multi-argument functions.

Primitive and Built-in Types

Primitive types map to atomic TypeExpr nodes:

• Any → BasicT("_")
• Nothing → NothingT("Nothing")
• Unit → UnitT("Unit")

Type Parameters

Unapplied type variables (where matchedTypeArgs.isEmpty and the base class is Any) become TP nodes representing type parameters in the λ‑calculus encoding.

Recursive Type References

The typesSeen set tracks type names during recursion. When a type name reappears in typesSeen, the macro emits a RecurseT(name, args) node to prevent infinite loops while preserving the recursive structure.

Case Classes and Case Objects

For case objects, the macro generates a NamedConjunctT with empty accessor lists:

NamedConjunctT(typeName, Nil, Nil, Nil)

For case classes, it inspects finalType.decls to find case accessors, building a NamedConjunctT with the constructor name, type parameters, accessor names, and their resolved TypeExpr types. It applies TypeExpr.substNames using the typeMap to resolve generic fields.

Sealed Traits and Sum Types

When processing a sealed trait with case subclasses, the macro constructs a DisjunctT. It retrieves knownDirectSubclasses, sorts them alphabetically, and recursively builds TypeExpr nodes for each. If subclasses have type parameters, the macro substitutes them with arguments from the parent trait to ensure consistency.

Generic Type Constructors

Types like Seq[Int] or Either[A, B] that do not match specific algebraic patterns become ConstructorT(name, args). These are treated as opaque atomic constructors during proof search.

TypeExpr AST Definitions

The resulting trees conform to the algebraic data type defined in src/main/scala/io/chymyst/ch/TypeExpr.scala. Key nodes include:

• Atomic types: BasicT, UnitT, NothingT
• Type parameters: TP
• Products: ConjunctT for conjunctions
• Functions: #-> (implication) for arrows
• Named products: NamedConjunctT for case classes
• Sums: DisjunctT for sealed traits
• Recursion: RecurseT for self-references
• Opaque constructors: ConstructorT for unhandled generics

Integration with Theorem Proving

Once constructed, the TypeExpr tree is consumed by TheoremProver.scala to search for a corresponding TermExpr (λ‑term) that inhabits the type. The macro expansion in Macros.scala ultimately emits Scala source code via emitTermCode, completing the Curry-Howard pipeline from type signature to implementation.

Summary

• The typeExpr macro in package.scala provides the public API, delegating to Macros.typeExprImpl.
• typeExprImpl uses c.WeakTypeTag to capture compile-time types and invokes buildTypeExpr to perform the translation.
• buildTypeExpr recursively pattern-matches on Scala type structures, encoding functions as implications (#->), case classes as named conjunctions (NamedConjunctT), and sealed traits as disjunctions (DisjunctT).
• Recursive types are detected via the typesSeen set and encoded as RecurseT to prevent infinite loops.
• Case classes become NamedConjunctT nodes with accessor metadata, while case objects become empty conjunctions.
• Unrecognized generic types fall back to ConstructorT, treated as opaque atoms during proof search.

Frequently Asked Questions

What is the difference between BasicT and ConstructorT in the TypeExpr AST?

BasicT represents primitive, non-parameterized types such as Int, String, or Any, acting as terminal leaves in the type expression tree. ConstructorT represents generic type constructors like Seq[Int] or Option[A] that take type arguments; while it preserves the constructor name and its arguments, it treats the structure as an opaque atom during proof search rather than decomposing it into algebraic components.

How does the typeExpr macro handle generic type parameters in case classes?

When processing a case class, the macro extracts the class's type parameters and builds a typeMap that associates parameter names with their concrete TypeExpr representations derived from the specific type application. As it processes each case accessor (field), it applies TypeExpr.substNames with the typeMap to replace any type parameter references in the field's type with the corresponding concrete types, ensuring the resulting NamedConjunctT contains fully resolved type information.

What happens when the macro encounters a recursive type definition?

The buildTypeExpr method maintains a typesSeen set that tracks the names of types currently being processed in the recursion stack. If the method encounters a type whose name already exists in typesSeen, it recognizes a recursive reference and returns a RecurseT(name, args) node instead of expanding the type again. This mechanism prevents infinite macro expansion while preserving the recursive structure necessary for the theorem prover to generate correct recursive implementations.

How does the macro handle generic types like Seq[Int] that are not case classes?

Types that do not match the specific patterns for functions, primitives, or algebraic data types are encoded as ConstructorT(name, args). For Seq[Int], this produces ConstructorT("Seq", List(BasicT("Int"))). During theorem proving, these constructors are treated as opaque atomic types; the prover knows the constructor name and its arguments but does not decompose the internal structure of Seq itself.

{
  "mcpServers": {
    "instagit": {
      "command": "npx",
      "args": ["-y", "instagit@latest"]
    }
  }
}