Type-level lambda calculus in Scala 3

This repository demonstrates compile-time lambda calculus parser, evalator, and type checker in Scala 3. It is heavily depending on match types feature.

Components

Parser

Parse[_] returns a type representing an abstract syntax tree of the parsed term.

import lambda.{Parse, Var, Abs, App}

summon[Parse["λx.x"] =:= Abs["x", Var["x"]]]

summon[Parse["λxy.x"] =:= Abs["x", Abs["y", Var["x"]]]]

summon[Parse["x y"] =:= App[Var["x"], Var["y"]]]

Evaluator

Eval[_] returns beta-normal form of the specified term. The evaluation strategy is leftmost-outermost.

import lambda.{Show, Eval, Parse}

summon[Show[Eval[Parse["(λxy.x) a b"]]] =:= "a"]

You can also use ReadEvalPrint[_] to Parse and Show together at once.

import lambda.ReadEvalPrint

summon[ReadEvalPrint["(λxy.x) a b"] =:= "a"]

Type checker

Type.Infer[_] returns a (Scala) type representing an abstract syntax tree of the type (of simply typed lambda calculus) of the specified term.

import lambda.Parse
import typing.{Show, Type}

summon[Show[Type.Infer[Parse["λx.x"]]] =:= "a -> a"]

You can also use Type.Check[_] (returns a boolean literal type) to determine whether a term is typeable.

Related Work

• tarao/lambda-scala: Type level lambda calculus in Scala
  • Scala 2 implmentation of type-level lambda calculus
  • It has no type checker
• About type-level lambda calculus in C++03 templates (in Japanese)
  • source code
  • lambda-scala3 is a translation from this implementation (except the parser)
• About match types and compile-time string literals by @xuwei-k (in Japanese)
  • source code 1
  • source code 2
  • This taught me how to write a compile-time parser