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

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

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

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

Называть минусы списком, хотя (1 2 3) и выглядит так, - это немного неправильное употребление. Например, он совершенно не сопоставим со статически типизированным списком, таким как std::list в C ++ или список Haskell. Это одномерные связанные списки, в которых все ячейки одного типа. Lisp с радостью разрешает (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 class для замены нашего Atomic класса, который позволяет сохранять произвольные значения с их типами и явным приведением обратно из этих типов. Это та система, которую вам нужно использовать для работы со структурами cons в Лиспе во всей их общности.

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

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

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

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

E : T :: K

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

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

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