Skip to content

Instantly share code, notes, and snippets.

@nicmart
Created December 19, 2017 22:43
Show Gist options
  • Save nicmart/b6c1ac6e3a91cb339eca3180e5d3b0d1 to your computer and use it in GitHub Desktop.
Save nicmart/b6c1ac6e3a91cb339eca3180e5d3b0d1 to your computer and use it in GitHub Desktop.
Experiments with a tagless final encoding for the simply typed lambda-calculus, following section 3 of the paper "Typed Tagless Final Interpreters" by Oleg Kiselyov
import scala.language.higherKinds
trait Symantics[F[_,_]] {
def int[E](n: Int): F[E, Int]
def add[E](n: F[E, Int], m: F[E, Int]): F[E, Int]
def z[E, T]: F[(T, E), T]
def s[E, T, A](f: F[E, T]): F[(A, E), T]
def lam[E, A, B](f: F[(A, E), B]): F[E, A => B]
def app[E, A, B](f: F[E, A => B], a: F[E, A]): F[E, B]
}
trait Term[A, G[_]] {
def run[F[_, _], E](alg: Symantics[F]): F[G[E], A]
}
type Id[E] = E
type PrepInt[E] = (Int, E)
type Context[E, T] = E => T
object Evaluate extends Symantics[Context] {
override def int[E](n: Int): Context[E, Int] =
_ => n
override def add[E](n: Context[E, Int], m: Context[E, Int]): Context[E, Int] =
env => n(env) + m(env)
override def z[E, T]: Context[(T, E), T] = {
case (t, env) => t
}
override def s[E, T, A](f: Context[E, T]): Context[(A, E), T] = {
case (t, env) => f(env)
}
override def lam[E, A, B](f: Context[(A, E), B]): Context[E, A => B] =
env => a => f((a, env))
override def app[E, A, B](f: Context[E, A => B], a: Context[E, A]): Context[E, B] =
env => f(env)(a(env))
}
val expr1 = new Term[Int, Id] {
def run[F[_, _], E](alg: Symantics[F]): F[E, Int] = {
import alg._
add(int(1), int(2))
}
}
val expr2 = new Term[Int => Int, Id] {
def run[F[_, _], E](alg: Symantics[F]): F[E, Int => Int] = {
import alg._
lam(add(z, z))
}
}
var expr3 = new Term[Int, Id] {
def run[F[_, _], E](alg: Symantics[F]): F[E, Int] = {
import alg._
app(expr2.run(alg), int(3))
}
}
val expr2b = new Term[Int => Int, PrepInt] {
def run[F[_, _], E](alg: Symantics[F]): F[(Int, E), Int => Int] = {
import alg._
lam(add(z, s(z)))
}
}
var expr3b = new Term[Int, Id] {
def run[F[_, _], E](alg: Symantics[F]): F[E, Int] = {
import alg._
app(app(lam(expr2b.run(alg)), int(1)), int(2))
}
}
expr2.run(Evaluate)(())
expr3.run(Evaluate)(())
expr3b.run(Evaluate)(())
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment