Set-Theoretic Types for Polymorphic Variants
| Autor: | PetruccianiTommaso, CastagnaGiuseppe, NguyễnKim |
|---|---|
| Přispěvatelé: | Centre National de la Recherche Scientifique (CNRS), Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Informatica, Bioingegneria, Robotica e Ingegneria dei Sistemi [Genova] (DIBRIS), Universita degli studi di Genova, Vérification d'Algorithmes, Langages et Systèmes (LRI) (VALS - LRI), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
FOS: Computer and information sciences
Current (mathematics) Theoretical computer science Relation (database) Unification Computer science ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.3: Language Constructs and Features 0102 computer and information sciences 02 engineering and technology 01 natural sciences Set (abstract data type) Type safety 0202 electrical engineering electronic engineering information engineering type constraints 0101 mathematics union types Functional programming Computer Science - Programming Languages [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Type reconstruction 010102 general mathematics Union type 020207 software engineering Computer Graphics and Computer-Aided Design Subtyping Feature (computer vision) 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Software Programming Languages (cs.PL) |
| Zdroj: | ICFP 16, 21st ACM SIGPLAN International Conference on Functional Programming ACM SIGPLAN International Conference on Functional Programming ACM SIGPLAN International Conference on Functional Programming, Sep 2016, Nara, Japan. ⟨10.1145/2951913.2951928⟩ |
| DOI: | 10.1145/2951913.2951928⟩ |
| Popis: | Polymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a type system whose behaviour is in some cases unintuitive and/or unduly restrictive. In this work, we present an alternative formalization of poly-morphic variants, based on set-theoretic types and subtyping, that yields a cleaner and more streamlined system. Our formalization is more expressive than the current one (it types more programs while preserving type safety), it can internalize some meta-theoretic properties, and it removes some pathological cases of the current implementation resulting in a more intuitive and, thus, predictable type system. More generally, this work shows how to add full-fledged union types to functional languages of the ML family that usually rely on the Hindley-Milner type system. As an aside, our system also improves the theory of semantic subtyping, notably by proving completeness for the type reconstruction algorithm. ACM SIGPLAN International Conference on Functional Programming, Sep 2016, Nara, Japan. ICFP 16, 21st ACM SIGPLAN International Conference on Functional Programming, 2016 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|