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

symantics.scala

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)(())