Making a Faster Curry with Extensional Types
Paul Downen
Zachary Sullivan
Zena M. Ariola

Simon Peyton Jones
Microsoft Research
Cambridge, UK
simonpj@microsoft.com

University of Oregon
Eugene, Oregon, USA
pdownen@cs.uoregon.edu
zsulliva@cs.uoregon.edu
ariola@cs.uoregon.edu

Abstract1Curried functions apparently take one argument at a time,
which is slow. So optimizing compilers for higher-order languages invariably have some mechanism for working aroundcurrying by passing several arguments at once, as many as
the function can handle, which is known as its arity. But
such mechanisms are often ad-hoc, and do not work at allin higher-order functions. We show how extensional, callby-name functions have the correct behavior for directly
expressing the arity of curried functions. And these extensional functions can stand side-by-side with functions native
to practical programming languages, which do not use callby-name evaluation. Integrating call-by-name with otherevaluation strategies in the same intermediate language expresses the arity of a function in its type and gives a principled and compositional account of multi-argument curried
functions. An unexpected, but significant, bonus is that ourapproach is equally suitable for a call-by-value language anda call-by-need language, and it can be readily integrated into
an existing compilation framework.

Consider these two function definitions:CCS Concepts • Software and its engineering → Semantics; Compilers.
Keywords arity, extensionality, type systems
ACM Reference Format:
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton
Jones. 2019. Making a Faster Curry with Extensional Types. In Proceedings of the 12th ACM SIGPLAN International Haskell Symposium(Haskell ’19), August 22–23, 2019, Berlin, Germany. ACM, New York,NY, USA, 13 pages. https://doi.org/10.1145/3331545.3342594
Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies
are not made or distributed for profit or commercial advantage and that
copies bear this notice and the full citation on the first page. Copyrights
for components of this work owned by others than the author(s) must
be honored. Abstracting with credit is permitted. To copy otherwise, or
republish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee. Request permissions from permissions@acm.org.
Haskell ’19, August 22–23, 2019, Berlin, Germany© 2019 Copyright held by the owner/author(s). Publication rights licensed
to ACM.
ACM ISBN 978-1-4503-6813-1/19/08. . . $15.00
https://doi.org/10.1145/3331545.3342594

Introduction

f 1 = λx . let z = h x x in λy.e y z
f 2 = λx .λy. let z = h x x in e y z
It is highly desirable for an optimizing compiler to η expand f 1 into f 2 . The function f 1 takes only a single argument before returning a heap-allocated function closure;then that closure must subsequently be called by passing thesecond argument. In contrast, f 2 can take both arguments
at once, without constructing an intermediate closure, andthis can make a huge difference to run-time performance inpractice [Marlow and Peyton Jones 2004]. But this η expansion could be bad if (h x x) was expensive, because in a calllike (map (f 2 3) xs), the expensive computation of (h 3 3)
would be performed once for each element of xs, whereas in(map (f 1 3) xs) the value of (h 3 3) would be computed only
once. An optimizing compiler should not cause an asymptotic slow-down!
So the question becomes “does (h x x) do serious work?”
We should transform f 1 into f 2 only if it does not. But what
exactly do we mean by “serious work?” For example, suppose
we knew that h was defined as h = λp.λr .λq.blah; that is, hcannot begin to do any work until it is given three arguments.
In this case, it is almost certainly a good idea to η expand f 1
and replace it with f 2 . For this reason GHC—an optimizing
compiler for Haskell—keeps track of the arity of every inscope variable, such as h, and uses that information to guidesuch transformations. This notion of arity is not uniqueto Haskell or GHC: the same impact of η expanding f 1 to
f 2 , with its potential performance improvement and risk ofdisastrous slow-down, is just as applicable in eager functional
languages like OCaml [Dargaye and Leroy 2009]. In fact, therisks are even more dire in OCaml, where inappropriate η
expansion can change the result of a program due to side
effects like exceptions and mutable state. So arity informationis crucial for correctly applying useful optimizations.
The problem is that the very notion of “arity” is a squishy,
informal one, rooted in operational intuitions rather thansolid invariants or principled theory. In this paper we resolveHaskell ’19, August 22–23, 2019, Berlin, Germany

Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones

that problem by characterizing arity formally in a type system. However, the way we do so differs from previous work
[Bolingbroke and Peyton Jones 2009] in integrating types
with calling conventions (by which they mean arity) thatwould require quite a large change for GHC to move froma lazy-by-default to strict-by-default intermediate language.
Instead, our idea is to leverage multiple calling conventions(by which we mean, e.g., call-by-name versus call-by-value)
to solve the issues surrounding arity and η laws with types.
The advantage of this approach is that it is less monolithic,
and can be added to a variety of existing systems without
disrupting orthogonal parts of their semantics or implementation, making it easier to incorporate into a serious compiler
like GHC. Supporting this idea, we make these contributions:2• (Section 3) We describe our approach by starting witha standard call-by-value polymorphic λ-calculus, Fv ,and extending it with a new function type that can
express higher arities. We call the extended languageeFv , and give a self-contained meaning of arity in termsof the type system and equational theory of eFv .
• (Section 4) To demonstrate the minimal impact onan existing implementation, we show the addition toa standard call-by-value abstract machine which isneeded to support fast higher-arity function calls, butotherwise keeping the same semantics as Fv .
• (Section 5) Since we intend to preserve the original
semantics of the above machine, we need to compilee
Fv programs in a way that makes their evaluation strategy explicit to a stock call-by-value implementation.
We show how to execute our extended intermediate
Fv tolanguage by performing a simple translation from ee
Fv based on η expansion, which is shown to be correct.
• (Section 6) This approach does not just apply to call-byvalue languages. We explain how the same extension
can be made to a call-by-need λ-calculus by likewiseformalizing the notion of arity in Haskell programs.
We believe our approach could be integrated well with levity
polymorphism [Eisenberg and Peyton Jones 2017] (discussed
in Section 7) by extending their solution for polymorphismof non-uniform representations to polymorphism of nonuniform arities. Unlike previous work on optimizing curried
functions (which we discuss in Section 8) our approach grows
directly from deep roots in type theory; in particular callby-push-value [Levy 2001] and polarity [Danos et al. 1997;
Munch-Maccagnoni 2013; Zeilberger 2009], which tell us the
optimal evaluation strategy for a type based on its logicalstructure. Polarity brings two optimizations for compilinglazy functional languages—arity and call-by-value data representations [Peyton Jones and Launchbury 1991]—under
the same umbrella.

The Key Idea

Informally, we say the arity of a function is the number ofarguments it must receive before “doing serious work.” So
if f has arity 3, then f, (f 3), and (f 3 9) are all partial
applications of f; the only time f will compute anything iswhen it is given three arguments. We begin by explaining
why arity is important, before intuitively introducing our
new approach.
2.1

Motivation

There are several reasons why an optimizing compiler mightcare about the arity of a function:• A function of arity n can be compiled into machinecode that takes n arguments simultaneously passed
in machine registers. This is much, much faster thantaking arguments one at a time, and returning an intermediate function closure after each application.
• In Haskell, the expression (seq e1 e2) evaluates e1
to weak head-normal form, and then returns e2. Now
suppose we define
loop1, loop2 :: Int -> Int
loop1 = \x -> loop1 x
loop2 = loop2(seq loop1 True) evaluates loop1 to a function closure, and returns True. In contrast, (seq loop2 True)
simply diverges because loop2 diverges. So Haskell
terms do not always enjoy η equivalence; in general,
λx .ex , e. But η equivalence does hold if e has arity
greater than 0—in other words, if e is sure to evaluate
to a closure—so knowing the arity of an expression can
unlock optimizations such as discarding unnecessary
calls. For example, (seq loop1 True) becomes True
since loop1 has arity 1. But this arity information is
not seen in the type: loop1 and loop2 have the same
type, but different arities (1 versus 0).
• The trouble with limiting η equivalence is not uniqueto seq in Haskell: the same issue arises in eager functional languages, too. For example, consider similar
definitions in OCaml:
let rec loop1 x = loop1 x;;
let rec loop2 x y = loop2 x y;;
As before, loop1 and loop2 appear to be η equivalent, but they are not the same function. For example, let f = loop1 5 in true diverges whereas
let f = loop2 5 in true returns true. This isbecause with eager evaluation, all closures are computed in advance when bound; loop2 5 evaluates to a
closure but loop1 5 loops forever. So both eager andlazy functional languages can have the same essential problem with restricted η equivalence, which canblock optimizations.

