Déduire les types de raffinement

Au travail, j'ai été chargé de déduire des informations de type sur un langage dynamique. Je réécris des séquences d'instructions en imbriquéeslet expressions , comme ceci:

return x; Z            =>  x
var x; Z               =>  let x = undefined in Z
x = y; Z               =>  let x = y in Z
if x then T else F; Z  =>  if x then { T; Z } else { F; Z }

Étant donné que je pars d'informations générales sur les types et que j'essaye d'en déduire des types plus spécifiques, le choix naturel est les types de raffinement. Par exemple, l'opérateur conditionnel renvoie une union des types de ses branches vraie et fausse. Dans les cas simples, cela fonctionne très bien.

Cependant, j'ai rencontré un problème lorsque j'essayais de déduire le type de ce qui suit:

function g(f) {
  var x;
  x = f(3);
  return f(x);
}

Qui est réécrit pour:

\f.
  let x = undefined in
    let x = f 3 in
      f x

$\mathtt{f} : \mathtt{Int} \to \mathtt{Int}$$\mathtt{g} : (\mathtt{Int} \to \mathtt{Int}) \to \mathtt{Int}$

$$\mathtt{g} : \forall \tau_1 \tau_2. \:(\mathtt{Int} \to \tau_1 \land \tau_1 \to \tau_2) \to \tau_2$$

J'utilise déjà des dépendances fonctionnelles pour résoudre le type d'un +opérateur surchargé , j'ai donc pensé que c'était un choix naturel de les utiliser pour résoudre le type de l' fintérieur g. Autrement dit, les types de fdans toutes ses applications déterminent ensemble le type de g. Cependant, il s'avère que les fonds ne se prêtent pas très bien à un nombre variable de types de sources.

Quoi qu'il en soit, l'interaction du polymorphisme et du typage de raffinement est problématique. Alors, y a-t-il une meilleure approche qui me manque? Je digère actuellement les «types de raffinement pour ML» et j'apprécierais plus de littérature ou d'autres pointeurs.

Vous êtes tombé sur le fait que l'inférence des invariants statiques pour les langages d'ordre supérieur est assez difficile en pratique, en plus d'être indécidable en théorie. Je ne sais pas quelle est la réponse définitive à votre question, mais notez plusieurs choses:

• Les types de polymorphisme et de raffinement se comportent mal ensemble, comme vous l'avez noté, en particulier la notion de type le plus général est perdue. Une conséquence de cela est que les analyses basées sur des types de raffinement en présence de polymorphisme peuvent avoir besoin de choisir entre l'analyse de programme entier (par opposition à l'analyse de composition) et l'utilisation d'heuristiques pour décider quel type vous souhaitez attribuer à votre programme.

• Il existe une forte relation entre la déduction des types de raffinement et:

  1. Calcul de l'interprétation abstraite de votre programme

  2. Calcul des invariants de boucle dans un langage impératif.

Dans cet esprit, voici quelques références désorganisées sur l'inférence des types de raffinement. Notez qu'il existe de nombreuses variantes de types de raffinement: j'ai tendance à être plus intéressé par les raffinements de types de données inductifs, donc cette liste peut être biaisée dans cette direction.

1. Commençons par les classiques: Interprétation abstraite relationnelle des programmes fonctionnels d'ordre supérieur par Cousot & Cousot. Cela explique comment étendre l'interprétation abstraite aux programmes d'ordre supérieur en utilisant la sémantique relationnelle.

2. Types liquides par Rhondon, Kawaguchi et Jhala. C'est un travail très évolué, qui combine HM et un type de raffinement de prédicat pour déduire des annotations de sécurité (contrôles liés au tableau par exemple) pour les programmes de style ML. L'inférence se déroule en 2 étapes; le premier est l'inférence HM des annotations de type, qui guident le choix des raffinements à effectuer.

3. Je devrais probablement aussi mentionner les travaux de Fournet, Swarmy, Chen, Strub ... sur $F^*$, une extension de $F^\#$qui semble similaire à l'approche des types liquides, mais dans le but de vérifier les protocoles et algorithmes cryptographiques pour le calcul distribué. Je ne sais pas combien de travaux publiés il y a sur l'inférence des annotations dans ce cas.

4. Il y a un bon article de Chin et Khoo sur l'inférence d'un type spécifique de types de raffinement: les types avec des annotations de taille.

5. Le langage de programmation ATS est un système qui permet divers raffinements et fournit des installations pour écrire des programmes avec eux. Cependant, les annotations peuvent être arbitrairement complexes (et donc indécidables) et peuvent donc nécessiter une interaction de l'utilisateur. Je crois qu'il existe une forme d'inférence pour ces types, je ne sais pas quel article recommander cependant.

6. Dernier point, mais non des moindres , l' algorithme de produit cartésien , par Ole Agesen. Sans mentionner explicitement les types de raffinement, cela semble être le travail le plus proche de la résolution du problème que vous semblez avoir. Ne vous laissez pas berner par la mention du polymorphisme paramétrique dans l'abstrait: ils cherchent à déduire des types concrets , qui ne sont que des tuples de types atomiques possibles. L'accent est mis sur l'efficacité. Je recommande d'abord de lire cet article pour voir s'il résout votre problème.

Note latérale: l'inférence de type en présence de types d'intersection peut être très indécidable: dans la forme la plus simple, $\lambda$-les termes de type intersection sont exactement les termes fortement normalisants. Marchez doucement autour d'eux :)