Добрый день!

Не могу найти не большого и внятного описания проектирования и создания статической системы типов и реализации вывода типов. Читаю TAPL, но он достаточно сложен для понимания неподготовленному читателю, без хорошего мат. бекграунда. Может вы встречали описание решения подобной задачи или решали/знаете как решать?

Задача простая: есть язык (для простоты возьмем диалект Лиспа, чтобы не заморачиваться синтаксисом), есть примерное понимание системы типов, которая должна быть реализована в языке -- Система F (лямбда-исчисление с полиморфизмом). Для простоты можно взять только простые варианты типов: примитивные типы (действительное — целое — знаковое/беззнаковое целое), структура, объединение (с тегом типа и без тега типа (C-style)).

Как я сейчас вижу себе решение этой задачи:
— Тип включает ссылки на базовые типы и ссылки на типы наследники, любой тип может быть приведен к базовому, то есть отношение наследования в типах реализует отношение "является": беззнаковое целое является целым, целое является действительным и т.д.
— Вывод типов для выражения происходит следующим образом, на примере:
Дано:
— результат парсинга входной строки -- '(+ (to_str 10) abc)
— лисп-система содержащая символы:
— + имеет тип (generic-function a b) со следующими реализациями (+ a:int b:int):int и (+ a:string b:string):string к примеру
— to_str имеет тип (generic-function a) со следующими реализациями (to_str a:int):string и (to_str a:uint):string
— abc имеет тип string

Нужно: проставить типы всему выражению и всем подвыражениям

Алгоритм решения:
1) Нужно составить систему уравнений для всех ограничений типов выводимых из использования выражений
1.1) Каждому выражению присваиваем уникальное имя: + = A, 10 = B, abc = C, to_str = D, (to_str 10) = E, (+ (to_str 10) abc) = F
1.2) Добавляем все ограничения типов последовательно
1.2.1) Список F типизируем по первому элементу, подтипам в нем тоже присваиваем уникальные имена (G H I):

F = G
(and H:int I:int) = G:int
(and H:string I:string) = G:string
H = (or string int)
I = (or string int)
E = H
C = I

1.2.2) Далее список E (J K):

E = J
J = string
K = (or int uint)
B = K

1.2.3) Типизируем B по значению, выбираем наиболее узкий тип (в реальном применении тут может быть правило -- наиболее узкий, но не уже машинно-специфичного, то есть не ubyte, а uint например, для эффективности)

B = (or ubyte byte)

1.2.3) Второй параметр в F -- С:

C = string

1.3) Полученная система уравнений:

F = G
(and H:int I:int) = G:int
(and H:string I:string) = G:string
H = (or string int)
I = (or string int)
E = H
C = I
E = J
J = string
K = (or int uint)
B = K
B = (or ubyte byte)
C = string

2) Нужно эту систему уравнений решить, решать её можно по идее хоть в лоб прямым перебором в ширину или глубину, это уже вопрос скорости процесса компиляции, здесь же решим её аналитически:

F = string
G = string
H = string
I = string
E = string
J = string
K = (or int uint)
B = (or int uint)
C = string

3) Здесь по идее мы получили ошибку вывода типа, т.к. 10 может быть как int, так и uint и требуется дополнительная декларация типа. Если такую декларацию добавить:

(+ (to_str (: 10 uint)) abc)

То выражение будет типизироваться корректно.

--

Правильное или не правильное понимание сути решения задачи? Каким образом лучше/проще реализовать систему записи и решения таких уравнений? Есть ли уже какие-то готовые системы вывода типов на Си++?