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

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

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

Синтаксис

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

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
a == b
a < (>) b
a <= (>=) b

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

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

Цикл

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

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

Функции

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

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

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

void foo(<параметры>)       // процедура
    ...
    return;
end

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

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

T foo[!T, S](S->T f, S xx) 
    ...
end

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

foo(x, y, ...);

Типы

Базовые типы

• Nat
• Bool
• Int
• Double
• String

Функциональные типы

T->S
T->S->U ~ T->(S->U)
(T->S)->U

Процедуры и функции

Основная функция — typeof.

typeof(<выражение>);

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

Вероятно, добавим вывод:

print()

Лямбда-выражения

Простое лямбда-выражение от одного параметра:

Nat x => x*x

Простое лямбда-выражение от двух параметров:

(Nat x, Nat y) => x + y

Сложное лямбда-выражение от двух параметров (???):

(Nat x, Nat y) => {var z = x + y; return ((x + y) mod 2 = 0) ? x*x : y*y}

var lambda =
  Nat x => var y = x*x*x;
               var z = f(y);
               z + x <=