Действительно ли полный Lisp со статическим контролем типов различен возможный?

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

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

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