É possível uma variante completa do Lisp estaticamente tipada?

É possível uma variante completa do Lisp estaticamente tipada? Faz sentido que algo assim exista? Acredito que uma das virtudes de uma linguagem Lisp é a simplicidade de sua definição. A tipagem estática comprometeria este princípio básico?

Sim, é muito possível, embora um sistema de tipo de estilo HM padrão seja geralmente a escolha errada para a maioria dos códigos Lisp / Scheme idiomáticos. Veja Typed Racket para uma linguagem recente que é um "Full Lisp" (mais como Scheme, na verdade) com tipagem estática.

Se tudo o que você quisesse era uma linguagem com tipagem estática que parecia Lisp, você poderia fazer isso facilmente, definindo uma árvore de sintaxe abstrata que representa sua linguagem e, em seguida, mapeando esse AST para S-expressões. No entanto, não acho que chamaria o resultado de Lisp.

Se você quiser algo que realmente tenha características Lisp-y além da sintaxe, é possível fazer isso com uma linguagem de tipo estático. No entanto, existem muitas características do Lisp das quais é difícil obter muita tipagem estática útil. Para ilustrar, vamos dar uma olhada na própria estrutura da lista, chamada de contras , que forma o bloco de construção principal do Lisp.

Chamar os contras de lista, embora (1 2 3)pareça uma, é um pouco incorreto. Por exemplo, não é nada comparável a uma lista digitada estaticamente, como a lista de C ++ std::listou Haskell. Essas são listas vinculadas unidimensionais em que todas as células são do mesmo tipo. Lisp felizmente permite (1 "abc" #\d 'foo). Além disso, mesmo se você estender suas listas de tipo estático para cobrir listas de listas, o tipo desses objetos requer que cada elemento da lista seja uma sublista. Como você representaria ((1 2) 3 4)neles?

Os conses Lisp formam uma árvore binária, com folhas (átomos) e ramos (conses). Além disso, as folhas de tal árvore podem conter qualquer tipo Lisp atômico (não cons)! A flexibilidade dessa estrutura é o que torna o Lisp tão bom em lidar com computação simbólica, ASTs e transformar o próprio código Lisp!

Então, como você modelaria tal estrutura em uma linguagem de tipagem estática? Vamos tentar em Haskell, que tem um sistema de tipo estático extremamente poderoso e preciso:

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

Seu primeiro problema será o escopo do tipo Atom. Claramente, não escolhemos um tipo de Atom com flexibilidade suficiente para cobrir todos os tipos de objetos que desejamos usar como complemento. Em vez de tentar estender a estrutura de dados Atom conforme listado acima (que você pode ver claramente que é frágil), digamos que tivéssemos uma classe de tipo mágico Atomicque distinguia todos os tipos que queríamos tornar atômicos. Então podemos tentar:

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

Mas isso não funcionará porque requer que todos os átomos da árvore sejam do mesmo tipo. Queremos que eles possam variar de folha para folha. Uma abordagem melhor requer o uso de quantificadores existenciais de Haskell :

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

Mas agora você chega ao cerne da questão. O que você pode fazer com átomos neste tipo de estrutura? Que estrutura eles têm em comum que poderia ser modelada Atomic a? Que nível de segurança de tipo você garante com esse tipo? Observe que não adicionamos nenhuma função à nossa classe de tipo, e há um bom motivo: os átomos não compartilham nada em comum no Lisp. Seu supertipo em Lisp é simplesmente chamadot (ou seja, top).

Para usá-los, você teria que criar mecanismos para forçar dinamicamente o valor de um átomo a algo que você possa realmente usar. E nesse ponto, você basicamente implementou um subsistema tipado dinamicamente dentro de sua linguagem tipada estaticamente! (Não se pode deixar de notar um possível corolário da Décima Regra de Programação de Greenspun .)

Observe que Haskell fornece suporte apenas para um subsistema dinâmico com um Objtipo, usado em conjunto com um Dynamictipo e uma classe Tipável para substituir nossoAtomic classe, que permite que valores arbitrários sejam armazenados com seus tipos, e a coerção explícita desses tipos. Esse é o tipo de sistema que você precisa usar para trabalhar com estruturas de cons Lisp em sua generalidade completa.

O que você também pode fazer é seguir o outro caminho e incorporar um subsistema de tipo estático dentro de uma linguagem de tipo essencialmente dinâmico. Isso permite o benefício da verificação de tipo estático para as partes do seu programa que podem tirar proveito de requisitos de tipo mais rigorosos. Esta parece ser a abordagem adotada na forma limitada do CMUCL de verificação de tipo preciso , por exemplo.

Finalmente, existe a possibilidade de ter dois subsistemas separados, com tipos estáticos e dinâmicos, que usam a programação no estilo de contrato para ajudar a navegar na transição entre os dois. Dessa forma, a linguagem pode acomodar usos do Lisp onde a verificação de tipo estática seria mais um obstáculo do que uma ajuda, bem como usos onde a verificação de tipo estática seria vantajosa. Essa é a abordagem feita pelo Typed Racket , como você verá nos comentários a seguir.

Minha resposta, sem um alto grau de confiança é provavelmente . Se você olhar para uma linguagem como SML, por exemplo, e compará-la com Lisp, o núcleo funcional de cada uma é quase idêntico. Como resultado, não parece que você teria muitos problemas para aplicar algum tipo de tipagem estática ao núcleo do Lisp (aplicativo de função e valores primitivos).

Porém, sua pergunta diz completo , e vejo alguns dos problemas surgindo na abordagem de código como dados. Os tipos existem em um nível mais abstrato do que as expressões. Lisp não tem essa distinção - tudo é "plano" na estrutura. Se considerarmos alguma expressão E: T (onde T é alguma representação de seu tipo), e então considerarmos essa expressão como sendo simples dados, então qual é exatamente o tipo de T aqui? Bem, é um tipo! Um tipo é um tipo de pedido superior, então vamos prosseguir e dizer algo sobre isso em nosso código:

E : T :: K

Você pode ver onde estou indo com isso. Tenho certeza de que separando as informações de tipo do código seria possível evitar esse tipo de autorreferencialidade de tipos, no entanto, isso tornaria os tipos não muito "ceceios" em seu sabor. Provavelmente, existem muitas maneiras de contornar isso, embora não seja óbvio para mim qual seria a melhor.

EDIT: Oh, então com um pouco de pesquisa no Google, encontrei Qi , que parece ser muito semelhante ao Lisp, exceto que é digitado estaticamente. Talvez seja um bom lugar para começar a ver onde eles fizeram alterações para obter a tipagem estática lá.

Dylan: Estendendo o sistema de tipos de Dylan para melhor inferência de tipos e detecção de erros