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

Dunfield showed that a simply typed core calculus with intersection
types and a merge operator is able to capture various programming
language features. While his calculus is type-safe, it is not
coherent: different derivations for the same expression can
elaborate to expressions that evaluate to different values.
The lack of coherence is an important
disadvantage for adoption of his core calculus in implementations of
programming languages, as the semantics of the programming language
becomes implementation-dependent.

This paper presents λi: a coherent and type-safe calculus with a
form of *intersection types and a merge operator.
Coherence is achieved by ensuring that intersection types
are disjoint and programs are sufficiently
annotated to avoid type ambiguity. We propose a definition of disjointness where two
types A and B are disjoint only if certain set of types are common
supertypes of A and B. We investigate three different variants of
λi, with three variants of disjointness. In the simplest
variant, which does not allow top types, two types are disjoint if
they do not share any common supertypes at all. The other two variants
introduce top types and refine the notion of disjointness to allow
two types to be disjoint when the only the set of common supertypes are
top-like. The difference between the two variants with top
types is on the definition of top-like types, which has an impact on
which types are allowed on intersections. We present a type system
that prevents intersection types that are not disjoint, as well as an
algorithmic specifications to determine whether two types are disjoint
for all three variants.

Wed 21 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

10:35 - 12:15
Session 9Research Papers at Noh Theater
Chair(s): Sam Lindley University of Edinburgh, UK
Ghostbuster: A Tool for Simplifying and Converting GADTs
Research Papers
Trevor L. McDonell Indiana University, USA, Timothy A. K. Zakian Oxford University, UK, Matteo Cimini Indiana University, USA, Ryan R. Newton Indiana University, USA
Indexed Codata Types
Research Papers
David Thibodeau McGill University, Canada, Andrew Cave McGill University, Canada, Brigitte Pientka McGill University, Canada
Disjoint Intersection Types
Research Papers
Bruno C. d. S. Oliveira University of Hong Kong, China, Zhiyuan Shi University of Hong Kong, China, João Alpuim University of Hong Kong, China
Set-Theoretic Types for Polymorphic Variants
Research Papers
Giuseppe Castagna Paris Diderot University & CNRS, Tommaso Petrucciani University of Genoa, France, Kim Nguyễn University of Paris-Sud, France