golang

Типизированные eDSL на Go

  • понедельник, 26 августа 2024 г. в 00:00:15
https://habr.com/ru/articles/838268/

В статье показано, как реализовать встраиваемый типизированный DSL на Go. Рассматриваемое представление будет типобезопасным, т.е. не позволит сконструировать некорректные выражения (термы), но допускает разные интерпретации выражений. Система типов DSL один-к-одному маппится на систему типов Go, поэтому весь type-checking производится компилятором.

Обычно для этого требуются GADT или HKT. В статье показан механизм кодирования выражений, который не зависит ни от первого, ни от второго.

В отличие от универсально квантифицированного кодирования Boehm-Berarducci [1] в данной статье используется экзистенциальное квантифицирование (без потребности в полиморфизме высшего порядка за счет того, что интерфейсы являются экзистенциальными типами).

Скрытый текст

Про экзистенциальные типы см. [2]

Как и алгебраические типы данных рассматриваемое кодирование закрыто (нельзя без доработки кода добавить новый statement), но типобезопасно и операции паттерн-матчинга проверяются на полноту в compile-time. Альтернативное кодирование GADT в стиле Tagless-final требует полиморфные термы, которые в Go могут быть только функциями, но функции не сериализуются. В данном случае закрытость кодирования это осознанный выбор в пользу большей type-safety, но при желании можно сделать кодирование открытым, чтобы решить expression problem.

Мы будем кодировать следующий GADT (пример на Haskell):

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

Интерфейс Exp представляет сериализуемое выражение на нашем eDSL. Метод MatchExp распаковывает ADT для продолжения обработки. ExpBoolVars и ExpIntVars это множества продолжений (continuations). Возвращаемый тип ExpKind строго говоря не обязателен для кодирования, но так удобней сообщать какое из продолжений было выбрано для обработки.

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

Введем небольшой костыль, ограничение ety для денотационной семантики DSL

type ety interface {
	bool | int
}

exp[t] - выражение для DSL-ного типа t, который маппится на Go-тип t. Не является сериализуемым в отличие от Exp. Причина по которой мы можем сохранить сериализуемость Exp, заключается в том что t это фантомный тип (существует только в compile-time для проверки типов). Кодирование бестеговое (tagless), таким образом мы можем поместить его за экзистенциалом и использовать гетерогенные списки выражений.

type exp[t ety] interface {
	Exp
}

ExpBoolVars, ExpIntVars представляет проекции конструкторов ADT. Чтобы это работало множество внутренних типов у DSL должно быть конечным. Здесь не показано, но конструкторы все еще могут быть полиморфными.

// Продолжения для булевых выражений
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 еще один ADT нужный чтобы классифицировать выражения по их типам. KindVars - это возможные продолжения для обработки результата выражения.

type ExpKind interface {
	MatchKind(KindVars)
}

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

boolVal, intVal захватывают продолжения для соответствующих выражений. Реализуют интерфейс ExpKind.

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 - функции для переиспользования продолжений для тех операций для которых уже знаем их тип.

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[t], add, or, lt, if_ кодируют типизированные выражения. Если ADT это абстрактное представление, то здесь мы уточняем конкретные типы значений.

type lit[t ety] struct{ val t }
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[t]
	f exp[t]
}

Методы MatchExp реализуют exp[t]. Каждая функция выбирает соответствующие продолжения, исполняет их. Мы используем switch по типам чтобы обойти ограничения Go и отсутствие универсальной квантификации для методов. Компилятор Go не может понять что набор case веток полон (exhaustive) и требует указать default. На уровне пользователя DSL никаких switch не требуется.

func (l lit[t]) MatchExp(bv ExpBoolVars, nv ExpIntVars) ExpKind {
	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_[t]) MatchExp(bv ExpBoolVars, nv ExpIntVars) ExpKind {
	switch interface{}(*new(t)).(type) {
	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")
	}
}

Реализуем fmt.Stringer для конструкторов значений.

func (l lit[t]) String() string { return fmt.Sprintf("(lit %v)", l.val) }
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_[t]) String() string { return fmt.Sprintf("(if %v %v %v)", e.c, e.t, e.f) }

Реализуем конструкторы значений как функции вместо того, чтобы дать пользователю создавать типы напрямую, потому что вывод типов в Go работает лучше в этом случае. К сожалению, это все еще не работает для If, что удручает. Если бы Go использовал вывод типов по алгоритму Хиндли - Милнера, то проблем бы не было.

func Lit[t ety](v t) lit[t] { return lit[t]{v} }
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[t]) if_[t] {
	return if_[t]{c, tr, fl}
}

Использование DSL

Все что было рассмотрено до этого раздела было внутренней реализацией. Далее будем рассматривать код с точки зрения потребителя DSL. Мы хотим написать интерпретацию ADT в которой будет определена операционная семантика большого шага (big-step). Мы можем выбрать и другие интерпретации - данный подход не заставляет делать конкретный выбор. Как пример мы может написать интерпретацию которая компилирует в native код.

Разберем интерпретацию eval.

EvalInt это множество взаимно рекурсивных определений, которые определяют значение выражений типа int. EvalInt реализует ExpIntVars, поэтому компилятор проверяет, что мы реализуем все требуемые продолжения (варианты паттерн-матчинга), а иначе код не скомпилируется. По аналогии добавляем 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(t)
		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(t)
		return
	}
	*ev = evalBool(f)
}
func evalBool(e exp[bool]) EvalBool {
	return *MatchBoolExp(e, new(EvalBool))
}

Eval предоставляет все необходимые продолжения, которые требуются ADT: ExpBoolVars, ExpIntVars, ExpKind. Мы не можем забыть какую-то имплементацию. Это не скомпилируется.

type Eval struct {
	EvalInt
	EvalBool
	val interface{}
}

Функция eval вычисляет значение выражения. В отличие от evalBool и evalInt, которые принимают exp[t], eval принимает Exp, что позволяет ему работать с гетерогенными списками выражений. Внутри Exp содержится достаточно информации для обработки. А exp[t] мы вводили для большей типобезопасности.

func eval(e Exp) interface{} {
	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
}

Мы можем создавать и комбинировать выражения. У всех выражений какой-то подтип exp[t]. Комбинировать их можно только если проходит проверка типов.

var e00 = Lit(false)
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)

Мы можем сохранить выражения в гетерогенном списке:

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

Для каждого выражения (не зная его конкретный тип) запустим унифицированную процедуру eval 

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

Получим следующий результат:

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

Ссылки

  1. Beyond Church encoding: Boehm-Berarducci isomorphism

  2. Роман Душкин. Мономорфизм, полиморфизм и экзистенциальные типы