Types (are / want to be) Calling Conventions

schedule May 14th 10:30 - 11:00 AM place Red Room people 98 Interested

Functions in the lambda calculus rightly take single values as their arguments, and return single values as their results. Functions in machine code rightly take multiple values as their arguments (preferably in registers), and return multiple values (preferably in registers) as their results. For a compiler writer, dealing with this mismatch is a right headache. Arity information, which describes how many arguments each source level function "actually" takes wafts through ones codebase like an unpleasant odour, and after particular compiler stages subverts ones once loved source-level type signatures into unfortunate lies.

Salt is a new compiler intermediate language that embraces uncurriedness as a first class condition, and whose type signatures speak the truth about arity. Functions are functions still, but their types are honest about the fact that no one really evaluates lambda expressions using capture avoiding substitution. The GHC core language tried to tell a similar story using unboxed tuples, but it didn't quite work. The C language stayed out in the sun for too long wondering what a void returning lambda abstraction really returned, and when we all came back to find it, the only thing left was Salt.

 
 

Outline/Structure of the Talk

Lecture style talk. I'll introduce some examples and use them to explain ideas in compilers and type theory.

Learning Outcome

A better understanding of how type information can be used in compiler engineering. Exposure to alternate interpretations of common type notation such as the function constructor (->)

The ideas about expressing uncurriedness in type signatures were developed by Max Boilingbroke and Simon Peyton Jones for GHC, but never implemented. There was a paper about it in the Haskell Symposium 2009, and the implementation in Salt derives from that work. I'll also explain the history of this GHC work, and how it relates to the compilation of Haskell code.

Target Audience

People interested in type system design and applications in compiler engineering.

Prerequisites for Attendees

Basic experience with typed functional programming. Ability to read Haskell style type signatures.

schedule Submitted 8 months ago