В продолжение спора про лисперов...

[dmitry_vk]

Про лисп, хаскель и типизацию

Довольно интересная дискуссия развернулась в ru_lisp про лисперов, статическую типизацию и прогресс. Наверное, тоже стоит высказаться.

Во-первых, про тезис «лисперы тормозят прогресс». Отчасти это верно. Те из лисперов (лиспников), кто считает, что лисп — это вершина эволюции, не правы. Вернее, рядом с лисповской вершиной эволюции появляются новые вершины. Лисп все еще содержит множество вещей, которые в других языках не реализованы или реализованы не так естественно — например, макросы, CLOS, data-as-code и code-as-data. Но и в других языках есть вещи, которых в лиспе нет. Собственно, про это весь и спор.
Позиция некоторых лиспников о том, что «это не надо», очень странна.

Собственно, сама статическая типизация — вещь приятная. Приятно знать, что компилятор не даст сделать всякую ерунду. Все бы ничего, но на практике статическая типизация пока несовместима с лиспом. И дело даже не в том, что лисп древний. Причина несовместимости в самой основе языка: в лиспе данные — это код и код — это данные. А данные статически типизировать пока не особо умеем (хотя есть некоторые варианты). Эта же проблема есть и в других языках (и в хаскелле).

Приведу пример. Допустим, имеется xml-документ D со схемой S и XPath-выражение X. Теперь напишем функцию F, которая вернет R — результат применения произвольного XPath-выражения к документу с известной заранее схемой. Очевидно, что имея схему и XPath-выражение, мы можем сказать, что R — это не просто некий узел в дереве документа D, а мы можем сказать, какие у него есть атрибуты и потомки, типы атрибутов и так далее. Но выразить в статической системе типов мы не сможем — имеющиеся системы типов недостаточно выразительны, чтобы позволить компилятору вывести это. Приходится возвращаться к динамическим проверкам.

Другой пример. Необходимо написать интерпретатор какого-либо языка программирования. Программы заранее неизвестны, они приходят по сети. Но эти программы тоже подчиняются некоторым ограничениям. Например, у них есть вполне определенная точка входа. Аналогично, как это указать в статической системе типов? Опять, придется обращаться к динамическим проверкам.

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

Вывод: статическая типизация — это хорошо. Но не везде ее получается реализовать. И если есть статическая типизация, то сделать динамическую поверх нее можно. А наоборот — нет.

В современных реализациях лиспа (например, sbcl), увы, есть только компромиссное решение — обнаруженные несоответствия типов низведены до уровня предупреждений.
Языки сближаются, и новые теории могут позволить сделать статическую типизацию совместимой с лиспом.

Comments

[lomeo.livejournal.com]

Сорри за долгое молчание. Ну, если что такое GADT понятно, то непонятно, что же собственно непонятно :-) Надо полагать, понятно, как выражать в типах некоторые ограничения?

- последовательность (простой конструктор данных в ADT)
- maxOccurs="unbounded" - список
- minOccurs="0" maxOccurs="1" - Maybe
- maxOccurs="n" - ограничение в DT на вектор Vec n a.
- всякие positive и date можно выразить просто типом

и т.д.?

[dmitry-vk.livejournal.com]

Про ограничения понятно.
Непонятно, как оно в коде выглядит и как работает. Какая будет сигнатура функции обработки XPath-выражения (ограничимся случаем, когда возвращается только один узел)?
processXPath :: XPathExpression -> XmlTree -> XmlNode
Скажем, компилятор изначально не знает про xml-схемы. Как его «научить» проверять такие типы?

[lomeo.livejournal.com]

Ну, вообще то, я про схему XML говорил. Про XPath особо не думал.
Общие мысли - для начала нужно определить, что мы хотим проверять во время компиляции и это выносить в тип, например, если мы хотим проверять, что длина абсолютного XPathExpression не превышает расстояние от корня до самого глубокого узла, то эту информацию надо выносить в эти два типа, а в processXPath ставить ограничение.

[dmitry-vk.livejournal.com]

То, что схему можно представить, сомнений никаких нету.
Что хочется проверить: скажем, проверить, что у узла, являющегося результатом применения XPath к документу с заданной схемой, будут иметься определенные атрибуты (с определенными типа). Конечно, проверять нужно только то, что можно проверить статически.
Правильно я понимаю, что в коде это может выглядеть вроде нечто такого (как выглядит синтаксис с dependent types, я не знаю)?
processXPath :: (XPathExpression e) -> (XmlSchema s) -> XmlTree -> (XmlNode x) where (hasAttributes x (attributesBySchema s e))
где hasAttributes x a удостоверяет, что у x есть атрибуты из набора атрибутов a, а attributesBySchema s e возвращает, какие атрибуты должны быть у результата выражения e в схеме s.

Только пока непонятно, как это работает:) В смысле, непонятно, как проверяться будет.