Generalised recursion and type inference for intersection types

Récursion généralisée et inférence de types avec intersection

Pascal Zimmer (1)

1 MIMOSA - Migration and mobility : semantics and applications

In the first part, we define a new programming language with a functional core and generalised recursion, by using Boudol's type system with degrees to rule out unsafe recursions. The language is extended first with recursive records, then with mixins, allowing the programmer to fully mix functional and object-oriented paradigms. We also present an implementation, MlObj, and an abstract machine for execution.

In a second part, we design a new inference algorithm for intersection type systems, on an extension of the lambda-calculus. After proving its correctness, we study its generalisation to references and recursion, we compare it with existing inference algorithms, mainly System I, and we show that its finite rank version becomes decidable.

Dans une première partie, nous définissons un nouveau langage à base fonctionnelle et avec récursion généralisée, en utilisant le système de types avec degrés de Boudol pour éliminer les récursions dangereuses. Ce langage est ensuite étendu par des enregistrements récursifs, puis par des mixins, permettant ainsi de mêler totalement les paradigmes fonctionnels et objets. Nous présentons également une implémentation, MlObj, ainsi que la machine abstraite servant à son exécution.

Dans une deuxième partie, nous présentons un nouvel algorithme d'inférence pour les systèmes de types avec intersection, dans le cadre d'une extension du lambda-calcul. Après avoir prouvé sa correction, nous étudions sa généralisation aux références et à la récursion, nous le comparons aux algorithmes d'inférence déjà existants, notamment à celui de Système I, et nous montrons qu'il devient décidable à rang fini.

Mots clés: lambda-calculus; object-oriented programming; intersection types; type inference; Klop calculus

Mots clés: lambda-calcul; ML; récursion; programmation orientée objet; mixins; types avec intersection; inférence de types; calcul de Klop

Domaines: Autre [cs.OH]

Pascal Zimmer. Récursion généralisée et inférence de types avec intersection. Autre [cs.OH]. Université Nice Sophia Antipolis, 2004. Français. ⟨NNT : ⟩. ⟨tel-00006314⟩