untyped lambda calculus in various languages

utlc.aya

--| Basic definitions of natural numbers, booleans and deBruijn indices
--------------------------------------------------------------------------------
open data Nat : Type | zero | suc Nat
open data Bool : Type | true | false
open data DBI : Type | Dbi Nat

def infix ==' (a b : Nat) : Bool
  | zero, zero => true
  | zero, suc b => false
  | suc a, zero => false
  | suc a, suc b => a ==' b

def infix == (a b : DBI) : Bool
  | Dbi a, Dbi b => a ==' b

def if {A : Type} (cond : Bool) (t f : A) : A
  | {A}, true, t, f => t
  | {A}, false, t, f => f

--| Well-typed terms, substitution and evaluation
--------------------------------------------------------------------------------
open data Term : Type
  | Ref DBI
  | Lam DBI Term
  | App Term Term

def subst (term : Term) (dbi : DBI) (replace : Term) : Term
  | Ref i,          dbi, replace => if (i == dbi) replace (Ref i)
  | Lam param body, dbi, replace => Lam param (subst body dbi replace)
  | App fn arg,     dbi, replace => App (subst fn dbi replace) (subst arg dbi replace)

def applyLam (lam : Term) (arg : Term) : Term
  | Lam param body, arg => subst body param arg
  | Ref i, arg => Ref i
  | App fn arg', arg => App fn arg

def normalize (term : Term) : Term
  | Ref i => Ref i
  | Lam param body => Lam param body
  | App lam arg => applyLam (normalize lam) (normalize arg)

--| Definitions of some usual functions like id, const
----------------------------------------------------------------

def a : DBI => Dbi zero
def b : DBI => Dbi (suc zero)

def infixr |> (dbi : DBI) (body : Term) => Lam dbi body
def infixl $ (term : Term) (arg : Term) => App term arg

--| Haskell: id a = a
def id        : Term => a |> Ref a
--| Haskell: const a b = a
def const     : Term => a |> b |> Ref a

--| Applying id to const
def constId   : Term => const $ id

--| Path type
----------------------------------------------------------------
prim I
prim left
prim right
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
 | at (i : I) : A i {
   | left => a
   | right => b
 }
def path {A : I -> Type} (p : Pi (i : I) -> A i)
  => new Path A (p left) (p right) { | at i => p i }
def infix = {A : Type} (a b : A) : Type => Path (\ i => A) a b
def idp {A : Type} {a : A} : a = a => path (\ i => a)

--| Proofs that:
--|   id a normalizes to a
--|   const a b normalizes to a
--|   constId a b normalizes to b
--|   flipConst is equal to constId
----------------------------------------------------------------
def valA : Term => Ref a
def valB : Term => Ref b

def id-a-is-a : normalize (id $ valA) = valA => idp
def id-b-is-b : normalize (id $ valB) = valB => idp
def const-a-b-is-a   : normalize (const $ valA $ valB) = valA => idp
def constId-a-b-is-b : normalize (constId $ valA $ valB) = valB => idp

def flipConst : Term => a |> b |> Ref b
def flipConst=constId (a b : Term)
   : normalize (flipConst $ a $ b) = normalize (constId $ a $ b)
  => idp

utlc.rs

#![feature(box_patterns)]
#![feature(box_syntax)]

#[derive(Debug, Eq, PartialEq, Clone)]
struct LocalVar(String);

#[derive(Debug, Eq, PartialEq, Clone)]
enum Term {
  Ref(LocalVar),
  App(Box<Term>, Box<Term>),
  Lam(LocalVar, Box<Term>),
}

impl Term {
  fn subst(self, name: &LocalVar, replace: &Term) -> Term {
    match self {
      Term::Ref(resolved) if &resolved == name => replace.clone(),
      Term::App(box f, box arg) => Term::App(box f.subst(name, replace), box arg.subst(name, replace)),
      Term::Lam(param, box body) if &param != name => Term::Lam(param, box body.subst(name, replace)),
      term => term
    }
  }

  fn normalize(self) -> Term {
    match self {
      Term::App(box f, box arg) => match f.normalize() {
        Term::Lam(param, box body) => body.subst(&param, &arg.normalize()),
        _ => panic!("type error: expected lambda in app")
      },
      term => term,
    }
  }
}

