System F with Coercion Constraints

Résumé : Nous présentons un lambda-calcul de second ordre avec des contraintes de coercions qui généralisent une extension précédente du Système F avec des abstractions de coercions paramétriques en permettant des abstractions multiples mais simultanées sur les types et les coercions, ainsi que des coercions récursives et des types équi-récursifs. Cela permet de présenter de façon uniforme plusieurs fonctionnalités des systèmes de types auparavant tudiées séparément: le confinement de types, le polymorphisme bornée et bornée par instance, qui sont déjà codables avec l'abstraction de coercions paramétrique, et les contraintes de sous-typage à la ML. Notre cadre permet une séparation claire entre les constructions du langage avec et sans contenu calculatoire. Nous distinguons également les coercions cohérentes qui sont entièrement effaçables des coercions incohérentes qui suspendent l'évaluation, et permettent le codage des GADTs. Techniquement, les coercions de type, témoins d'une relation de sous-typage entre les types, sont remplacées par une notion plus expressive de coercions de typages, témoins d'une relation d'inclusion entre les typages, e.g. des paires composées d'un environnement de typage et d'un type. Le calcul est équipé d'une relation de réduction forte permettant la réduction sous les abstractions---mais nous introduisons également une forme de réduction faible car la réduction ne peut pas être poursuivie sous les abstractions de types incohérentes. La sûreté du typage est prouvée en adaptant une technique sémantique de types indexés aux stratégies de réduction forte, en plaçant les indices à l'intérieur des termes afin de contrôler les étapes de réduction de façon interne.
Type de document :
Rapport
[Research Report] RR-8456, INRIA. 2014, pp.36
Liste complète des métadonnées


https://hal.inria.fr/hal-00934408
Contributeur : Didier Rémy <>
Soumis le : mardi 21 janvier 2014 - 23:18:32
Dernière modification le : samedi 17 septembre 2016 - 01:37:28
Document(s) archivé(s) le : mardi 22 avril 2014 - 10:15:31

Fichier

RR-8456.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00934408, version 1

Collections

Citation

Julien Cretin, Didier Rémy. System F with Coercion Constraints. [Research Report] RR-8456, INRIA. 2014, pp.36. <hal-00934408>

Partager

Métriques

Consultations de
la notice

359

Téléchargements du document

289