Добрый вечер всем! Предлагаю продолжить дискуссию 20-летней давности, а именно, обсудить статическую типизацию в Рефале. Тема уже поднималась в рассылке как минимум 2 раза.
Первый раз Аркадий Климов предложил определять типы вариантом L-выражений (11 августа 1999): https://mazdaywik.github.io/direct-link/refal-botik-ru/refal/0005-utf8.html Рекомендую прочитать это письмо, прежде чем читать дальше. В нём Аркадий описал типизацию как теоретическую проблему, предложил приемлемое на практике решение и перечислил задачи, которые требуется решить при реализации типизации. Второй раз Михаил Ковтун предложил использовать древесные автоматы (19 августа 2001): https://mazdaywik.github.io/direct-link/refal-botik-ru/refal/0222-utf8.html https://mazdaywik.github.io/direct-link/refal-botik-ru/refal/0223-utf8.html https://mazdaywik.github.io/direct-link/refal-botik-ru/refal/0224-utf8.html https://mazdaywik.github.io/direct-link/refal-botik-ru/refal/0225-utf8.html Здесь в первом письме Михаил описывает свой подход в типизации, во втором Аркадий комментирует его соображения, в третьем и четвёртом Михаил Потанин и Сергей Абрамов дают непринципиальные уточнения. В общем, из этой переписки достаточно внимательно прочитать только первые два. (Эти письма конвертированы в UTF-8, поэтому должны открываться нормально.) Я сам как-то пытался реализовать прототип статической типизации — давал задачу на ВКР бакалавра (диплом). Но, поскольку эту тему взял студент-двоечник, ничего толкового не получилась. Остался проект с путанным кодом на Java, в src/main/resources/docs можно найти записку к диплому: https://github.com/bmstu-iu9/refal-type-verifier https://github.com/bmstu-iu9/refal-type-verifier/tree/master/src/main/resources/docs (записка довольно сумбурная) Мой подход был близок к подходу Аркадия с тем отличием, что рекурсия для e-переменных на верхнем уровне запрещена, но допустим итератор (звёздочка) для одного терма. Система типов для Рефала, на мой взгляд, обязательно должна включать параметрический полиморфизм. Допустим, есть такая функция: Rev { t.First e.Mid t.Last = t.Last <Rev e.Mid> t.First; t.One = t.One; /* пусто */ = /* пусто */; } Вот какой у неё тип? <Rev t.x*> == t.x* для любого t.x. Т.е. если функция вызывается со строкой символов — она должна возвращать строку. Если последовательность скобочных термов с какой-то хитрой структурой — на выходе должны быть они же. Подход Аркадия, как мне кажется, проще расширить на обобщённые типы, нежели подход Михаила. Потому что в случае древесных автоматов нужно научиться решать регулярные неравенства, а как их решать, тем более эффективно — понятия не имею. С уважением, Александр Коновалов