Making a Faster Curry with Extensional Types

Haskell ’19, August 22–23, 2019, Berlin, Germany• Values of type (σ { τ ), such as f 1 or f 2 , are still fully
first-class: they can be passed to a function, returned
as a result, or stored in a data structure.
• At run-time, if f : τ1 { . . . τn { ρ, where ρ is notof form ρ 1 { ρ 2 , then f is bound to a heap-allocatedfunction closure of arity exactly n. This differs froman ordinary function д : τ1 → . . . τn → ρ in a call-byvalue language because there is no guarantee that д isbound to a closure which takes n arguments before performing work. And it is even further different from an
ordinary function in a call-by-need language becauseд itself might be bound to an unevaluated thunk.
• But what if the result type ρ was a type variable a? Is
it possible that a could be instantiated by (ρ 1 { ρ 2 ),thereby changing f ’s arity and making nonsense of
our claim that types statically encode arity? No: in
our system you cannot instantiate a type variable withsuch a type, which corresponds to similar existing
restrictions in GHC. For example, GHC does not let
type variable be instantiated with an unboxed, or unlifted type [Eisenberg and Peyton Jones 2017]. This
restriction is enforced by our type system and our new
function arrow fits neatly into this framework.

• Fast calls for higher-order functions are a problem in
GHC and OCaml today. Consider this higher-orderfunction:
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]zipWith f (a:as) (b:bs) = f a b : zipWith f as bs
zipWith f __= []The call to f in the body of zipWith is an “unknown
call” [Marlow and Peyton Jones 2004] where the compiler knows nothing about the arity of f. It might
expect one argument, or two, or even three (so that
zipWith would return a list of functions). Such unknown calls impose runtime overhead, which is frustrating because the vastly-common case is that f is anarity-2 function.
2.2 The Key Idea: A New Function Arrow
Our key idea is to add a new function type (σ { τ ), introe .e, alongside the existing one (σ → τ ). With
duced with λx
this idea, we can express that zipWith’s first argument f
is a function that takes precisely two arguments with thefollowing type:f :: a { b { c

Now the call in zipWith’s body can be fast, passing two
arguments in registers with no runtime arity checks. Thisnew type can be added locally, when compiling zipWith,
without looking at its call sites (see Section 2.3).
The new type has the following intuitions:• Terms of type (σ { τ ) enjoy unconditional η equivae . e x) = e.
lence: if e : σ { τ then (λx• The type (σ { τ ) is unlifted; that is, it is not inhabitedby ⊥ (a divergent value). This is why η equivalenceholds unconditionally; it is nonsensical to have a program of type (σ { τ ).
• This η equivalence also preserves work equivalence;that is, η expansion does not change the number of reduction steps in a program run. For example, consider
these two programs
let f 1 : Int { Intf 1 = let x = ack 2 3
e +y
in λy.x

let f 2 : Int { Inte let x = ack 2 3
f 2 = λy.
in x + yin map f 1 [1..1000]

in map f 2 [1..1000]

With an ordinary λ, one would expect these two program to behave differently: in f 1 , the (expensive) function ack would be called once, with x’s value being
shared by the 1000 calls of f 1 . But in f 2 , ack would
be called once for each of the 1000 invocations of f 2 .
e however, the two are precisely
With our new lambda λ,equivalent, and in both cases ack is called 1000 times.
In effect, the binding for f 1 is not memoised as a thunk,but is intentionally treated in a call-by-name fashion, apoint we will return to.

2.3

Adding Higher-Arity Functions to an
Intermediate Language

One of the major advantages to our approach to function
arity is that it is non-disruptive to orthogonal concerns ofan intermediate language. Rather than a monolithic solution like [Bolingbroke and Peyton Jones 2009], requiring
significant investment by changing the entire language, weshow here how to seamlessly add extensional higher-arity
functions to a λ-based calculus. Worded more formally, oursolution to higher-arity functions is a conservative extensionof an existing base language, meaning that the semantics andimplementation of the original features in the base language
are unchanged. In practical terms, being a conservative extension is important in the context of a compiler because itmeans that its other orthogonal jobs, like translating the fullsource language into the smaller core intermediate representation, do not need to be changed. And optimizations thatwere performed on the base intermediate language—while
they may now make use of arity information provided bytypes if it is advantageous to do so—are still correct to apply
directly as-is in the extended calculus.
While we anticipate that expert programmers may want
to write code that uses ({) directly, our main focus is on
using it internally, in the intermediate language of a compiler.
How, then, do higher-arity functions fit into the compiler
pipeline? Since there is no need to modify the front-end of
the compiler (the translation from the source language tothe intermediate language), the program can be first translated without generating any ({) functions, pessimisticallyassuming arity 0. The arity analysis that is already being

Haskell ’19, August 22–23, 2019, Berlin, Germany

Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones

performed can then be formally captured in the types offunctions by replacing (→) with ({). But just arbitrarilychanging types is not sound! So how can the optimizer improve function arity when it is entwined with types?
The so-called worker/wrapper transform is the standard
way that GHC uses to move information from the definitionof a function to its call sites [Gill and Hutton 2009], and is
especially useful for type-changing transformations. The
general technique is amenable to several optimizations, mostnotably [Peyton Jones and Launchbury 1991]. Here, we use
worker/wrapper to improve the arity of types. For example,
we can split the standard Haskell zipWith function into ae .e)
worker and wrapper like so (where \x{e means λx

Typesr, s, t ∈ Kind ::= V|Ea, b, c ∈ TyVarτ , σ, ρ ∈ Type ::= a|σ →τ
| ∀a.τ
|σ {τ
|e
∀a.τ

The worker wzipWith is an arity 3 function, and its firstargument is an arity 2 function. That way, the call to f in
the body of wzipWith can be a fast binary call, even though
the definition of f is unknown. The purpose of the wrapper is to serve as an interface change, which can update
individual call sites by inlining. For example, we can makethe following simplifications in a call to zipWith, where theboolean function has also been split into the arity 0 wrapper (||) :: Bool -> Bool -> Bool and arity 2 worker|~| :: Bool { Bool { Bool:
zipWith (||)==> wzipWith (\a { \b { (||) a b)==> wzipWith (\a { \b { (|~|) a b)==> wzipWith (|~|){- inline -}{- inline -}{- eta -}It may not look as if much has happened, but the new code ismuch better: the higher-order call to (|~|) in the wzipWith
loop is now a fast call to a known-arity function.

3

Extending an Intermediate Language
With Higher-Arity Curried Functions

Since the choice of the beginning base calculus is rather arbitrary, we choose a modest starting point: the call-by-value
system F, referred to here as Fv . We make this choice only forillustrative purposes due to the fact that it is simple to state
formally, but still serves as a common core for strict functional languages which can speak about important issues
such as polymorphism. However, the exact same extension
can be applied to a lazy λ-calculus—serving as an intermediate representation for Haskell programs—as well, which we
discuss later in Section 6.
3.1

Syntax

We give the syntax of e
Fv —a simple language based on a conventional system Fv for expressing higher-arity functions—inFig. 1. Expressions in e
Fv include the usual λ-abstractions andapplications (of the forms λx:σ .e and e u) for functions ofType variable
CBV function
CBV polymorphism
CBN function
CBN polymorphism

Expressions
x, y, z ∈ Vare, u, v ∈ Expr

::= x
|eд
| λx.ee| λx.e| error τ

wzipWith :: (a { b { c) { [a] { [b] { [c]wzipWith f (a:as) (b:bs) = f a b : wzipWith f as bs
wzipWith f __= []zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]zipWith f = wzipWith (\a { \b { f a b)

Source (CBV)Extensional (CBN)

Variable
Application
CBV abstraction
CBN abstraction
Erroneous resultд ∈ Arg::= u | σx, a ∈ BoundVar ::= x:τ|aTerm binding
Type binding

Shorthand
λr x.eλ x.e = λx.ee
λEx.e = λx.e
V

r

σ →τ

V
σ→
τ =σ →τE

σ →τ = σ { τ∀ra.τ
∀ a.τ = ∀a.τ∀Ea.τ = e∀a.τVFigure 1. Syntax of e
Fv : call-by-value system Fv extended
with call-by-name λ-abstractions.

some type σ → τ . Expressions also allow for polymorphismwith the analogous syntax of the form λa.e for abstracting
a type variable a in the polymorphic type ∀a.τ , and e σ for
specializing the polymorphic term e with the specific type σ .
We also include the expression error τ to allow for the possibility of run-time errors when a value of type τ is expected.
Note that this addition is not fundamental, it just shows therobustness of the approach.
Our extension with higher-arity functions is highlighted
in the figure, and consists of one new form of expression andtwo new types. In types, we introduce a new form of function,σ { τ . The purpose of this new function type is that (unlike→ arrows) multiple { arrows chain together into a single,
higher-arity abstraction. Intuitively, this chaining could beviewed in terms of multiple-argument functions (similar to[Bolingbroke and Peyton Jones 2009]) like so
τ { σ { ρ ≈ (τ , σ ) { ρhowever we do not require that all the arguments of a function be grouped together, allowing for the usual currying
and partial application even for higher-arity functions in e
Fv .

Making a Faster Curry with Extensional Types

We also introduce a new form of polymorphism, e∀a.τ thatsimilarly chains together along with {. Incrementally chaining polymorphism with function arguments is another advantage of our approach over [Bolingbroke and Peyton Jones2009]. In order to view them both as a polymorphic multiargument function, we would have to combine polymorphic
abstraction and functions into a single monolithic type likee∀a.τ { σ ≈ (a, τ ) { σwith the understanding that in (a, τ ) { σ , the type variablea introduced on the left-hand side of the arrow is in scopefor both τ and σ . Such monolithic types immediately be∀s and {s could be nested
come more complex because ein any way, requiring a notion of telescoping in the input of a function that reaches into its output. For example,e∀a.τ { e∀b.σ { ρ chains together as the multi-argument
function (a, τ , b, σ ) { ρ, where a is in scope for τ , σ , andρ, but b is only in scope for σ and ρ. Our approach keeps
higher-arity functions and polymorphism separate from one
another, completely avoiding the need for telescoping.
To go along with the two new forms of types, we also havee .e for introducing a function
a new form of abstraction: λx:σeof type σ { τ and λa.e for introducing polymorphism oftype e∀a.τ (where e is of type τ ). The two new types sharethe same syntax for application as in the base system Fv . The
primary reason to distinguish λ from λe is for the purposeof determining the types of annotated terms: without thedistinction, we don’t know whether λx:a.x should be of typea → a or a { a absent additional context.
Distinguishing the base language features from the extension is an essential ingredient in our approach: it allows us
to preserve the semantics for the original V-subset of the language, which remains untouched while we add the semantics
for new E-features. And it is important to know which of thetwo we are dealing with (the original base language or theextension) because the two semantics need not (and in thiscase will not) be the same. Having the distinction lets us add
an entirely new evaluation strategy as a conservative extension to a seemingly incompatible base calculus. To achieve
this goal, we just need to distinguish between the new types
introduced by the extension and the original types of Fv . Thisis done by classifying types as either V (for the base Fv types)
or E (for the extensional types being added on top), which
are two different basic kinds of types. In ordinary system Fv ,kinds are not necessary, since every type has the same kind(sometimes written ⋆). Classifying types as just V or E canbe seen as a rather rudimentary kind system. But this styleof classification makes it possible to extend the kind systemwith more advanced features in a more full-fledged system.
3.2

Type System

We present the type system for e
Fv in Fig. 2. Again, the extension to the base language is highlighted in the figure. In

Haskell ’19, August 22–23, 2019, Berlin, Germany

Typing environmentsΓ ::= x 1 : τ1 . . . x n : τnClassifying types τ : r
a:Vσ →τ :V∀a.τ : Vσ {τ :Ee∀a.τ : E

Checking types Γ ⊢ e : τVarΓ, x : τ ⊢ x : τΓ, x : σ ⊢ e : τ→IΓ ⊢ λx:σ .e : σ → τΓ ⊢ e : τ a < FV (Γ)∀IΓ ⊢ λa.e : ∀a.τΓ, x : σ ⊢ e : τ{Ie .e : σ { τΓ ⊢ λx:σΓ ⊢ e : τ a < FV (Γ)
e
∀I
e :e
Γ ⊢ λa.e∀a.τΓ ⊢ error τ : τErrorΓ ⊢e :σ →τ Γ ⊢u :σ→EΓ ⊢eu :τΓ ⊢ e : ∀a.τ σ : V∀EΓ ⊢ e σ : τ [σ /a]Γ ⊢e :σ {τ Γ ⊢u :σ{EΓ ⊢eu :τΓ ⊢e :e∀a.τ σ : V eΓ ⊢ e σ : τ [σ /a] ∀E

Figure 2. Type system of eFv .
the base system Fv language, there is only one kind of type(denoted here by V). However, since our extension has added
a new kind of types (denoted by E), checking whether τ : rholds points out the dichotomy between the two. And this
distinction can be done by just reading the head connectiveof the type. As such, the base language features (type variables a, arrows →, and quantifiers ∀) are all assigned thekind V. In contrast, the extension (arrows { and quantifierse∀) are assigned the kind E.
Also note that, for now, we choose not to add E type variables in addition to the existing V ones inherited from thebase system F, since this extension is not necessary for capturing arity in types. We will further discuss the ramificationsof this choice later in Section 7.
Next, Fig. 2 shows the typing rules. The rules for the baselanguage are conventional for system Fv , showing how totype check variables as well as abstractions and applications
for both functions and polymorphism. The highlighted typing rules are essentially the same as the ones for system
Fv , except that they refer to the new forms of arrow andquantifier.
3.3

Equational Theory

In order to reason about programs in terms of high-level
syntactic rewriting, we give an equational theory for e
Fv withthe axioms presented in Fig. 3. Notice that the first two
axioms, β V and ∀ are the usual rules for resolving applicationsof function and type abstraction in the call-by-value system
Fv . In particular, the β V rule is limited to substituting only
arguments which are values (syntactically, a variable or a
λ-abstraction). That’s because in call-by-value, arguments

Haskell ’19, August 22–23, 2019, Berlin, Germany

Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones

V ∈ Value ::= x | λx.e

thereby avoiding the above counter example. However, evenadmitting this restricted η axiom does not solve the problem
of explicating arity by expanding out every λ allowed bya type. For example, if we have some unknown functionz : a → a → a, then the above η → axiom gets stuck after
the first expansion:(β V )(λr x:σ .e) V = e[V /x](∀)(λra.e) σ = e[σ /a](β E )(λr x:σ .e) u = e[u/x](σ : E)(η { )e .(e x) = e : σ { τλx:σ(x < FV (e))(ηe∀ )eλa.(ea) = e : e∀a.τ

(a < FV (e))

Figure 3. Equational theory of e
Fv .
are evaluated first before the call is resolved, so that only
values may be passed to the function. For example,(λz:a.λx:a.x) (error a) , λx:a.x
is not a valid equation because the two sides give vastly different results: evaluating the left-hand side causes an error at
run-time when the argument error a is encountered, whereas
the right-hand side is already a value.
Besides the usual call-by-value system Fv axioms, we haveadditional axioms to handle higher-arity functions in e
Fv . Firstof all, we have the full version of the β axiom, denoted hereby β E , which can substitute expressions which are not values.
However, just allowing such a rule to apply whenever would
be dangerous—as illustrated by the inequality above. How
can we reconcile the difference between call-by-name andcall-by-value functions coexisting in the same language? We
can use the type of the argument to determine when the fullcall-by-name β axiom is safe. If the parameter of a function
has type σ : E, then any expression may be substituted
since the argument should be handled in a call-by-name way.
Otherwise, if the function’s parameter has type σ : V, thenthis is a call-by-value application, and only values may besubstituted. This side condition allows us to safely mix both
β axioms in the same language.
The primary motivation, though, is the addition of the fullη axioms η { and ηe∀ in Fig. 3. These are the equations thatallow us to use types to statically expand any expression
e to match its arity. As
with the appropriate number of λs
usual, the η axioms only apply to expressions of the correct
type (for example, expanding 5 to λx .(5 x) is nonsensical).
We really do need to use a call-by-name understandingfor expressions of type σ { τ and e∀a.τ in order to support
these η axioms. For example, applying the analogous η axiom
to an erroneous expression of type a → b is not an equality
error (a → b) , λx:a.(error (a → b) x)
because the left-hand side evaluates to an error while theright-hand side is a value. The safe version of the η axiom inthe call-by-value λ-calculus must be restricted like so(η → )

λx:σ .(V x) = V : σ → τ(x < FV (V ))z =η→ λx:a.(z x) ,η→ λx:a.λy:a.(z x y)This is because the partial application z x might alreadyresult in an error, so η → no longer applies.
In order to fully η-expand a function of any higher arity,
we must ensure that even erroneous expressions of typeσ { τ can be safely η-expanded without changing the resultof a program. The consequence of this constraint is that the
only context in which we are ever allowed to evaluate an
expression of type σ { τ is a calling context that already has
an argument ready. This restriction on evaluation follows
the call-by-name strategy, making it safe to η-expand any
e like for the expression e : enumber of λs∀a.a { a { aee =ηe∀ λa.(ea)
e λx:a.(ee=η { λa.
a x)
e λx:a.
e λy:a.(ee=η { λa.
a x y)
Note that as a side constraint necessary for satisfying the fullη axiom: expressions of type τ : E are not programs and cannot be evaluated. Allowing such expressions to be programs
would let us observe the difference between error (a { b)eand λx:a.(error(a { b) x) which, again, must be equivalent.

4

Adding Higher-Arity Calls to an Abstract
MachineNow, lets consider how to run programs, with the goal of
performing higher-arity function calls to a stock implementation [Peyton Jones 1992]. As is the running theme, we begin
with a standard call-by-value abstract machine for system Fv
and only add an extension to function applications and calls
which is capable of passing multiple parameters at once. The
machine in question is specified by the operational semantics in Fig. 4, and eagerly evaluates all function arguments ina right-to-left order. Evaluated function parameters can beeither types (for specializing polymorphism) or closures, andthe stack consists of a pending function waiting for its argument (eB ◦ S) or a chain of parameters which are annotatedwith the calling convention of their function (P r P ′ s P ′′ t S).
The purpose of keeping track of the calling convention offunction arguments is to remember the difference from thebase system Fv (for which r will always be V) and the newform of extensional functions during β-reduction. Our only
significant extension to this base semantics is found in the β ∗rule. When limited to just expressions from the base call-byvalue system Fv , the β ∗ performs the usual single-argument

Making a Faster Curry with Extensional Types

Haskell ’19, August 22–23, 2019, Berlin, Germany

Runtime state

4.1

W ∈ WHNF ::= λr x.e
P ∈ Param ::= W B|σS ∈ Stack ::= ε| eB ◦ S|PrS
B ∈ Env::= ε| [W B/x]B| [σ /a]B

Abstraction value
Closure parameter
Type parameter
Empty stack
Function application
Application chain
Empty environment
Closure binding
Type binding

Differences in Evaluation OrderIf we just run an arbitrary e
Fv expression, then the result
might be wrong! That’s because the machine in Fig. 4 uses
just a call-by-value evaluation order, and has no idea thatsome expressions should be treated in a call-by-name way
as specified by the axioms in Fig. 3. For example, we have
(λx:σ {τ .I ) (error σ {τ ) =βE Iewhere I = λa.λx:a.x
is the identity function, but instead at
run-time we get an error (i.e. a stuck state):

Machine steps ⟨e |B|S⟩ 7→ ⟨e ′ |B ′ |S ′⟩(β ∗ )′

r′⟨(λx:σ {τ .I ) (error σ {τ ) | ε | ε⟩7→ ⟨error σ {τ | ε | (λx:σ {τ .I )ε ◦ ε⟩′

⟨λ x.e | B | P r S⟩ 7→ ⟨e | B | S ⟩(app∗ (e, [P/x]B, S) = (e ′, B ′, S ′ ))(var)⟨x | B | S⟩ 7→ ⟨W | B ′ | S⟩(arg)⟨e u | B | S⟩ 7→ ⟨u | B | (eB) ◦ S⟩

(fun)

⟨W | B | (eB ′ ) ◦ S⟩ 7→ ⟨e | B ′ | (W B) t S⟩

(e : τ : t)

(spec)⟨e σ | B | S⟩ 7→ ⟨e | B | σ t S⟩

(e : τ : t)Multi-arity application([W B ′ /x] ∈ B)

app∗ (e, B, S) = (e ′, B ′, S ′ )e B, P E S) = app∗ (e, [P/x]B, S)
app∗ (λx.e,app∗ (e, B, S) = (e, B, S)e ′ and S , P E S ′ )(e , λx.e

Figure 4. Abstract machine for e
Fv-function application like so̸7→
In this case, the equational theory gives the intended result
and the machine is wrong. But we don’t want to modify theexisting machine, since it is already perfectly serviceable forthe base language.
Instead, we should elaborate the input programs themselves so that they give the correct result even on a purely
call-by-value machine. Thankfully we don’t need to do anything as drastic as continuation-passing style in order tomake the evaluation order explicit. Rather, η expansion comesin to solve the problem for us. As a pleasant side benefit, just
η-expanding the call-by-name expression to make the arity
explicit in the syntax also makes the evaluation order explicit! So there is no need to change the implementation of
the machine; strategically η expanding the program gives
the correct result as in:e .error σ {τ y) | ε | ε⟩⟨(λx:σ {τ .I ) (λy:σ⟨λx.e | B | P V S⟩ 7→ ⟨e | [P/x]B | S⟩
However, β ∗ is also capable of passing multiple arguments
at once during a single step, as defined by app∗ (e, B, S). The
idea is that, once the first argument is being passed to afunction closure (of any r ), then all the following arguments
for the next E-function calls are passed, too, at the sametime. For example, a ternary function call beginning with a
V closure and followed by two E calls is performed by thefollowing single β ∗ step:e .error σ {τ y | ε | (λx:σ {τ .I )ε ◦ ε⟩
7→ ⟨λy:σe .error σ {τ y)ε V ε⟩7→ ⟨λx:σ {τ .I | ε | (λy:σe .error σ {τ y)ε/x]ε | ε⟩7→ ⟨I | [(λy:σ4.2

Run-Time Arity Mismatche λz.(fe⟨λx.λy.
z y x) | B | P V P ′ E P ′′ E ε⟩

There is a new kind of error that might occur at run-time: it
may be the case that the machine gets stuck if the arity of afunction and the call stack do not match. For example, there
e like so
could be too many E-parameters and not enough λs

7→ ⟨f z y x | [P ′′/z][P ′/y][P/x]B | ε⟩e⟨λx:σ {τ .λy:ρ.x| B | P 1 V P2 E P3 E ε⟩ ̸7→

All three parameters are substituted in exactly one step. In
this sense, the semantics in Fig. 4 explicitly models how to
add higher-arity function calls to a standard abstract machine.
But if we want to run programs of e
Fv on this stock call-byvalue machine, we will need to compile e
Fv programs firstto implement the semantics of e
Fv that was given in Fig. 3.
In particular, in order to reflect e
Fv semantics with this stock
call-by-value machine, the compilation we describe next in
Section 5 will have to resolve the following two issues.

This is a stuck configuration because the multiple-argument
application operation is not defined in this case, since there
e to match the last E-parameter remaining
are not enough λs
on the stack:eapp∗ ((λy:ρ.x),[P1 /x]B, (P2 E P 3 E ε))= app∗ (x, [P2 /y][P1 /x]B, (P3 E ε))
In this case, too, applying the missing η-expansion to supe allowed by the type fixes the dynamic arity
ply all the λs

Haskell ’19, August 22–23, 2019, Berlin, Germany

Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones

Type-driven EJeKд : τ

Restricted η-long typing rules Γ ⊢η e : τ(invariant, e д : τ )

e
(λ)

e
e
EJλx.eKε: τ = λx.EJeKε:σ(η { )(ηe∀ )

ηVar(e : σ )Γ, x : τ ⊢η x : τ

e .EJeKд, x : τ
EJeKд : σ {τ = λx:σe .e ′)(e , λx:σΓ, x : σ ⊢ηE e : τeEJeKд : e∀a.τ = λa.EJeKд,
a :τ

e ′)
(e , λa.eΓ ⊢η λr x:σ .e : σ → τ

EJeKд : τ = CJeKд

(V)

(var)

CJxKд = x д(err)

CJerror τ Kд = error τ дrΓ ⊢η e : σ → τΓ ⊢ηE e : τ

a < FV (Γ)Γ ⊢η λra.e : ∀ra.τ

CJλr x.eKд = (λr x.EJeKε : τ ) д(e : τ )(app)

CJe uKд = CJeK(EJuKε : σ ), д(u : σ )(spec)CJe σ Kд = CJeKσ, д

(λ)

η→I

Γ, x : σ ⊢η e : σ → τ
η→E x
Γ, x : σ ⊢η e x : τΓ ⊢ηE u : σΓ ⊢η e u : τType-generic CJeKдηErrorrr(τ : V)Γ ⊢η error τ : τ

η→EΓ ⊢ e : ∀a.τ σ : V η∀EΓ ⊢ e σ : τ [σ /a]η∀I

Checking η-expansion Θ; Γ ⊢ηE e : τΓ, x : τ ⊢ηE e : σ
e .e : τ { σΓ ⊢ηE λx:τΓ ⊢ηE e : τ

η{I

τ :V

Γ ⊢η e : τEΓ ⊢η e : τ

Figure 5. Pre-processing transformation from e
Fv to eFv-

a < FV (Γ)

eΓ ⊢ηE λa:k.e:e∀a:k.τ

ηe∀V

Figure 6. Type system of eFv- .

mismatch problem:e λz:σe .(x z) | B | P1 V P2 E P 3 E ε⟩⟨λx:σ {τ .λy:ρ
7→ ⟨x z | [P 3 /z][P2 /y][P1 /x]B | ε⟩The opposite case is when there are too few E-parameters
e For example, we could haveon the stack to fill all of the λs.
e⟨(λx:a{a.λy:a.xy) Ia | ε | ε⟩e7→∗ ⟨λx:a{a.λy:a.x
y | ε | Ia ε V ε⟩̸7→ewhere Ia = λx:a.x: a { a. But notice that the type of the
input program was a { a, which is call-by-name (E), notcall-by-value (V)! As pointed out previously in the context ofthe equational theory, validating the η axioms requires us torestrict programs to expressions of V-types. This conditionealready rejects the term (λx:a{a.λy:a.xy) Ia as a valid input
program because it has the type a { a. As it turns out,
this same condition on the final type of result that welltyped programs are allowed to produce also eliminates thepossibility that there are not enough parameters on the stack
to complete a higher-arity function call.

5

Compiling Extensional Functions

We just saw some examples of how strategic η expansion
can let us run extensional, higher-arity functions on a stock
call-by-value machine. But is there a general procedure for
Fv expression? Here, we demonstrate a transcompiling any ee allowed by theformation for inserting all the missing λs
types of sub-expressions via η { and ηe∀ expansion, thereby
making the arity implied by types explicit in the syntax ofthe program. This transformation is given in Fig. 5 and consists of two parts. EJeKε : τ uses the type τ of e to insert any

λe missing from e (in the η { and η λe steps). CJeKε handles all
the other cases by descending down a chain of applications(in the app and spec steps). To do so, both transformations
are parameterized by a list, д, of the arguments surrounding the expression. So in their full generality, we have theη-expansion transformation EJeKд : τ (where e д : τ ) andthe helping CJeKд.
The purpose of this compilation process is to transforman e
Fv program into an equivalent one that gives the correct
answer. The first fact about the transformation is that it justelaborates the original expression by selectively applying η.
Proposition 1 (η Elaboration). For a typed e
Fv expression esuch that Γ ⊢ e : τ ,1. e =η { ηe∀ (EJeKε : τ ), and
2. e =η { ηe∀ (CJeKε).
The invariants created by the η-elaboration process canbe captured in the form of a type system, shown in Fig. 6.
This type system is a restriction of Fig. 2 by mandating ηexpansion in the arguments to function calls and underneathe We refer to the strict subset of eany λ (either λ or λ).
Fv expressions which are well-typed according to this restricted
system (i.e., expressions e such that Γ ⊢η e : τ ) as the executable sub-language eF- .
v

Proposition 2 (Compilation). For a typed e
Fv expression esuch that Γ ⊢ e : τ ,1. Γ ⊢E (EJeKε : τ ) : τ is a e
F- expression, andη

v

2. Γ ⊢η (CJeKε) : τ is a e
Fv- expression when τ : V.

Making a Faster Curry with Extensional Types

Haskell ’19, August 22–23, 2019, Berlin, Germany

Runtime StateW ∈ WHNF ::= λr x.e
P ∈ Param ::= x | σ
S ∈ Stack ::= ε|PrS| !x; SH ∈ Heap ::= ε| x := e; H

functions interact with sharing and memoization in a callby-need language like Haskell?”Empty stack
Application Chain
Thunk update
Empty heap
Thunk allocation

Machine steps ⟨e |H |S⟩ 7→ ⟨e ′ |H ′ |S ′⟩(β ∗ )⟨λr x.e | H | P r S⟩ 7→ ⟨e ′ | H | S ′ ⟩(app∗ (e[P/x], S) = (e ′, S ′ ))(push)⟨e P | H | S⟩ 7→ ⟨e | H | P t S⟩

(alloc)⟨let x = u in e | H | S⟩ 7→ ⟨e[y/x] | y := u; H | S⟩

(e : τ : t)(force)⟨x | x := e; H | S⟩ 7→ ⟨e | x := e; H | !x; S⟩(memo)⟨W | x := e; H | !x; S⟩ 7→ ⟨W | x := W ; H | S⟩

Multi-arity application app∗ (e, S) = (e ′, S ′ )e P E S) = app∗ (e[P/x], S)app∗ (λx.e,app∗ (e, S) = (e, S)

e ′ and S , P E S ′ )(e , λx.e

Figure 7. A lazy abstract machine extended with higherarity function calls
We are now equipped to properly run e
Fv expressions byefirst compiling to the sub-language F . Doing so lets us use

6.1

CJe xKP = CJeKx, Pv

the same implementation of the base call-by-value system
Fv (with support for faster multiple-argument function calls)
while still satisfying the mixed call-by-value and call-byname semantics of eFv .
Definition 1 (Programs). An expression e is an e
Fv- program
if ε ⊢η e : τ and τ : V.
Proposition 3 (Operational soundness). For any e
Fv- program e, if e = V (for some value V according to Fig. 3) then⟨e |ε |ε⟩ 7→∗ ⟨W |B|ε⟩ (for some W and B).

6

Sharing and Lazy Evaluation

So far, we showed how to extend an existing language withhigher-arity using extensional functions to get the eFv calculus. But the starting point—the call-by-value system Fv —was
not important; we needed to begin somewhere for the purpose of illustration. Because we formally distinguish thebase language (Fv ) in the extended calculus (eFv ) in orderto preserve two different semantics, we can choose a baselanguage with any evaluation strategy and apply the same extension. Of particular interest, we could have instead started
with an intermediate language that uses lazy evaluation, andachieve higher-arity functions using the same technique. The
question then becomes “how do higher-arity, extensional

A Higher-Arity Lazy Machine

To avoid repetition, we will only discuss the interesting differences that laziness poses when compared with Sections 3
to 5. In order to model laziness and sharing, we can use thestandard construct let x:τ = u in e which should be read as“first evaluate e and remember x = u; only evaluate u if x isneeded in e.” This understanding of let-bindings is formalized by the call-by-need abstract machine in Fig. 7. In thismachine, function parameters cannot be arbitrary expressions; they are pointers into the heap H which are allocatedby the alloc step. As such, they are only ever evaluated whenthe variable is referenced (by the force step) after which its
binding will be updated with its value (by the memo step).
Just like with the call-by-value machine of Section 4, thislazy machine requires some pre-processing step for elaborating the evaluation strategy of extensional functions. The elaboration for lazy evaluation is the same sort of η-expansion
as the one in Section 5, with a few minor differences. First,
since function parameters must be variables, we should takecare to name arguments with a let. Second, to compile a let,we should η-expand the bound expression, and push all thesurrounding arguments into its body. These additions are
expressed by the following new lines for the transformation(where we use a list of parameters P instead of arguments):

CJe uKP = CJlet x:τ = u in e xKP(x , u : τ )CJlet x:τ = u in eKP = let x:τ = EJuKε : τ in CJeKP
6.2

Forcing Thunks

Haskell-like languages have the capability of forcing thunks
even when their value is not yet needed using an operation
like seq to evaluate them to weak-head normal form. As
mentioned in Section 2, seq is precisely the operation that
invalidates η expansion for lazy function closures. This is
unacceptable for our approach, since we heavily rely on theη law to make the evaluation strategy explicit at run-time.
Thankfully, the same solution we used to differentiate
the evaluation strategy of the base language and the higherarity function space—that is, distinguishing the two types ofprograms—also solves the issue of inappropriate forcing due
to seq. In Section 3, there wasn’t even the possibility of a callby-name type variable, so the type of seq : ∀a.∀b.a → b →b prevents it from being applied to higher-arity functions,
thereby rescuing their η law. Even if we were to go to amore expressive system with arity polymorphism (discussed
next in Section 7), the type variables a and b only range
over lazy (call-by-need) types, which rules out extensional(call-by-name) ones. Note that if our lazy base calculus hasa polymorphic case expression of the form case e of x → uHaskell ’19, August 22–23, 2019, Berlin, Germany

Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones

which forces e, then it too needs to follow the interface ofseq described above; e cannot have a call-by-name type.

id) and binary function (like const) as follows:

6.3

Work Preservation

Even though both call-by-need and call-by-name are nonstrict evaluation strategies, they still have a crucial difference: call-by-need shares the work done to evaluate bindings,
whereas call-by-need repeats work every time the bindingis used. So we must take care that adding call-by-name toa call-by-need language does not accidentally cause work
duplication, as that could have a severe performance penalty.
With our methodology, work is preserved automaticallybecause we distinguish work-sharing bindings (call-by-need)from ones that are intended to be repeated (call-by-name).
If we bind a variable of a call-by-need type, then we intend
to share its work, so the η law does not apply in generalwhich prevents duplication. But if an expression e has acall-by-name type, then we do not plan to share its worke .(e x). This gives ananyway because it must be treated as λx
optimizer more freedom to η expand, which is somethingcall-by-need compilers are sensitive about doing because
it may duplicate work. Moreover, distinguishing the twokinds of function types allows us to simplify the runtime
representation of functions. Call-by-name functions can be adirect pointer to a closure instead of a pointer to a thunk likecall-by-need functions, which avoids the need to dynamicallycheck whether the closure has been evaluated yet.

7

Arity Polymorphism

In Section 3, we began with a calculus (system Fv ) that had
a notion of polymorphism, and added to it higher-arity curried functions. The base language and the extension weredistinguished by different kinds of types (written V versus
E, respectively). A consequence of this decision meant that
there was only polymorphism over the original V types, but
not over the new E types. For example, if we just added a pairing constructor Pair : ∀a.∀b.a → b → (a, b), then we could
only instantiate Pair with call-by-value (V) types, but notextensional types (E). On the surface, putting higher-arity
functions inside a pair seems reasonable. But to quantify overhigher-arity types, there are some serious issues surrounding
arity polymorphism to consider.
Notice that the polymorphism already available in e
Fv does
allow for polymorphism over functions that might have different arity. For example, consider the identity function
id : ∀a.a { aeid = λa.λx:a.x
Even though a is a V-type variable, it can still be instantiatedwith call-by-value function types that are called with multiple arguments. For example, id can be applied to unary (likeconst : ∀a.e∀b.a { b { ae λx:a.
e λy:b.xeconst = λa.λb.
id (∀a.a { a) id : (∀a.a { a)id (∀a.e∀b.a { b { a) const : ∀a.e∀b.a { b { aFv is analogous toIn this sense, the polymorphism allowed by e
[Bolingbroke and Peyton Jones 2009]. But e
Fv is more expressive, because in addition to call-by-value function closures(which might have a higher arity by starting with ∀ or →and continuing with multiple e∀s or {s) it also allows for“naked” higher-arity functions of kind E.
Now suppose that we just added type variables of kind
E (we will distinguish the two kinds of type variables bya : V versus a : E at their binding site à la system Fω ). Whatgoes wrong? We could now write the following alternative
identity and constant functions over E types:
id E : e∀a:E.a { aconst E : e∀a:E.e∀b:E.a { b { ae λx:a.xe= λa:E.
e λb:E.
e λx:a.
e λy:b.xe= λa:E.

But remember, in order to be able to evaluate programswith a stock implementation, we need to be able to fully
η-expand them! This makes both the evaluation strategy andthe arity of each function call fully explicit in the syntaxof the program. But how much expansion is necessary? Inboth of the above cases, it depends on the instantiation ofa, which can include any number of additional { arrows
which must “fuse” with the preceding ones. For example, if
we specialize the a in id E to the type of the identity function,e and so that special case
we learn that we are missing one λ,should be expanded once, but if we specialize a to the typee like so:of the constant function, it is instead missing two λs,e ee
id E (e∀a:E.a{a) =η { λx:∀a:E.a{a.λy:a.x
yid E (e∀a:E.e∀a:E.a{b{a)e ee λz:b.xe=η { λx:∀a:E.e∀b:E.a{b{a.λy:a.
yz
In each case, depending on the type of the higher-orderparameter x, x will be called at a different arity, which is nolonger known at compile-time in the definition site of id E .
The problem with polymorphic types a of kind E is that
E types posses a form of non-uniformity: they may varyin their calling convention in terms of the number of arguments they expect. Unlike V types for which arity checking isdone dynamically at run-time (“unknown” functions in theparlance of [Marlow and Peyton Jones 2004]), the different
arity of E types is “known” at compile-time. This property isessential for fast code generation: the call site of an E function type will just assume a particular arity for passing somenumber of arguments at once and call that function without
consulting its meta-data. As such, the arity of E types must

Making a Faster Curry with Extensional Types

be statically predictable, which conflicts with generic typevariables a : E.
There is another, better-known, non-uniformity problem
with polymorphism: data representation. For example, consider the projection function: snd : (a, b) → b = λ(x, y).y.
When both a and b are unknown polymorphic types, how
can we generate code for extracting the second componentof the pair? This is quite a complicated question when thevalues of different types may be represented by different
sizes and layouts in memory. If the pair (x, y) is stored contiguously in memory, then the offset to the beginning of ydepends on the size of the value x: when x is a character it
may 8-bits, but when it is a double-precision floating point
number it takes up 64-bits. Likewise, we need to know thesize of y to know how many bytes to move. And the situation is further exacerbated when certain types of values, likefloating-points, require special code for parameter passing.
A common solution to these problems with polymorphism
is to enforce uniform representation: every type is constrained
to values represented by pointer-sized data. With this solution, all of the above problems vanish, but at the cost of
extra boxing: if a value cannot fit within the constraints of apointer-like shape, then there is an extra level of indirection
by replacing the value with a pointer to the value. The indirection of boxing is costly in practice, and so an optimizing
compiler should use unboxed values when possible, but thismay come at the cost of disabling polymorphism.
An interesting approach to reconciling unboxing withpolymorphism was introduced by [Eisenberg and Peyton
Jones 2017] called “levity polymorphism.” One can view levity polymorphism as a conservative extension of a conventional functional language relying on uniform representation
with the following novel features:
1. unboxed types (e.g., integer and floating-point numbers) with a variety of different representations,
2. polymorphism over types with a known (i.e., monomorphic) representation, and3. polymorphism over representations themselves.
The key idea to make levity polymorphism work is to enrich kinds to be informative enough to determine the representations of values, even when the specific type of thosevalues are yet unknown. Pleasantly, points 1 and 2 together
do not cause issue for compilability. Only point 3 could betrouble, which encapsulates all of the above issues we discussed about compiling non-uniform polymorphism. And
thankfully, [Eisenberg and Peyton Jones 2017] gives a simple,
fundamental, requirement to ensure compilability:
Never move or store a levity-polymorphic value.
We believe that the same basic idea can be applied toenhance the polymorphism over functions with non-uniform
arity. As future work, we would like to further enrich thelanguage of kinds to fill in arity information even when the

Haskell ’19, August 22–23, 2019, Berlin, Germany

specific type is unknown. This extension could give a richlanguage of kinds with the goal of statically tracking:1. the specific evaluation strategy of function arguments(e.g., call-by-value versus call-by-name) as in Section 3,
2. the number of arguments the function accepts before
doing serious work (the traditional notion of arity),
3. the representation of each argument (so that specificparameter-passing code is known at the call site), and4. the representation of its result (so that higher-arity
functions can be composed).
The purpose of such an extension would be to maintain
information about both representations and arity in a compositional way: arities and representations should still beinferred from kinds no matter how deeply nested functions
and data structures become.

8

Related Work

8.1

Uncurrying

The classic way to handle multi-argument function calls is
to uncurry the function [Bolingbroke and Peyton Jones 2009;
Dargaye and Leroy 2009; Hannan and Hicks 1998]. Similar
to the work here, they too focus on solving fast higher-arity
calls inside higher-order functions.
Like us, uncurrying techniques aim to encode arity intypes, resulting in the introduction of new function types.
Both [Dargaye and Leroy 2009] and [Bolingbroke and Peyton Jones 2009] use a compound, multiple-argument function
type (σ0, . . . , σn ) → τ for uncurrying. As discussed in Section 3, multi-argument functions requires special support
in the presence of polymorphism, which ends up entwining
the two different language features into one. This involves
a telescoped introduction of type variables in the (many)arguments of the function which remain in scope for the
return type. Our approach based on extensional functions
completely avoids this technical problem since the structureof our higher-arity types e∀a.τ and σ { τ are exactly thesame as the original curried definition of functions.
In an approach more similar to ours, [Hannan and Hicks
1998] introduce an intermediate representation for their uncurrying transformation that involves adding annotated function types. The function type σ →⇑ τ fuses with τ when it isalso a function, and (σ →ϵ τ ) is a standard curried function
type. Our (σ { τ ) functions also have a fusion property, but
we do not require the codomain τ be function. [Hannan andHicks 1998]’s work avoids the problem of polymorphismthat other uncurrying techniques have by sticking to theHindley-Milner type system, where quantifiers only appear
in type schemes, but this is significantly less expressive thanthe unrestricted quantifiers of system F [Girard et al. 1989].
Thus far, uncurrying-based arity presents a monolithic
approach which fuses several distinct language features andcan require switching to an entirely different evaluation strategy like [Bolingbroke and Peyton Jones 2009], which canHaskell ’19, August 22–23, 2019, Berlin, Germany

Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones

interfere with the rest of the compiler pipeline. As a general design goal, our technique aims to be as non-disruptive
as possible, maintaining the same overall structure of programs and types for both lazy and strict languages (avoiding
both explicit uncurrying and thunking), and only requiringthat types inform us of the evaluation strategy. Thus, ourtechnique is better suited for integrating into existing implementations because of its lower initial investment. As
a pleasant side benefit, our approach based on integrating
multiple evaluation strategies introduces opportunities for
optimizations unrelated to arity. For instance, in Haskell,a call to f :: Int -> Int must first perform a dynamic
check to determine if f needs to be evaluated. In contrast,
calling f :: Int { Int can just immediately call f withoutthat dynamic check, because it must be bound to a closure.
Just uncurrying a higher-arity function does not express thisdifference of evaluation strategy.

while optimizations freely manipulate the structure of terms.
To apply the standard worker/wrapper transformation, thetype is derived from counting λs and this is used to create
the worker and wrapper. The wrapper η expands higherorder functions to produce higher-arity ({) functions. These
functions must appear fully applied in the wrapper which
may require further η expansion. We exploit the fact thatcall-by-name functions can always appear fully applied dueto the η law in order to generate saturated applications.

8.2

Arity in Compilation

The importance of function arity became apparent in theonce-pervasive categorical abstract machine [Cousineau et al.
1985] wherein curried functions would allocate many intermediate closures. With the goal of fast multi-arity function
calls, the Krivine [Krivine 2007] and ZINC [Leroy 1990] abstract machines repeatedly push arguments onto the stack
and an n-ary function will consume all n arguments it needs.
Another approach to speeding up curried programs is presented by [Marlow and Peyton Jones 2004] which combines
both statically and dynamically known arity information to
make fast calls. Statically, the compiler knows that a function
declared with 2 manifest lambdas has the arity 2. If a functionof known arity is fully applied, then the compiler can generate code that fuses the applications. For the cases where thearity is unknown at compile time, e.g., inside higher-orderfunctions like zipWith, there is a dynamic check for whencalls can be fused. The crux of these approaches is that either
the compiler must propagate statically-known arity information to the call site at compile-time, or there must be a
dynamic check for arity information at run-time.
The usage of arity information has long been an issue
in compilers leading to the development of complex arity
analyzers [Breitner 2014; Xu and Peyton Jones 2005] which
use the information to η expand and to float λ-abstractions
into and out of contexts; all while being careful to not duplicate work. More recent work performs cardinality analysis(which checks the usage of expressions) to apply the sametransformations [Sergey et al. 2014] and also to generate nonupdateable thunks at run-time if they will only be evaluatedonce. Our goal is to improve the frequency of multi-arity
function calls, which is orthogonal to analysis. We can use either simple analysis like syntactically-visible λ-abstractions
and applications, or those more thorough methods.
We seek to secure arity information inside the types of ourintermediate language; a place where it will be preserved

8.3 Polarity
Our inspiration for the treatment of arity came from polarity
and call-by-push-value [Levy 2001; Munch-Maccagnoni 2013;
Zeilberger 2009], which study a type-based mixture of evaluation strategies in programming languages from the fields
of logic and type theory. These systems enjoy the strongest
possible extensionality laws (a.k.a. η axioms) for every type
[Munch-Maccagnoni 2009], even in the presence of recursion and computational effects. To this end, every type has
an “innate” evaluation strategy which allows for mixing ofcall-by-value constructs (like data types) with call-by-nameconstructs (like functions).
Polarity has been used in the past to address other issues relevant to intermediate languages and optimization,
like resolving the conflict between “strong sum” types andnon-termination [Munch-Maccagnoni and Scherer 2015]. Recently, they have been extended with call-by-need constructs[Downen and Ariola 2018; McDermott and Mycroft 2019]used to support Haskell-like languages. Investigating theconsequences of these polarized languages in a practicalsetting has lead us to find that the practical concerns of afunction’s arity and representation are actually semantic
properties of the function’s type.
Interestingly, types with an innate evaluation strategy
have arisen independently in practice. For example, consider
what happens if we have a type Int# for real, 64-bit machine integers suitable for storing directly in a register. In
an expression like f (g 1), where f and g both have type
Int# -> Int#, is (g 1) evaluated before or after f is called?
Since a value of type Int# is represented by a 64-bit machine
integer, there is no way to delay the call to g. Passing an
unboxed integer in a register means it is already a value,
so it must be evaluated ahead of time (call-by-value). This
insight lets GHC handle unboxed values [Peyton Jones andLaunchbury 1991].
There are different ways of formalizing polarity in a system, and the closest one to our approach here is [MunchMaccagnoni 2009; Munch-Maccagnoni and Scherer 2015],
wherein type constructors can be applied to any types. Other
systems [Levy 2001; Zeilberger 2008] impose stronger constraints on types. In the notation here, we could restrictσ { τ : E so that σ : V and τ : E. This style requires “polarity shifts:” conversions between V and E kinds of types. With
shifts, we could remove the original type σ → τ : V, but that

Making a Faster Curry with Extensional Types

would go against our desire for a conservative extension; it
fundamentally changes the semantics of the base language,changing the front-end translation into the intermediate language. However, this alternative could have its own merits.
For example, GHC already uses monomorphic versions ofthese shifts to represent the boxing and unboxing explicitly
in programs (e.g., the unboxed Int# type is primitive, and thelazy Int is derived from it). Further investigation is required
to evaluate the relative practical merits of these two styles.

9

Conclusion

This work follows the tradition of designing calculi thatfaithfully capture the practical issue of optimizing curried
function calls. On one hand, higher-order functions are very
important for expressiveness and currying can dramaticallyreduce code size [Arvind and Ekanadham 1988]. On the other,efficiency is also a concern; no one wants to be penalized forwriting elegant programs! Compiler writers have many techniques to solve these problems, and we think some of thesecan be put on solid ground with polarization and extensionality. Interestingly, the solutions for making fast calls acrosshigher-order functions and for unboxing tuples appear to bedual to one another. As a pleasant side effect, this approachis suitable for both strict and lazy functional languages. We
have implemented the ideas presented here as an extensionof GHC’s Core intermediate language as a proof of concept.(available at https://github.com/zachsully/ghc/tree/etaarity).

Acknowledgments
This material is based upon work supported by the National
Science Foundation under Grant No. CCF-1719158 and Grant
No. CCF-1423617. Any opinions, findings, and conclusions
or recommendations expressed in this material are those of
the author and do not necessarily reflect the views of the
National Science Foundation.

References
Arvind and Kattamuri Ekanadham. 1988. Future Scientific Programmingon Parallel Machines. J. Parallel Distrib. Comput. 5, 5 (1988), 460–493.
Maximilian C. Bolingbroke and Simon L. Peyton Jones. 2009. Types Are
Calling Conventions. In Proceedings of the 2Nd ACM SIGPLAN Symposium
on Haskell (Haskell ’09). 1–12.
Joachim Breitner. 2014. Call Arity. In Trends in Functional Programming- 15th International Symposium, TFP 2014, Soesterberg, The Netherlands,
May 26-28, 2014. Revised Selected Papers. 34–50.
Guy Cousineau, Pierre-Louis Curien, and Michel Mauny. 1985. The Categorical Abstract Machine. In Functional Programming Languages andComputer Architecture, FPCA 1985, Nancy, France, September 16-19, 1985,
Proceedings. 50–64.
Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. 1997. A New
Deconstructive Logic: Linear Logic. Journal of Symbolic Logic 62, 3 (1997),
755—-807.

Haskell ’19, August 22–23, 2019, Berlin, Germany
Zaynah Dargaye and Xavier Leroy. 2009. A verified framework for higherorder uncurrying optimizations. Higher-Order and Symbolic Computation
22, 3 (2009), 199–231.
Paul Downen and Zena M. Ariola. 2018. Beyond Polarity: Towards a MultiDiscipline Intermediate Language with Sharing. In 27th EACSL Annual
Conference on Computer Science Logic, CSL 2018, September 4-7, 2018,
Birmingham, UK. 21:1–21:23.
Richard A. Eisenberg and Simon Peyton Jones. 2017. Levity polymorphism.
In Proceedings of the 38th ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI 2017, Barcelona, Spain, June
18-23, 2017. 525–539.
Andy Gill and Graham Hutton. 2009. The Worker/Wrapper Transformation.
J. Funct. Program. 19, 2 (March 2009), 227–251.
Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and Types.
Cambridge University Press, New York, NY, USA.
John Hannan and Patrick Hicks. 1998. Higher-Order unCurrying. In POPL
’98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998.
1–11.
Jean-Louis Krivine. 2007. A Call-By-Name Lambda-Calculus Machine.
Higher-Order and Symbolic Computation 20, 3 (2007), 199–207.
Xavier Leroy. 1990. The ZINC experiment: an economical implementation of
the ML language. Technical report 117. INRIA.
Paul Blain Levy. 2001. Call-By-Push-Value. Ph.D. Dissertation. Queen Maryand Westfield College, University of London.
Simon Marlow and Simon L. Peyton Jones. 2004. Making a fast curry:
push/enter vs. eval/apply for higher-order languages. In Proceedings of
the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP 2004, Snow Bird, UT, USA, September 19-21, 2004. 4–15.
Dylan McDermott and Alan Mycroft. 2019. Extended Call-by-Push-Value:
Reasoning About Effectful Programs and Evaluation Order. In Programming Languages and Systems, Luís Caires (Ed.). Springer International
Publishing, Cham, 235–262.
Guillaume Munch-Maccagnoni. 2009. Focalisation and Classical Realisability. In Computer Science Logic: 23rd international Workshop, CSL 2009, 18th
Annual Conference of the EACSL (CSL 2009), Erich Grädel and Reinhard
Kahle (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 409–423.
Guillaume Munch-Maccagnoni. 2013. Syntax and Models of a non-Associative
Composition of Programs and Proofs. Ph.D. Dissertation. Université Paris
Diderot.
Guillaume Munch-Maccagnoni and Gabriel Scherer. 2015. Polarised Intermediate Representation of Lambda Calculus with Sums. In 2015 30th
Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015).
127–140.
Simon L. Peyton Jones. 1992. Implementing Lazy Functional Languages on
Stock Hardware: The Spineless Tagless G-machine. Journal of Functional
Programming 2, 2 (1992), 127—-202.
Simon L. Peyton Jones and John Launchbury. 1991. Unboxed Values As
First Class Citizens in a Non-Strict Functional Language. In Proceedingsof the 5th ACM Conference on Functional Programming Languages andComputer Architecture. Springer-Verlag, London, UK, UK, 636–666.
Ilya Sergey, Dimitrios Vytiniotis, and Simon Peyton Jones. 2014. Modular,
Higher-order Cardinality Analysis in Theory and Practice. In Proceedingsof the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). 335–347.
Dana N. Xu and Simon L. Peyton Jones. 2005. Arity Analysis. (2005). Working notes.
Noam Zeilberger. 2008. On the Unity of Duality. Annals of Pure and Applied
Logic 153, 1 (2008), 660–96.
Noam Zeilberger. 2009. The Logical Basis of Evaluation Order and PatternMatching. Ph.D. Dissertation. Carnegie Mellon University.