Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Wed 21 Sep 2016 11:50 - 12:15 at Noh Theater - Session 9 Chair(s): Sam Lindley

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 polymorphic
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.

Wed 21 Sep

icfp-2016-papers
10:35 - 12:15: Research Papers - Session 9 at Noh Theater
Chair(s): Sam LindleyUniversity of Edinburgh, UK
icfp-2016-papers10:35 - 11:00
Talk
Trevor L. McDonellIndiana University, USA, Timothy A. K. ZakianOxford University, UK, Matteo CiminiIndiana University, USA, Ryan R. NewtonIndiana University, USA
DOI
icfp-2016-papers11:00 - 11:25
Talk
David ThibodeauMcGill University, Canada, Andrew CaveMcGill University, Canada, Brigitte PientkaMcGill University, Canada
DOI
icfp-2016-papers11:25 - 11:50
Talk
Bruno C. d. S. OliveiraUniversity of Hong Kong, China, Zhiyuan ShiUniversity of Hong Kong, China, João AlpuimUniversity of Hong Kong, China
DOI
icfp-2016-papers11:50 - 12:15
Talk
Giuseppe CastagnaParis Diderot University & CNRS, Tommaso PetruccianiUniversity of Genoa, France, Kim NguyễnUniversity of Paris-Sud, France
DOI