Typed eDSLs in Go

This article shows how to implement an embedded typed DSL in Go. The representation in question will be type-safe, i.e. it will not allow constructing incorrect expressions (terms), but will allow different interpretations of expressions. The DSL type system is mapped one-to-one to the Go type system, so all type-checking is performed by the compiler.

This usually requires GAD or HKT. The article shows a mechanism for encoding expressions that does not depend on either the first or the second.

Unlike universal Boehm-Berarducci quantified coding [1] This article uses existential quantification (without the need for higher-order polymorphism due to the fact that interfaces are existential types).

Hidden text

For existential types, see [2]

Like algebraic data types, the considered encoding is closed (it is impossible to add a new statement without reworking the code), but it is type-safe and pattern-matching operations are checked for completeness at compile-time. The alternative encoding of GADT in the Tagless-final style requires polymorphic terms, which in Go can only be functions, but functions are not serialized. In this case, the closed encoding is a conscious choice in favor of greater type-safety, but if desired, the encoding can be made open to solve expression problem.

We will code the following GADT (Haskell example):

data Exp a where
    Lit :: a -> Exp a
    Add :: Exp Int -> Exp Int -> Exp Int
    Or  :: Exp Bool -> Exp Bool -> Exp Bool
    Lt  :: Exp Int -> Exp Int -> Exp Bool
    If  :: Exp Bool -> Exp a -> Exp a -> Exp a

DSL implementation

The Exp interface represents a serializable expression in our eDSL. The MatchExp method unpacks the ADT for further processing. ExpBoolVars and ExpIntVars are continuation sets (continuations). The return type ExpKind is not strictly required for encoding, but it is more convenient to communicate which continuation was selected for processing.

type Exp interface {
	MatchExp(ExpBoolVars, ExpIntVars) ExpKind
}

Let's introduce a small crutch, a limitation ety for denotational semantics of DSL

type ety interface {
	bool | int
}

exp
Exp
}

ExpBoolVars, ExpIntVars represents projections of ADT constructors. For this to work, the set of internal types in the DSL must be finite. Not shown here, but constructors can still be polymorphic.

// Продолжения для булевых выражений
type ExpBoolVars interface {
	Lit(bool)
	Or(exp[bool], exp[bool])
	Lt(exp[int], exp[int])
	If(exp[bool], exp[bool], exp[bool])
}

// Продолжения для int выражений
type ExpIntVars interface {
	Lit(int)
	Add(exp[int], exp[int])
	If(exp[bool], exp[int], exp[int])
}

ExpKind another ADT needed to classify expressions by their types. KindVars – these are possible continuations for processing the result of the expression.

type ExpKind interface {
	MatchKind(KindVars)
}

type KindVars interface {
	Bool(ExpBoolVars)
	Int(ExpIntVars)
}

boolVal, intVal capture continuations for the corresponding expressions. Implement the ExpKind interface.

type boolVal struct{ ev ExpBoolVars }
type intVal struct{ ev ExpIntVars }

func (b boolVal) MatchKind(v KindVars) { v.Bool(b.ev) }
func (n intVal) MatchKind(v KindVars)  { v.Int(n.ev) }

MatchIntExp, MatchBoolExp – functions for reusing continuations for those operations for which we already know their type.

func MatchIntExp[tv ExpIntVars](e exp[int], v tv) tv {
	e.MatchExp(nil, v)
	return v
}

func MatchBoolExp[tv ExpBoolVars](e exp[bool], v tv) tv {
	e.MatchExp(v, nil)
	return v
}

lit
type add struct{ a, b exp[int] }
type or struct{ a, b exp[bool] }
type lt struct{ a, b exp[int] }
type if_[t ety] struct {
c exp[bool]
t exp
f exp
}

Methods MatchExp are implementing exp
switch v := interface{}(l).(type) {
case lit[bool]:
bv.Lit(bool(v.val))
return boolVal{bv}
case lit[int]:
nv.Lit(int(v.val))
return intVal{nv}
default:
panic("unreachable")
}
}
func (n add) MatchExp(_ ExpBoolVars, v ExpIntVars) ExpKind {
v.Add(n.a, n.b)
return intVal{v}
}
func (b or) MatchExp(v ExpBoolVars, _ ExpIntVars) ExpKind {
v.Or(b.a, b.b)
return boolVal{v}
}
func (b lt) MatchExp(v ExpBoolVars, _ ExpIntVars) ExpKind {
v.Lt(b.a, b.b)
return boolVal{v}
}
func (e if_
switch interface{}(*new
case bool:
bv.If(e.c, e.t.(exp[bool]), e.f.(exp[bool]))
return boolVal{bv}
case int:
nv.If(e.c, e.t.(exp[int]), e.f.(exp[int]))
return intVal{nv}
default:
panic("unreachable")
}
}

