This repository demonstrates compile-time lambda calculus parser, evalator, and type checker in Scala 3. It is heavily depending on match types feature.
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"]]]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.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.
- 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
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent