Subject: Refal weak typing
From: Arkady Klimov (klimovark@mail.ru)
Date: Wed Aug 11 1999 - 16:14:06 MSD
На вчерашнем Рефал-семинаре в ИПМ Виктор К. затронул вопрос о типизации
рефала как теоретической проблемы:
Необходимость типизации ощущается как желание иметь твердую почву под
ногами при написании больших программ. Но рефал - изначально
нетипизированный язык, который этим дает большую свободу, и в этом также его
преимущество перед такими изначально строго типизированными языками как
языки ML, Haskel и тп. Хотелось бы эту свободу не потерять. Поэтому подход к
типизации Рефала должен отличаться от подхода в ML. Типизатор должен уметь:
1. Выводить типы насколько это возможно и сообщать о них программисту. В
крайних случаях оставлять все как есть (то есть что все перменные могут
принимать любые допустимые значения).
2. Допускать описания типов некоторых функций и их аргументов на некотором
языке (аннотаций) и проверять их состоятельность, предупреждая о
несоответствиях..
Далее я высказываю свое видение этой проблемы, точнее ее конкретизацию.
Я не буду говорить о типизации типа Хиндли-Милнера (параметрический
полиморфизм для функций высших порядков). Возможно этот вопрос можно будет
поставить после. Сейчас меня интересует типизация данных, когда тип можно
понимать просто как ограничение на множество допустимых значений. Такая
задача также вытекает из практики: многим приходилось описывать в
комментариях что-то входе синтаксисов для обрабатываемых данных и мечтать о
том, чтобы компилятор проверял, что функции применяются к правильным данным.
Я решил это написать, имея несколько целей:
1. Сверить свое понимание проблемы с пониманим других.
2. Подтолкнуть молодых, дав по возможности более точную постановку.
3. Облегчить свою голову.
Продолжаю.
Чтобы задачи о типизации можно было решать, надо договориться о системе
типов (языке описания типов). Этот вопрос может решаться по разному. Есть
два общих требованиея к его решению:
1. Система типов должна быть достаточно богатой (детальной), чтобы
удовлетворить практические потребности.
2. Она должна быть достаточно бедной (грубой), чтобы можно было надеяться с
ней алгоритмически совладать (в частности, эффективно разрешать равенство,
включение и т.п.).
Как всегда, требования противоречивы и наша задача - найти удачный
компромисс.
Первый пункт можно конкретизировать так: хочется, чтобы система типов была
замкнутой относительно некоторых операций, в частности:
- объединение: T1 | T2
- произведение (для нас - конкатенация): T1 T2
- заключение в скобки (T)
- рекурсия - разрешимость системы уравнений
(T1, ..., Tn) = F(T1, ...,Tn),
где F- типовое выражение, использующее вышеприведенные операции.
Однако, если все это разрешить то система получится явно неподъемной. Она
включает КС-языки, для которых включение, если я не ошибаюсь, неразрешимо. В
любом случае, работать с такими широкими типами будет непросто. Поэтому, и
так мне казалось всегда, возможность выполнения названных операций надо
как-то ограничить, но не слишком сильно. И вот вчера, когда я уже ехал в
метро, мне пришла в голову идея наложить некоторое довольно элегантное
ограничение, которое и разрешимость восстановит и необходимую свободу
сохранит.
Формулировка очень простая: используем понятие L-образца - образец, в
котором нет открытых e-переменных и нет повторных. (Повторные символы тоже
запретим.) Такие образцы можно записывать без индексов переменных, например:
A s (t e t) e. Вспомним теорему В.Турчина (1974), о том, что пересечение
L-образца L с любым образцом P представимо в виде конечного объединения
образцов Pi, где каждый Pi получается из P некоторой L- подстановкой Si,
причем все Si попарно ортогональны (надеюсь, понятно, что это такое). В
частности, предикаты непустоты пересечения, включения L-образцов легко
разрешимы.
Теперь основная формулировка: описание набора типов { Ti } есть система
уравнений видa:
Ti = определение-типа
где правая часть - это система попарно непересекающихся L-образцов, в
которых каждая переменная может быть аннотирована одним из Ti. Важно, что
условие непересечения образцов проверяется без учета аннотирующих типов! Еще
парочка естественных ограничений:
1. Правая часть не может содержать (то есть состоять из единственного)
образца e. (Такой тип легко исключить.)
2. Если тип T аннотирует переменную терма (символа), то все образцы правой
части описания T должны быть сужениями переменной терма (символа).
Аннотацию e-переменной типом T будет записывать как e:T.
Примеры:
symbols = <empty> | s e:symbols
multibracket = '*' e | (e:multibracket) e
В качестве сахара, можно также разрешить в правых частях писать и выражения
от типов, например: symbols | multibracket, но с условием: вхождение имени T
(в отличие от переменной e:T) означает неободимость подставить определение T
и раскрыть результат в объединение образцов, после чего должны получиться
непересекающиеся образцы. В частности, приведенное выражение не выдерживает
этой проверки, так как оно раскрывается в набор
<empty> | s e | '*' e | (e) e
Видно, что второй и третий образцы пересекаются.
И вообще, про операции объединения и конкатенации надо сказать, что они
выполняются не всегда. Более точно:
1. Объединение: объединяем определения, и если нет пересекающихся образцов,
то ОК, иначе нельзя.
2. Конкатенация: берутся все попарные конкатенации, и если получается набор
непересекающихся L-образцов, то OK, иначе нельзя.
Когда операцию точно выполнить нельзя, надо прибегать к обобщению (как его
делать - отдельная задача).
Вот и все про определение. А теперь можно переходить к задачам.
1. Проверить включение: T1<=T2. Уверен, что проблема разрешима. Проверяя
включения в обе стороны, получаем равенство.
Воможные трудности: один и тот же тип, например симовольная строка можно
определить как слева направо, так и справа налево. Надо распознавать эти
типы как равные.
2. Тип (типовое выражение) подается на произвольный образец P для
отождествления. Надо получить типы для переменных образца P. Не знаю,
разрешимо ли это точно. Надеюсь, что да. Возможны трудности с повторными
переменными образца P - может от таковых придется отказаться (обобщая
образец P).
3. Дана полная типизация программы, то есть для каждой функции указаны типы
аргумента и результата. Проверить состоятельность.
4. Дана программа. Построить состоятельную типизацию, возможно более узкую.
5. Дана частичная типизация. Дополнить ее и проверить.
Не задачи, а конфетки! Особенно первая. Хорошо бы кто-то из молодых за это
взялся. Какие мнения?
Аркадий.
This archive was generated by hypermail 2b25 : Mon Oct 25 2004 - 21:24:58 MSD