programming languages - ¿Es posible una variante de Lisp completa de tipo estático?
programming-languages static-typing (4)
¿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?
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 sí dice completa , 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! Un tipo es un tipo de orden superior, así que simplemente continuemos y digamos algo al respecto en nuestro código:
E : T :: K
Puede ver 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: Oh, 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í.
Sí, es muy posible, aunque un sistema tipo HM estándar suele ser la opción incorrecta para la mayoría del código Idiom / 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.
Si todo lo que quería era un lenguaje estáticamente tipificado que se pareciera a Lisp, podría hacerlo con bastante facilidad, definiendo un árbol de sintaxis abstracta que represente su lenguaje y luego mapee ese AST a expresiones S. 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 contras , que forma el bloque de construcción primario de Lisp.
Sin embargo, llamar a los contras una lista (1 2 3) parece uno, es un nombre un tanto inapropiado. Por ejemplo, no es para nada comparable a una lista estáticamente tipada, como la std::list C ++ 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 extiende sus listas de tipo estático para cubrir listas de listas, el tipo de estos objetos requiere que cada elemento de la lista sea una sublista. ¿Cómo representarías ((1 2) 3 4) en ellos?
Lisp se compone de un árbol binario, con hojas (átomos) y ramas (conses). 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ías esa estructura en un lenguaje estáticamente tipado? Probémoslo 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 indica más 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 intentar:
class Atomic a where ?????
data Atomic a => Cons a = CCons Cons Cons
| CAtom a
Pero esto no funcionará porque requiere que todos los átomos en el árbol sean del mismo tipo. Queremos que puedan diferir de una hoja a otra. Un mejor enfoque requiere el uso de los cuantificadores existenciales de Haskell:
class Atomic a where ?????
data Cons = CCons Cons Cons
| forall a. Atomic a => CAtom a
Pero ahora llegas al quid de la cuestión. ¿Qué puedes hacer con los átomos en este tipo de estructura? ¿Qué estructura tienen en común que pueda 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ías que idear mecanismos para forzar dinámicamente el valor de un átomo a algo que realmente puedas usar. Y en ese punto, básicamente has implementado un subsistema de tipo dinámico dentro de tu lenguaje estáticamente tipado. (No se puede dejar de notar un posible corolario de la Décima Regla de Programación de Greenspun ).
Tenga en cuenta que Haskell proporciona soporte para dicho subsistema dinámico con un tipo Obj , utilizado junto con un tipo Dynamic y una Clase Typeable para reemplazar nuestra clase Atomic , que permite almacenar valores arbitrarios con sus tipos, y una coacción explícita de aquellos 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 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 comprobación precisa de tipos de CMUCL, por ejemplo.
Finalmente, existe la posibilidad de tener dos subsistemas separados, tipeados dinámicamente y estáticamente, que usan programación estilo 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án en los comentarios que siguen.