Модельный язык программирования — исследование типизации

Модельный язык программирования с шаблонами, на примере которого изучается алгоритм типизации Хиндли-Милнера (Белякова Ю.).

Язык нужен для исследования алгоритма типизации, поэтому операторы не будут исполняться.
Основная задача — проверка и вывод типов.

Единственный исполняемый оператор — print_type.

print_type <выражение>;

Выражением может быть имя функции, арифметическое или логическое выражение, применение, etc.

Синтаксис

Присваивание

Nat x = 5;     
var x = 7.9;   // автовыведение типа переменной
y = x;

Выражения

expr
(expr)

Арифметические:

a + b
a - b
a * b
a / b
a div b
a mod b

Логические:

a || b
a && b
!a

Условный оператор

if <условие> then
    ops1
{elif <условиеi> then
    opsi}
[else
    ops2]
fi

Цикл

Цикл с предусловием.

while <условие> do
    ops;
done

Функции

Определение функции:

Nat foo() def          // функция без параметров
    ...
    return 5;
fed

Nat foo(Nat x) def     // функция с параметрами
    ...
    return x + 7;
fed

void foo(...) def      // процедура
    ...
    return;
fed

t_inf foo(...) def      // автовыведение типа возвращаемого значения
    ...
    return true;
fed

Определение шаблона функции:

T foo<T, S>(S->T f, S xx) def
    ...
fed

Вызов функции:

foo(x, y, ...);

Методы

x.p();

Базовые типы

• Nat
• Bool
• Int
• Double