Live coding a lambda calculus with core.typed

core-typed-live-coding.clj

(ns achilles.live
  (:require [clojure.core.typed :as t]))

"term : x          (Variable)
        λx.term    (Abstraction)
        term term  (Application)"

(t/ann-datatype TVar [name :- t/Str])
(deftype TVar [name])

(t/ann-datatype TAbs [argument :- TVar
                      body :- Term])
(deftype TAbs [argument body])

(t/ann-datatype TApp [lhs :- Term
                      rhs :- Term])
(deftype TApp [lhs rhs])

(t/defalias Term (t/U TVar TAbs TApp))

(t/ann v [t/Str -> TVar])
(def v ->TVar)

(t/ann abs [TVar, Term -> TAbs])
(def abs ->TAbs)

(t/ann app [Term, Term -> TApp])
(def app ->TApp)

(def program
  (app
   (abs (v "x") (v "x"))
   (v "input")))

(t/ann show [Term -> t/Str])
(defmulti show class)
(defmethod show TVar [^TVar v]
  (.name v))
(defmethod show TApp [^TApp app]
  (str (show (.lhs app)) " " (show (.rhs app))))
(defmethod show TAbs [^TAbs abs]
  (str "λ"(show (.argument abs)) "." (show (.body abs))))

(t/defalias Value (t/U Number [Value -> Value]))
(t/defalias Context (t/Map t/Str Value))

(t/ann interp [Context, Term -> Value])
(defmulti interp (fn [_ term] (class term)))
(defmethod interp TVar [context ^TVar v]
  (if-let [found (get context (.name v))]
    found
    (throw (Exception. (str (.name v) " is not bound")))))
(defmethod interp TApp [context ^TApp app]
  (let [lhs (interp context (.lhs app))
        rhs (interp context (.rhs app))]
    (if (number? lhs)
      (throw (Exception. (str (show (.lhs app)) " is not a function: " lhs)))
      (lhs rhs))))
(defmethod interp TAbs [context ^TAbs abs]
  (t/fn [arg :- Value] :- Value
    (let [argument ^TVar (.argument abs)
          body (.body abs)
          context' (assoc context (.name argument) arg)]
      (interp context' body))))

(show program)
(interp {"input" 98}
        program)