Functors are Type Refinement Systems

Abstract : The standard reading of type theory through the lens of category theory is based on the idea of viewing a type system as a category of well-typed terms. We propose a basic revision of this reading: rather than interpreting type systems as categories, we describe them as functors from a category of typing derivations to a category of underlying terms. Then, turning this around, we explain how in fact any functor gives rise to a generalized type system, with an abstract notion of typing judgment, typing derivations and typing rules. This leads to a purely categorical reformulation of various natural classes of type systems as natural classes of functors. The main purpose of this paper is to describe the general framework (which can also be seen as providing a categorical analysis of refinement types), and to present a few applications. As a larger case study, we revisit Reynolds' paper on "The Meaning of Types" (2000), showing how the paper's main results may be reconstructed along these lines.
Type de document :
Communication dans un congrès
42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015), Jan 2015, Mumbai, India. 〈10.1145/2676726.2676970〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01096910
Contributeur : Noam Zeilberger <>
Soumis le : jeudi 18 décembre 2014 - 14:32:12
Dernière modification le : jeudi 11 janvier 2018 - 06:17:49
Document(s) archivé(s) le : lundi 23 mars 2015 - 16:44:00

Fichier

funts.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Copyright (Tous droits réservés)

Identifiants

Collections

INRIA | PPS | USPC

Citation

Paul-André Melliès, Noam Zeilberger. Functors are Type Refinement Systems. 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015), Jan 2015, Mumbai, India. 〈10.1145/2676726.2676970〉. 〈hal-01096910〉

Partager

Métriques

Consultations de la notice

533

Téléchargements de fichiers

211