Une variante de Lisp complet à typage statique est-elle possible ?

Question

Une variante de Lisp complet à typage statique est-elle possible ? L'existence d'une telle variante a-t-elle un sens ? 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 de base ?

Answer 1

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

Answer 2

Si tout ce que vous vouliez était un langage statiquement typé qui ressemblait à Lisp, vous pouvez le faire assez facilement, en définissant un arbre syntaxique abstrait qui représente votre langage, puis en faisant correspondre cet AST aux expressions S. Cependant, je ne pense pas que j'appellerais le résultat Lisp.

Si vous voulez quelque chose qui a les caractéristiques de Lisp en plus de la syntaxe, il est possible de le faire avec un langage statiquement typé. Cependant, il existe de nombreuses caractéristiques de Lisp qui sont difficiles à utiliser pour le typage statique. Pour illustrer cela, regardons la structure de liste elle-même, appelée la structure contre qui constitue le principal élément de base de Lisp.

Appeler les contre une liste, cependant (1 2 3) en a l'air, est un peu un terme impropre. Par exemple, il n'est pas du tout comparable à une liste typée statiquement, comme la liste C++. std::list ou la liste de Haskell. Il s'agit de listes liées unidimensionnelles où toutes les cellules sont du même type. Lisp permet heureusement (1 "abc" #\d 'foo) . De plus, même si vous étendez vos listes à typage statique pour couvrir les listes de listes, le type de ces objets exige que chaque L'élément de la liste est une sous-liste. Comment représenter ((1 2) 3 4) en eux ?

Les conses de Lisp forment 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-cons) ! La flexibilité de cette structure est ce qui rend Lisp si bon pour gérer le calcul symbolique, les ASTs, et la transformation du code Lisp lui-même !

Alors comment modéliser une telle structure dans un langage statiquement typé ? Essayons en Haskell, qui possède un système de types statiques 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 sera la portée du type Atom. Il est clair que nous n'avons pas choisi un type Atom suffisamment flexible pour couvrir tous les types d'objets que nous voulons faire circuler dans les conses. Au lieu d'essayer d'étendre la structure de données Atom comme indiqué ci-dessus (ce qui, comme vous pouvez le constater, est fragile), disons que nous avons une classe de type magique Atomic qui distinguait tous les types que nous voulions rendre atomiques. Alors nous pourrions essayer :

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

Mais cela ne fonctionnera pas car il faut que tous les atomes de l'arbre soient de la catégorie même type. Nous voulons qu'ils puissent différer d'une feuille à l'autre. Une meilleure approche nécessite l'utilisation de la fonction quantificateurs existentiels :

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

Mais vous arrivez maintenant au cœur du problème. Que pouvez-vous faire avec des atomes dans ce type de structure ? Quelle est la structure qu'ils ont en commun et qui pourrait être modélisée avec Atomic a ? Quel est le niveau de sécurité de type garanti avec un tel type ? Notez que nous n'avons pas ajouté de fonctions à notre classe de types, et ce pour une bonne raison : les atomes n'ont rien en commun en Lisp. Leur supertype en Lisp est simplement appelé t (c'est-à-dire en haut).

Pour pouvoir les utiliser, il faudrait 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 fondamentalement implémenté un sous-système dynamiquement typé dans votre langage statiquement typé ! (On ne peut s'empêcher de noter un possible corollaire à La dixième règle de programmation de Greenspun .)

Notez que Haskell fournit un support pour une telle fonction sous-système dynamique avec un Obj utilisé en conjonction avec un Dynamic et un Classe de type pour remplacer notre Atomic qui permettent de stocker des valeurs arbitraires avec leurs types, et une coercition explicite à partir de ces types. C'est le genre de système qu'il faudrait utiliser pour travailler avec les structures de cons Lisp dans toute leur généralité.

Vous pouvez également faire l'inverse et intégrer un sous-système à typage statique dans un langage essentiellement à typage dynamique. Cela vous permet de bénéficier de la vérification statique des types 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 CMUCL de un contrôle précis des types par exemple.

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

Answer 3

Ma réponse, sans grand degré de confiance, est la suivante probablement . Si vous regardez un langage comme SML, par exemple, et que vous le comparez à Lisp, le noyau fonctionnel de chacun est presque identique. Par conséquent, il ne semble pas que vous auriez beaucoup de difficultés à appliquer une sorte de typage statique au noyau de Lisp (application de fonctions et valeurs primitives).

Votre question dit bien complet Cependant, et là où je vois une partie du problème, 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), et que nous considérons ensuite cette expression comme une simple donnée, quel est exactement le type de T ici ? Eh bien, c'est un type ! Un type est un type d'ordre supérieur, alors allons-y et disons quelque chose à ce sujet dans notre code :

E : T :: K

Vous voyez peut-être où je veux en venir. Je suis sûr qu'en séparant les informations sur les types du code, il serait possible d'éviter ce genre d'autoréférence des types, mais cela rendrait les types pas très "lisp" dans leur saveur. Il existe probablement de nombreuses façons de contourner ce problème, mais je ne vois pas quelle serait la meilleure.

EDIT : Oh, donc avec un peu de google, j'ai trouvé Qi qui semble être très similaire à Lisp, sauf qu'il est typographié de manière statique. C'est peut-être un bon endroit pour commencer à voir où ils ont fait des changements pour obtenir le typage statique.

Answer 4

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