Join Newsletter

Types (are / want to be) Calling Conventions

YOW! Lambda Jam 2019

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.

Ben Lippmeier

Post-Functional Reprogrammer

Ghost Locomotion


I am a programming languages researcher and compiler engineer. Most of my work has been in the fields of type theory, stream fusion and parallel programming. Until recently I worked at Digital Asset in smart contract languages, and am an an adjunct at the University of New South Wales.