Une variante Lisp complète de type statique est-elle possible?

Une variante Lisp complète de type statique est-elle possible? Est-il même logique que quelque chose comme ça existe? Je crois que l'une des vertus d'un langage Lisp est la simplicité de sa définition. Le typage statique compromettrait-il ce principe fondamental?

Oui, c'est très possible, bien qu'un système de type standard de type HM soit généralement le mauvais choix pour la plupart des codes Lisp / Scheme idiomatiques. Voir Typed Racket pour un langage récent qui est un "Full Lisp" (plus comme Scheme, en fait) avec un typage statique.

Si tout ce que vous vouliez était un langage de type statique qui ressemblait à Lisp, vous pourriez le faire assez facilement, en définissant un arbre de syntaxe abstrait qui représente votre langage, puis en mappant cet AST aux expressions S. Cependant, je ne pense pas que j'appellerais le résultat Lisp.

Si vous voulez quelque chose qui a réellement des caractéristiques Lisp-y en plus de la syntaxe, il est possible de le faire avec un langage typé statiquement. Cependant, il existe de nombreuses caractéristiques de Lisp sur lesquelles il est difficile d'obtenir un typage statique très utile. Pour illustrer, jetons un coup d'œil à la structure de la liste elle-même, appelée les inconvénients , qui forme le bloc de construction principal de Lisp.

Appeler les inconvénients une liste, bien que cela en (1 2 3)ressemble, est un peu un abus de langage. Par exemple, ce n'est pas du tout comparable à une liste typée statiquement, comme la liste de C ++ std::listou de Haskell. Ce sont des listes chaînées unidimensionnelles où toutes les cellules sont du même type. Lisp le permet volontiers (1 "abc" #\d 'foo). De plus, même si vous étendez vos listes de type statique pour couvrir des listes de listes, le type de ces objets nécessite que chaque élément de la liste soit une sous-liste. Comment les représenteriez-vous ((1 2) 3 4)?

Lisp conses forme un arbre binaire, avec des feuilles (atomes) et des branches (conses). De plus, les feuilles d'un tel arbre peuvent contenir n'importe quel type Lisp atomique (non contre)! La flexibilité de cette structure est ce qui rend Lisp si efficace pour gérer le calcul symbolique, les AST et la transformation du code Lisp lui-même!

Alors, comment modéliseriez-vous une telle structure dans un langage typé statiquement? Essayons-le dans Haskell, qui dispose d'un système de type statique extrêmement puissant et précis:

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

Votre premier problème va être la portée du type Atom. De toute évidence, nous n'avons pas choisi un type Atom d'une flexibilité suffisante pour couvrir tous les types d'objets que nous souhaitons utiliser dans les conses. Au lieu d'essayer d'étendre la structure de données Atom comme indiqué ci-dessus (dont vous pouvez clairement voir qu'elle est fragile), disons que nous avions une classe de type magique Atomicqui distinguait tous les types que nous voulions rendre atomiques. Ensuite, nous pourrions essayer:

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

Mais cela ne fonctionnera pas car tous les atomes de l'arbre doivent être du même type. Nous voulons qu'ils puissent différer d'une feuille à l'autre. Une meilleure approche nécessite l'utilisation des quantificateurs existentiels de Haskell :

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

Mais maintenant vous arrivez au coeur du problème. Que pouvez-vous faire avec des atomes dans ce type de structure? Quelle structure ont-ils en commun qui pourraient être modélisés Atomic a? Quel niveau de sécurité de type êtes-vous garanti avec un tel type? Notez que nous n'avons ajouté aucune fonction à notre classe de types, et il y a une bonne raison: les atomes n'ont rien de commun en Lisp. Leur supertype en Lisp est simplement appelé t(ie top).

Pour les utiliser, vous devez trouver des mécanismes pour contraindre dynamiquement la valeur d'un atome à quelque chose que vous pouvez réellement utiliser. Et à ce stade, vous avez essentiellement implémenté un sous-système typé dynamiquement dans votre langage typé statiquement! (On ne peut s'empêcher de noter un corollaire possible de la dixième règle de programmation de Greenspun .)

Notez que Haskell fournit un support pour un tel sous-système dynamique avec un Objtype, utilisé en conjonction avec un Dynamictype et une classe Typeable pour remplacer notre Atomicclasse, qui permettent de stocker des valeurs arbitraires avec leurs types, et de revenir explicitement à ces types. C'est le genre de système que vous auriez besoin d'utiliser pour travailler avec les structures Lisp contre dans leur pleine généralité.

Ce que vous pouvez également faire, c'est aller dans l'autre sens et incorporer un sous-système typé statiquement dans un langage essentiellement typé dynamiquement. Cela vous permet de bénéficier d'une vérification de type statique pour les parties de votre programme qui peuvent tirer parti d'exigences de type plus strictes. Cela semble être l'approche adoptée dans la forme limitée de contrôle de type précis de la CMUCL , par exemple.

Enfin, il est possible d'avoir deux sous-systèmes distincts, typés dynamiquement et statiquement, qui utilisent une programmation de style contrat pour aider à naviguer dans la transition entre les deux. De cette façon, le langage peut s'adapter aux utilisations de Lisp où la vérification de type statique serait plus un obstacle qu'une aide, ainsi que des utilisations où la vérification de type statique serait avantageuse. C'est l'approche adoptée par Typed Racket , comme vous le verrez dans les commentaires qui suivent.

Ma réponse, sans un degré élevé de confiance est probablement . Si vous regardez un langage comme SML, par exemple, et comparez-le avec Lisp, le noyau fonctionnel de chacun est presque identique. En conséquence, il ne semble pas que vous ayez beaucoup de mal à appliquer une sorte de typage statique au cœur de Lisp (application de fonction et valeurs primitives).

Votre question dit cependant complet , et là où je vois une partie du problème se poser, c'est l'approche du code en tant que données. Les types existent à un niveau plus abstrait que les expressions. Lisp n'a pas cette distinction - tout est "plat" dans la structure. Si nous considérons une expression E: T (où T est une représentation de son type), puis que nous considérons cette expression comme étant de simples données, alors quel est exactement le type de T ici? Eh bien, c'est une sorte! Un kind est un type d'ordre supérieur, alors allons-y et disons quelque chose à ce sujet dans notre code:

E : T :: K

Vous pourriez voir où je veux en venir. Je suis sûr qu'en séparant les informations de type du code, il serait possible d'éviter ce genre d'auto-référentialité des types, mais cela rendrait les types pas très "lisp" dans leur saveur. Il y a probablement de nombreuses façons de contourner ce problème, même si ce n'est pas évident pour moi quelle serait la meilleure.

EDIT: Oh, donc avec un peu de googler, j'ai trouvé Qi , qui semble être très similaire à Lisp sauf qu'il est typé statiquement. C'est peut-être un bon endroit pour commencer à voir où ils ont apporté des modifications pour y insérer la saisie statique.

Dylan: Extension du système de typage de Dylan pour une meilleure inférence de type et une meilleure détection des erreurs