Возможен ли статически типизированный полный вариант Лиспа?

Возможен ли статически типизированный полный вариант Лиспа? Есть ли вообще смысл в существовании чего-то подобного? Я считаю, что одним из достоинств языка Lisp является простота его определения. Подорвет ли статическая типизация этот основной принцип?

Да, это очень возможно, хотя стандартная система типов в стиле HM обычно является неправильным выбором для большинства идиоматического кода Lisp / Scheme. См. Typed Racket, чтобы узнать о новом языке, который является «Full Lisp» (на самом деле больше похожим на Scheme) со статической типизацией.

Если все, что вам нужно, это статически типизированный язык, похожий на Lisp, вы могли бы сделать это довольно легко, определив абстрактное синтаксическое дерево, представляющее ваш язык, и затем сопоставив этот AST с S-выражениями. Однако я не думаю, что назову результат Лиспом.

Если вам нужно что-то, что действительно имеет характеристики Lisp-y, помимо синтаксиса, это можно сделать с помощью статически типизированного языка. Однако у Лиспа есть много характеристик, из которых трудно извлечь много полезной статической типизации. Чтобы проиллюстрировать это, давайте взглянем на саму структуру списка, называемую cons , которая формирует основной строительный блок Lisp.

Называть минусы списком, хотя и (1 2 3)выглядит так, но неправильно. Например, он совершенно не сопоставим со статически типизированным списком, таким как список C ++ std::listили Haskell. Это одномерные связанные списки, в которых все ячейки одного типа. Лисп с радостью позволяет (1 "abc" #\d 'foo). Кроме того, даже если вы расширяете свои списки со статической типизацией до списков-списков, тип этих объектов требует, чтобы каждый элемент списка был подсписком. Как бы вы ((1 2) 3 4)в них представились ?

Конусы Лиспа образуют двоичное дерево с листьями (атомами) и ветвями (конусами). Кроме того, листья такого дерева могут содержать любой атомарный (не являющийся минусом) тип Лиспа! Гибкость этой структуры делает Lisp таким хорошим в обработке символьных вычислений, AST и преобразовании самого кода Lisp!

Итак, как бы вы смоделировали такую ​​структуру на языке со статической типизацией? Давайте попробуем это в Haskell, который имеет чрезвычайно мощную и точную систему статических типов:

type Symbol = String
data Atom = ASymbol Symbol | AInt Int | AString String | Nil
data Cons = CCons Cons Cons 
            | CAtom Atom

Ваша первая проблема будет связана с типом Atom. Ясно, что мы не выбрали тип Atom, обладающий достаточной гибкостью, чтобы охватить все типы объектов, которые мы хотим использовать в качестве аргументов. Вместо того, чтобы пытаться расширить структуру данных Atom, как указано выше (которая, как вы ясно видите, является хрупкой), предположим, что у нас есть класс магического типа, Atomicкоторый различает все типы, которые мы хотели сделать атомарными. Тогда мы могли бы попробовать:

class Atomic a where ?????
data Atomic a => Cons a = CCons Cons Cons 
                          | CAtom a

Но это не сработает, потому что для этого требуется, чтобы все атомы в дереве были одного типа. Мы хотим, чтобы они отличались от листа к листу. Лучший подход требует использования квантификаторов существования Haskell :

class Atomic a where ?????
data Cons = CCons Cons Cons 
            | forall a. Atomic a => CAtom a 

Но теперь вы подошли к сути дела. Что вы можете делать с атомами в такой структуре? Какая у них общая структура, с которой можно было бы моделировать Atomic a? Какой уровень типовой безопасности вам гарантирован с таким типом? Обратите внимание, что мы не добавили никаких функций в наш класс типов, и на то есть веская причина: у атомов нет ничего общего в Лиспе. Их супертип в Лиспе просто называется t(т.е. верхний).

Чтобы использовать их, вам нужно было бы разработать механизмы для динамического приведения значения атома к тому, что вы действительно можете использовать. И в этот момент вы в основном реализовали подсистему с динамической типизацией в своем статически типизированном языке! (Нельзя не отметить возможное следствие десятого правила программирования Гринспана .)

Обратите внимание, что Haskell обеспечивает поддержку именно такой динамической подсистемы с Objтипом, используемым в сочетании с Dynamicтипом и классом Typeable для замены нашего Atomicкласса, что позволяет сохранять произвольные значения с их типами и явным приведением обратно из этих типов. Это та система, которую вам нужно использовать для работы со структурами cons в Лиспе во всей их общности.

Что вы также можете сделать, так это пойти другим путем и встроить статически типизированную подсистему в по существу динамически типизированный язык. Это дает вам преимущество проверки статического типа для частей вашей программы, которые могут использовать преимущества более строгих требований к типу. Похоже, что это подход, используемый, например, в ограниченной форме точной проверки типов в CMUCL .

Наконец, есть возможность иметь две отдельные подсистемы, динамически и статически типизированные, которые используют программирование в контрактном стиле, чтобы облегчить переход между ними. Таким образом, язык может приспособиться к использованию Лиспа, где проверка статического типа будет больше помехой, чем помощью, а также использования, где проверка статического типа была бы полезной. Это подход, используемый Typed Racket , как вы увидите из последующих комментариев.

Мой ответ, без особой уверенности, наверное . Если вы посмотрите, например, на такой язык, как SML, и сравните его с Lisp, функциональное ядро ​​каждого из них практически идентично. В результате не похоже, что у вас будет много проблем с применением статической типизации к ядру Lisp (приложение функций и примитивные значения).

Ваш вопрос действительно говорит полный , и где я вижу, что некоторые из проблем возникают, это подход «код как данные». Типы существуют на более абстрактном уровне, чем выражения. Lisp не имеет этого различия - все «плоское» по структуре. Если мы рассмотрим какое-то выражение E: T (где T - некоторое представление его типа), а затем мы будем рассматривать это выражение как простые старые данные, то что именно здесь является типом T? Ну это вид! Тип - это тип более высокого порядка, поэтому давайте просто скажем что-нибудь об этом в нашем коде:

E : T :: K

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

РЕДАКТИРОВАТЬ: Итак, немного погуглив, я нашел Qi , который очень похож на Lisp, за исключением того, что он статически типизирован. Возможно, это хорошее место, чтобы увидеть, где они внесли изменения, чтобы добавить статическую типизацию.

Дилан: Расширение системы типов Дилана для лучшего вывода типов и обнаружения ошибок