We implement fmt.Stringer for value constructors.

func (l lit
func (n add) String() string    { return fmt.Sprintf("(add %v %v)", n.a, n.b) }
func (b or) String() string     { return fmt.Sprintf("(or %v %v)", b.a, b.b) }
func (b lt) String() string     { return fmt.Sprintf("(lt %v %v)", b.a, b.b) }
func (e if_
func Add(a, b exp[int]) add { return add{a, b} }
func Or(a, b exp[bool]) or  { return or{a, b} }
func Lt(a, b exp[int]) lt   { return lt{a, b} }
func If[t ety](c exp[bool], tr, fl exp
	return if_
}

Using DSL

Everything that has been considered up to this section was the internal implementation. Now we will consider the code from the point of view of the DSL consumer. We want to write an interpretation of the ADT in which the operational semantics of the big step (big-step). We can choose other interpretations – this approach does not force us to make a specific choice. As an example, we can write an interpretation that compiles to native code.

Let's look at the interpretation of eval.

EvalInt This is a set of mutually recursive definitions that define the value of expressions of type int. EvalInt implements ExpIntVarsso the compiler checks that we implement all the required continuations (pattern matching options), otherwise the code will not compile. By analogy, we add EvalBool.

type EvalInt int
type EvalBool bool

func (ev *EvalInt) Lit(n int) { *ev = EvalInt(n) }
func (ev *EvalInt) Add(a, b exp[int]) {
	*ev = evalInt(a) + evalInt(b)
}
func (ev *EvalInt) If(c exp[bool], t, f exp[int]) {
	if evalBool(c) {
		*ev = evalInt
		return
	}
	*ev = evalInt(f)
}

func evalInt(e exp[int]) EvalInt {
	// Компилятор знает, что мы работаем с exp[int],
	// так что здесь нельзя вызвать MatchBoolExp по ошибке.
	return *MatchIntExp(e, new(EvalInt))
}

func (ev *EvalBool) Lit(b bool) { *ev = EvalBool(b) }
func (ev *EvalBool) Or(a, b exp[bool]) {
	*ev = evalBool(a) || evalBool(b)
}
func (ev *EvalBool) Lt(a, b exp[int]) {
	if evalInt(a) < evalInt(b) {
		*ev = EvalBool(true)
		return
	}
	*ev = EvalBool(false)
}
func (ev *EvalBool) If(c, t, f exp[bool]) {
	if evalBool(c) {
		*ev = evalBool
		return
	}
	*ev = evalBool(f)
}
func evalBool(e exp[bool]) EvalBool {
	return *MatchBoolExp(e, new(EvalBool))
}

Eval provides all the necessary continuations that ADT requires: ExpBoolVars, ExpIntVars, ExpKind. We can't forget any implementation. It won't compile.

type Eval struct {
	EvalInt
	EvalBool
	val interface{}
}

Function eval evaluates the value of an expression. Unlike evalBool And evalIntwhich accept exp
var ev Eval

// После этого вызова мы знаем что сделан правильный выбор продолжения
// Но не знаем какой именно
ek := e.MatchExp(&ev.EvalBool, &ev.EvalInt)

// А после этого вызова узнаем и вернем значение
ek.MatchKind(&ev)
return ev.val
}
func (ev *Eval) Bool(ExpBoolVars) {
ev.val = ev.EvalBool
}
func (ev *Eval) Int(ExpIntVars) {
ev.val = ev.EvalInt
}

We can create and combine expressions. All expressions have some subtype exp
var e01 = Lit(42)
var e02 = Add(e01, Lit(22))
var e03 = Or(e00, Lit(true))
var e04 = Lt(e02, e01)
var e05 = If[int](e04, e01, e02)
var e06 = If[bool](e03, e03, e00)

We can store expressions in a heterogeneous list:

var progs = []Exp{
	e01,
	e02,
	e03,
	e04,
	If[int](e04, e01, e02),
	If[bool](e03, e03, e00),
}

For each expression (without knowing its specific type), we run the unified procedure eval

func main() {
	for _, p := range progs {
		fmt.Printf("%v=%v\n", eval(p), p)
	}
}

We get the following result:

42=(lit 42)
64=(add (lit 42) (lit 22))
true=(or (lit false) (lit true))
false=(lt (add (lit 42) (lit 22)) (lit 42))
64=(if (lt (add (lit 42) (lit 22)) (lit 42)) (lit 42) (add (lit 42) (lit 22)))
true=(if (or (lit false) (lit true)) (or (lit false) (lit true)) (lit false))

Links

  1. Beyond Church encoding: Boehm-Berarducci isomorphism

  2. Roman Dushkin. Monomorphism, Polymorphism and Existential Types

Similar Posts

Leave a Reply

Your email address will not be published. Required fields are marked *