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
Times are displayed in time zone: Osaka, Sapporo, Tokyo change

10:35 - 12:15: Session 9Research Papers at Noh Theater
Chair(s): Sam LindleyUniversity of Edinburgh, UK
10:35 - 11:00
Ghostbuster: A Tool for Simplifying and Converting GADTs
Research Papers
Trevor L. McDonellIndiana University, USA, Timothy A. K. ZakianOxford University, UK, Matteo CiminiIndiana University, USA, Ryan R. NewtonIndiana University, USA
11:00 - 11:25
Indexed Codata Types
Research Papers
David ThibodeauMcGill University, Canada, Andrew CaveMcGill University, Canada, Brigitte PientkaMcGill University, Canada
11:25 - 11:50
Disjoint Intersection Types
Research Papers
Bruno C. d. S. OliveiraUniversity of Hong Kong, China, Zhiyuan ShiUniversity of Hong Kong, China, João AlpuimUniversity of Hong Kong, China
11:50 - 12:15
Set-Theoretic Types for Polymorphic Variants
Research Papers
Giuseppe CastagnaParis Diderot University & CNRS, Tommaso PetruccianiUniversity of Genoa, France, Kim NguyễnUniversity of Paris-Sud, France