¿Es posible una variante de Lisp completa de tipo estático?

Question

¿Es posible una variante de Lisp completa de tipo estático? ¿Tiene sentido que algo así exista? Creo que una de las virtudes de un lenguaje Lisp es la simplicidad de su definición. ¿La escritura estática comprometería este principio básico?

Answer 1

Mi respuesta, sin un alto grado de confianza es probablemente. Si observa un lenguaje como SML, por ejemplo, y lo compara con Lisp, el núcleo funcional de cada uno es casi idéntico. Como resultado, no parece que tenga muchos problemas para aplicar algún tipo de tipeo estático al núcleo de Lisp (aplicación de función y valores primitivos).

Sin embargo, su pregunta dice full, y donde veo que parte del problema es el enfoque del código como datos. Los tipos existen en un nivel más abstracto que las expresiones. Lisp no tiene esta distinción: todo es "plano" en la estructura. Si consideramos alguna expresión E: T (donde T es una representación de su tipo), y luego consideramos que esta expresión es simple ol 'data, entonces ¿cuál es exactamente el tipo de T aquí? Bueno, es un tipo! Una especie es un tipo de orden superior, así que vamos a seguir adelante y decir algo sobre eso en nuestro código:

E : T :: K 

Es posible que vea a dónde voy con esto. Estoy seguro de que al separar la información de tipo del código, sería posible evitar este tipo de autorreferencialidad de los tipos, sin embargo, eso haría que los tipos no "cemen" en su sabor. Probablemente haya muchas formas de evitar esto, aunque no es obvio para mí cuál sería la mejor.

EDITAR: Ah, así que con un poco de Google, encontré Qi, que parece ser muy similar a Lisp, excepto que está tipado estáticamente. Tal vez sea un buen lugar para comenzar a ver dónde hicieron los cambios para obtener la escritura estática allí.

Answer 2

Sí, es muy posible, aunque un sistema tipo HM estándar es generalmente la opción incorrecta para la mayoría del código de Lisp/Scheme idiomático. Ver Typed Racket para un lenguaje reciente que es un "Full Lisp" (más parecido al Scheme, en realidad) con tipado estático.

Answer 3

Dylan: http://visualization.dylan-user.org/diploma.pdf

Answer 4

Si todo lo que quería era un lenguaje de tipos estáticos que parecía Lisp, se puede hacer eso con bastante facilidad, mediante la definición de un árbol de sintaxis abstracta que representa el idioma y luego la cartografía que AST S-expresiones. Sin embargo, no creo que llamaría al resultado Lisp.

Si desea algo que realmente tenga características Lisp-y además de la sintaxis, es posible hacerlo con un lenguaje estáticamente tipado. Sin embargo, hay muchas características para Lisp de las que es difícil obtener mucha escritura estática útil. Para ilustrar, echemos un vistazo a la estructura de la lista en sí, llamada cons, que forma el bloque de construcción primario de Lisp.

Llamar a los contras una lista, aunque (1 2 3) parece uno, es un nombre poco apropiado. Por ejemplo, no es para nada comparable a una lista estáticamente tipada, como la de C++ std::list o la lista de Haskell. Esas son listas unidimensionales vinculadas donde todas las celdas son del mismo tipo. Lisp felizmente permite (1 "abc" #\d 'foo). Además, incluso si amplía sus listas de tipo estático para cubrir las listas de listas, el tipo de estos objetos requiere que cada elemento de la lista sea una sublista. ¿Cómo representarías a ((1 2) 3 4) en ellos?

Lisp se compone de un árbol binario, con hojas (átomos) y ramas (consigna). Además, ¡las hojas de dicho árbol pueden contener cualquier tipo de Lisp atómico (sin contras)! ¡La flexibilidad de esta estructura es lo que hace que Lisp sea tan bueno en el manejo de computación simbólica, ASTs, y la transformación del código Lisp en sí mismo!

Entonces, ¿cómo modelaría esa estructura en un lenguaje estáticamente tipado? Vamos a intentarlo en Haskell, que tiene un sistema de tipo estático extremadamente potente y preciso:

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

Su primer problema va a ser el alcance del tipo Atom. Claramente, no hemos escogido un tipo de Atom de suficiente flexibilidad para cubrir todos los tipos de objetos que queremos lanzar en conses. En lugar de tratar de ampliar la estructura de datos de Atom como se menciona arriba (que se puede ver claramente que es frágil), digamos que teníamos una clase de tipo mágico Atomic que distinguía todos los tipos que queríamos hacer atómicos. Entonces podríamos tratar:

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

Pero esto no funcionará, ya que requiere que todos los átomos en el árbol para ser del mismo tipo . Queremos que puedan diferir de una hoja a otra. Un mejor enfoque requiere el uso de cuantificadores existenciales de Haskell:

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

Pero ahora se llega al quid de la cuestión. ¿Qué puedes hacer con los átomos en este tipo de estructura? ¿Qué estructura tienen en común que podría modelarse con Atomic a? ¿Qué nivel de seguridad de tipo tiene garantizado con dicho tipo? Tenga en cuenta que no hemos agregado ninguna función a nuestra clase de tipos, y hay una buena razón: los átomos no tienen nada en común en Lisp. Su supertipo en Lisp simplemente se llama t (es decir, arriba).

Para usarlos, tendría que idear mecanismos para forzar dinámicamente el valor de un átomo para algo que realmente pueda usar. Y en ese punto, básicamente has implementado un subsistema de tipo dinámico dentro de tu lenguaje estáticamente tipado. (Uno no puede dejar de notar un posible corolario de Greenspun's Tenth Rule of Programming.)

Tenga en cuenta que Haskell proporciona soporte para apenas tal dynamic subsystem con un tipo de Obj, se utiliza junto con un tipo Dynamic y una Typeable class para reemplazar nuestra clase Atomic, que permiten valores arbitrarios para almacenar con sus tipos, y coerción explícita de esos tipos. Ese es el tipo de sistema que necesitarías usar para trabajar con las estructuras cons de Lisp en su generalidad completa.

Lo que también puede hacer es ir hacia el otro lado, e insertar un subsistema tipado estáticamente dentro de un lenguaje esencialmente con tipado dinámico. Esto le permite el beneficio de la verificación de tipo estático para las partes de su programa que pueden aprovechar requisitos de tipo más estrictos. Este parece ser el enfoque adoptado en la forma limitada de CMUCL precise type checking, por ejemplo.

Finalmente, existe la posibilidad de tener dos subsistemas separados, tipeados dinámicamente y estáticamente, que usan programación de estilo de contrato para ayudar a navegar la transición entre los dos. De esta forma, el lenguaje puede adaptarse a los usos de Lisp donde la comprobación de tipos estáticos sería más un obstáculo que una ayuda, así como también usos donde la comprobación de tipos estáticos sería ventajosa. Este es el enfoque adoptado por Typed Racket, como verá en los comentarios que siguen.