lambda-scala icon indicating copy to clipboard operation
lambda-scala copied to clipboard

verified publisher icon tarao
→

Metadata

Type level lambda calculus in Scala

Type level lambda calculus in Scala

This repository demonstrates an implementation of lambda calculus in Scala types.

Untyped lambda calculus

import lambda._
case class Equals[A >: B <: B, B]() // this checks type equality

type S = x ->: y ->: z ->: ( x @@ z @@ (y @@ z) )
type K = x ->: y ->: x

type result = ( S @@ K @@ K @@ a ) # ->*
Equals[result, a]

More examples are found in TermSpec.scala.

Syntax

Code
Variables a, b, ..., z
Abstraction v ->: M
Application M @@ N
Terms M, N
1-step beta reduction M # ->
Multi-step beta reduction M # ->*

  • You can define your own variables by calling #next of existing (last defined) variable

    type variableName1 = z #next
type variableName2 = variableName1 #next

  • You may need parenthesis to avoid ambiguity

Capture-avoiding substitutions

Lambda terms are converted internally to De Bruijn indexed terms and indices are shifted during substitution to ensure capture-avoiding semantics.

License

  • Copyright (C) INA Lintaro
  • MIT License

References

← Metadata

33
Stars
3
Forks
Watchers

Owner

verified publisher icon tarao

Metadata

Type level lambda calculus in Scala

Back