Skip to content

Latest commit

 

History

2 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 

Repository files navigation

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

About

Type level lambda calculus in Scala

Topics

Resources

Stars

34 stars

Watchers

4 watching

Forks

Releases

Packages

Contributors

Languages