fn main() {
  use Term::*;
  let id = Lam(LocalVar("a".into()), box Ref(LocalVar("a".into())));
  let const_ = Lam(LocalVar("a".into()), box Lam(LocalVar("b".into()), box Ref(LocalVar("a".into()))));
  let flip_const = App(box const_.clone(), box id.clone());

  println!("id = {:?}", id);
  println!("const = {:?}", const_);
  println!("flip const = {:?}", flip_const);

  let hello = App(box const_, box Ref(LocalVar("hello".into()))).normalize();
  println!("const hello = {:?}", hello);
  println!("const hello world = {:?}", App(box hello, box Ref(LocalVar("world".into()))).normalize());
}

utlc.scala

case class LocalVar(name: String) {
    def ->(body: Term) = Lam(this, body)
}

sealed abstract class Term {
  def $(arg: Term) = App(this, arg)
}

case class Ref(resolved: LocalVar) extends Term
case class App(fn: Term, arg: Term) extends Term
case class Lam(param: LocalVar, body: Term) extends Term

def subst(term: Term, name: LocalVar, replace: Term): Term = term match {
  case Ref(resolved) if resolved == name => replace
  case App(fn, arg) => App(subst(fn, name, replace), subst(arg, name, replace))
  case lam@Lam(param, body) if param != name => Lam(param, subst(body, name, replace))
  case _ => term
}

def normalize(term: Term): Term = term match {
  case App(fn, arg) => normalize(fn) match {
    case Lam(param, body) => subst(body, param, normalize(arg))
    case _ => throw RuntimeException("type error: expected lambda in app")
  }
  case _ => term
}

implicit class LocalVarHelper(sc: StringContext) {
  def v(args: Any*): LocalVar = LocalVar(sc.parts.head)
}

@main def main: Unit = {
  val id = v"a" -> Ref(v"a") // a -> a
  val const = v"a" -> (v"b" -> Ref(v"a")) // a -> b -> a
  val flipConst = const $ id // a -> b -> b
  println(s"id = $id")
  println(s"const = $const")
  println(s"flipConst = $flipConst")

  val idHello = id $ Ref(v"hello") // should be hello
  val constHW = const $ Ref(v"hello") $ Ref(v"world") // should be hello
  val flipConstHW = flipConst $ Ref(v"hello") $ Ref(v"world") // should be world
  println(s"id hello = ${normalize(idHello)}")
  println(s"const hello world = ${normalize(constHW)}")
  println(s"flipConst hello world = ${normalize(flipConstHW)}")
}

zzz-utlc.cpp

// clang++ -std=c++17 zzz-utlc.cpp
// Prefixing this filename with `zzz` is aimed at putting this file at the very last.
// Less cpp, less permanent head damage. Please move to human-friendly langauges ASAP.

#include <iostream>
#include <string>
#include <variant>
#include <memory>
#include <functional>
#include <optional>

template <typename ... Ts>
struct Visitor : Ts ... { using Ts::operator()...; };
template <typename ... Ts> Visitor(Ts...) -> Visitor<Ts...>;

template <typename T>
using Box = std::unique_ptr<T>;

template <typename T>
using Option = std::optional<T>;

struct Ref;
struct App;
struct Lam;

using Term = std::variant<
  Ref,
  App,
  Lam
>;

struct LocalVar { std::string name; };
struct Ref { LocalVar resolvedVar; };
struct App { Box<Term> fn; Box<Term> arg; };
struct Lam { LocalVar arg; Box<Term> body; };

template <typename U, typename ...Ts>
auto cast(std::variant<Ts...> variant) -> Option<U> {
  return std::holds_alternative<U>(variant)
         ? std::optional<U>{std::move(std::get<U>(variant))}
         : std::nullopt;
}

template <typename T, typename... Args>
auto boxTerm(Args &&...args) -> Box<Term> {
  return std::move(std::make_unique<Term>(T{std::forward<Args>(args)...}));
}

template <typename T, typename U>
auto boxMap(Box<T> t, std::function<U(T)> mapper) -> Box<U> {
  return std::make_unique<U>(std::move(mapper(std::move(*t))));
}

