Tagless-Final in Lean

Stream: new members

[Aram Hăvărneanu]

I am learning Lean and I seeking suggestions on how to improve the following example of a DSL embedded in tagless-final style.

structure Value (α : Type) where
  val : α

def eval {α : Type} (e : Value α) : α := e.1

structure Syntax (α : Type) where
  val : String

def print {α : Type} [ToString α] (e : Syntax α) : String := e.1

class Exp (T : Type -> Type) where
  lit : {α : Type} -> [ToString α] -> α -> T α
  neg : T Int -> T Int
  add : T Int -> T Int -> T Int

instance : Exp Value where
  lit l := { val := l }
  neg e := { val := -e.val }
  add e1 e2 := { val := e1.val + e2.val }

instance : Exp Syntax where
  lit l := { val := "(lit " ++ toString l ++ ")" }
  neg e := { val := "(neg " ++ toString e.val ++ ")" }
  add e1 e2 := { val := "(add " ++ toString e1.val ++ " " ++ e2.val ++ ")" }

class EqExp (T : Type -> Type) extends Exp T where
  eq : {α : Type} -> [BEq α] ->T α -> T α -> T Bool

instance : EqExp Value where
  eq e1 e2 := { val := e1.val == e2.val }

instance : EqExp Syntax where
  eq e1 e2 := { val := "(eq " ++ toString e1.val ++ " " ++ e2.val ++ ")" }

class MulExp (T : Type -> Type) extends Exp T where
  mul : T Int -> T Int -> T Int

instance : MulExp Value where
  mul e1 e2 := { val := e1.val * e2.val }

instance : MulExp Syntax where
  mul e1 e2 := { val := "(mul " ++ toString e1.val ++ " " ++ e2.val ++ ")" }

open Exp
open EqExp
open MulExp
abbrev Exp' (α : Type) := {T : Type -> Type} -> [Exp T] -> T α
abbrev EqExp' := {T : Type -> Type} -> [EqExp T] -> T Bool
abbrev MulExp' := {T : Type -> Type} -> [MulExp T] -> T Int

def t0 : Exp' Int := lit 1
def t1 : Exp' Int := lit 1
def t2 : Exp' Int := lit 2
def t3 : Exp' Bool := lit true
def t4 : Exp' Bool := lit true
def t5 : Exp' Bool := lit false
def t6 : Exp' Int := neg t0
def t7 : Exp' Int := add t1 t2
def t8 : EqExp' := eq t1 t2
def t9 : EqExp' := eq t3 t4
def t10 : MulExp' := mul t2 t7

#eval eval t0
#eval eval t1
#eval eval t2
#eval eval t3
#eval eval t4
#eval eval t5
#eval eval t6
#eval eval t7
#eval eval t8
#eval eval t9
#eval eval t10

#eval print t0
#eval print t1
#eval print t2
#eval print t3
#eval print t4
#eval print t5
#eval print t6
#eval print t7
#eval print t8
#eval print t9
#eval print t10

The code does what I aimed to do, the encoding is extensible in two directions, you can extend the language without having to modify existing terms or existing interpretations, and you can also add new interpretations. Also you can only construct well-typed terms.

There is plenty of room for improvement, however.

First, is there a way to have type inference work for the terms? It's quite annoying to type terms by hand. Note that this works in Haskell.

Second, the denotational domain is of type Type -> Type. This is required, for example, by EqExp, because we want to have a polymorphic equality function (in the embedded DSL), but of course, the expression itself is a boolean expression. Having the denotational domain of type Type -> Type allows one to extract the type of the subterms. However, this choice forced us to invent some irrelevant wrappers for the denotational domains (Value and Syntax above) just because we needed something of type Type -> Type. Is there a way to get a Type -> Type that doesn't involve creating new types?

(As an aside, Oleg uses kind * in Haskell for his denotational domain, he can get away with it because his DSL doesn't have polymorphism, but I want mine to have polymorphism.)

I think some sort of identity function should work, for example, this implementation of Exp works:

instance : Exp (fun α => α) where
  lit l := l
  neg e := -e
  add e1 e2 := e1 + e2

Not only it works, but it reads much nicer than my original one for Value, because we don't need to pack/unpack the inner term. However, I don't know how to extract the value out of it (basically I don't know how to write eval for this type).

Since this is my first Lean program I am sure there are many other possible improvements to be made, and I am would be grateful for every suggestion.

Thanks!