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

[dmitry_vk]

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

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

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

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

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

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

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

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

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

Comments

[thesz.livejournal.com]

Ага, хорошая точка зрения.

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

Ну, интерпретатор, которому на вход нельзя подать программу с ошибкой типа (1+"a"), уже умеют описывать в Хаскеле: см. Generalized Algebraic Data Types, GADT. Судя по проекту "Перл 6 на Хаскеле" Pugs, с ними вполне справляются perl-hackers. ;)

Схему XML и тп вполне можно представить зависимыми типами (dependent types). По-моему, конечно, сам я в них до конца не разобрался, но все выглядит так, как будто можно.

Зависимые типы данных в Лиспе, вроде, есть, это Qi. Но его, почему-то, лисперы не используют. А даже если и используют, то молчат и не хотят рассказать нам, как им пользоваться. ;)

Но и в Qi можно допустить ошибку, в комментариях к обсуждениям это проскакивало, из-за его опциональности.

[lomeo.livejournal.com]

> Схему XML и тп вполне можно представить зависимыми типами (dependent types).

GADT достаточно. Ничего там значениями индексировать не надо, типов хватит.

[thesz.livejournal.com]

Для выбора (XPath, как я понимаю) необходимо ограничить индексы при выборе элемента из списка.

[lomeo.livejournal.com]

Ну, может быть :-)

[thesz.livejournal.com]

Вот. И поэтому, наверное, можно применить вектора и гарантированную выборку по ним.

(вместо просто кнопки Ввод нажал Табуляцию и Ввод, не знаю, зачем)

[dmitry-vk.livejournal.com]

А можно посмотреть, как это примерно выглядит? А то на словах-то все могут ;)

[lomeo.livejournal.com]

Для начала - что такое GADT и зависимые типы - понятно?

[dmitry-vk.livejournal.com]

В общих чертах — понятно.

[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.

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