auto subst(Term expr, const LocalVar &name, Term &replace) -> Term {
  return std::visit(Visitor{
    [&](Ref &&ref) { return ref.resolvedVar.name == name.name ? std::move(replace) : Term{std::forward<Ref>(ref)}; },
    [&](App &&app) {
      return Term{App{
        boxMap<Term, Term>(std::move(app.fn), [&](Term expr) { return subst(std::move(expr), name, replace); }),
        boxMap<Term, Term>(std::move(app.arg), [&](Term expr) { return subst(std::move(expr), name, replace); })
      }};
    },
    [&](Lam &&lam) {
      return lam.arg.name == name.name ? Term{std::forward<Lam>(lam)} : Term{Lam{
        lam.arg,
        boxMap<Term, Term>(std::move(lam.body), [&](Term expr) { return subst(std::move(expr), name, replace); })
      }};
    },
  }, std::move(expr));
}

auto normalize(Term expr) -> Term {
  return std::visit(Visitor{
    [&](Ref &&ref) { return Term{std::forward<Ref>(ref)}; },
    [&](App &&app) {
      auto fn = normalize(std::move(*app.fn));
      auto arg = normalize(std::move(*app.arg));
      auto lamOpt = cast<Lam>(std::move(fn));
      if (!lamOpt) throw std::runtime_error("type error: expected lambda in app");
      auto lam = std::move(*lamOpt);
      return subst(Term{std::move(*lam.body)}, lam.arg, arg);
    },
    [&](Lam &&lam) { return Term{std::forward<Lam>(lam)}; },
  }, std::move(expr));
}

///////////////////////////////////////
template <typename T>
std::ostream &operator<<(std::ostream &os, const Box<T> &box) {
  os << *box.get();
  return os;
}

std::ostream &operator<<(std::ostream &os, const LocalVar &var) {
  os << "LocalVar(name = \"" << var.name << "\")";
  return os;
}

std::ostream &operator<<(std::ostream &os, const Ref &ref) {
  os << "Ref(resolved = " << ref.resolvedVar << ")";
  return os;
}

std::ostream &operator<<(std::ostream &os, const App &app) {
  os << "App(fn = " << app.fn << ", arg = " << app.arg << ")";
  return os;
}

std::ostream &operator<<(std::ostream &os, const Lam &lam) {
  os << "Lam(arg = " << lam.arg << ", " << "body = " << lam.body << ")";
  return os;
}

std::ostream &operator<<(std::ostream &os, const Term &expr) {
  std::visit(Visitor{
    [&](const Ref &ref) { os << ref; },
    [&](const App &app) { os << app; },
    [&](const Lam &lam) { os << lam; },
  }, expr);
  return os;
}
///////////////////////////////////////

int main() {
  // Haskell:
  // id :: a -> a
  // id a = a
  auto id = boxTerm<Lam>(LocalVar{"a"}, boxTerm<Ref>(LocalVar{"a"}));
  std::cout << "id: " << id << std::endl;

  // Haskell:
  // idApp = id hello
  auto idApp = Term{App{
    std::move(id),
    boxTerm<Ref>(LocalVar{"hello"})
  }};

  std::cout << "idApp: " << idApp << std::endl;
  auto idAppNorm = normalize(std::move(idApp));
  std::cout << "idApp normalized: " << idAppNorm << std::endl;

  // Haskell:
  // add :: a -> a -> a
  // add a b = a + b
  auto add = boxTerm<Lam>(
    LocalVar{"a"},
    boxTerm<Lam>(
      LocalVar{"b"},
      boxTerm<App>(
        boxTerm<App>(boxTerm<Ref>(LocalVar{"+"}), boxTerm<Ref>(LocalVar{"a"})),
        boxTerm<Ref>(LocalVar{"b"})
      )
    )
  );

  std::cout << "add: " << add << std::endl;

  // Haskell:
  // add one two
  auto addOneTwo = Term{App{
    boxTerm<App>(std::move(add), boxTerm<Ref>(LocalVar{"one"})),
    boxTerm<Ref>(LocalVar{"two"})
  }};
  std::cout << "addOneTwo: " << addOneTwo << std::endl;
  auto addOneTwoNorm = normalize(std::move(addOneTwo));
  std::cout << "addOneTwo normalized: " << addOneTwoNorm << std::endl;
  return 0;
}