Equality-BasedUniquenessTyping

Date: 2007-04-26

Time: 11:45

Room: BBL room 471

Speaker: Edsko de Vries (Trinity College Dublin, Compiler Design Research Group)

Title: Equality-Based Uniqueness Typing

• Slides: stc-uniqueness.pdf

Abstract

Side effects in functional languages, such as I/O, are often provided through monads. However, monads are an advanced concept that beginning functional programmers often find difficult to understand. An alternative approach is to allow for ordinary functions to have side effects, but restrict how they can be applied -- these restrictions are enforced by a uniqueness type system.

I will explain the basics of uniqueness typing, what it is useful for and what uniqueness types look like. I will then give an overview of my work on uniqueness typing [IFL2006, TFP2007]; in particular, I'll show how to remove subtyping and uniqueness inequalities (constraints) from Clean's uniqueness type system, to get a uniqueness type system which is very similar to an ordinary Hindley/Milner (Haskell-like) type system. Finally, I will suggest some ways in which we can make uniqueness typing "translucent", so that it is visible only when relevant. In fact, using a few simple syntactic conventions, we can reinterpret Haskell programs under a uniqueness type system without anyone noticing.