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