Home

Types are Calling Conventions

If optimization and intermediate languages for lazy functional languages are your things, take a look at Types are Calling Conventions by Max Bolingbroke and Simon Peyton Jones.

It is common for compilers to derive the calling convention of a function from its type. Doing so is simple and modular but misses many optimisation opportunities, particularly in lazy, higher-order functional languages with extensive use of currying. We restore the lost opportunities by defining Strict Core, a new intermediate language whose type system makes the missing distinctions: laziness is explicit, and functions take multiple arguments and return multiple results.

By James Iry at 2009-05-16 23:29 | Functional | Implementation | other blogs | 26914 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

This is an exciting

This is an exciting direction! I've been thinking recently about guidance of how APIs should be used for optimal performance (esp. in bulk calls, which I'm finding to be a weakness for parallel systems), and have been on the fence over user directed, inferred, or perhaps a bit of both. I'll definitely be keeping an eye out for once they perform some sort of evaluation!

By lmeyerov at Sun, 2009-05-17 03:35 | login or register to post comments

Strict calculus better for lazy implementation

There's an interesting line in the conclusion:
""For a long time, a lazy language
was, to us at least, the obvious intermediate language for a
lazy source language such as Haskell – so it was rather surprising
to discover that an appropriately-chosen strict calculus seems to be
in many ways better suited to the task!""

By Marc Coram at Sun, 2009-05-17 06:09 | login or register to post comments

Well...

Urban Boquist did research on efficient compilation of lazy functional languages and devised GRIN, which is a strict, monadic, whole-program functional intermediate language. This language is the backend for the UHC, JHC and LHC haskell compilers.

I haven't read all of the paper by SPJ and Bolingbroke, but it's worth noting GRIN is untyped - JHC uses a variant of GRIN that has types, but we have reverted to using the simple language described by boquist in LHC.

By Austin Seipp at Sun, 2009-05-17 07:35 | login or register to post comments

Structure of Interaction

This also comes out very clearly when one translates sequential languages into interaction (games or process calculus).

By Martin Berger at Sun, 2009-05-17 09:38 | login or register to post comments

And "seq"

I also liked this short section:

4.4 The seq function

A nice feature of Strict CoreANF is that it is possible to give a
straightforward definition of the primitive seq function of Haskell:...
[ snip two line type and definition of "seq" ]

By ChrisKuklewicz at Mon, 2009-05-18 09:47 | login or register to post comments

strict types in the lazy source language

I've been waiting a good while for progress with coexistence of strictness and laziness, as referred to in the final paragraph.

We would like to expose the ability to use “strict” types to the compiler user, so Haskell programs can, for example, manipulate lists of strict integers ([!Int ]). Although it is easy to express such things in the Strict Core language, it is not obvious how to go about exposing this ability in the source language in a systematic way – work on this is ongoing.

In the earlier paper, Wearing the hair shirt, SPJ said

Still unclear exactly how to add laziness to a strict language. For example, do we want a type distinction between (say) a lazy Int and a strict Int?
I've got my own toy language which supports the distinction at its heart, and would like to try a real, useful language that does so. I doubt Haskell is the place for this, since laziness is so entrenched in the libraries.

Does anyone have a pointer to ongoing work?

By Scott Turner at Tue, 2009-05-19 02:25 | login or register to post comments

See Noam Zeilberger's PhD thesis...

On the Logical Basis of Evaluation Order and Pattern Matching

An old and celebrated analogy says that writing programs is like proving theorems. This analogy has been productive in both directions, but in particular has demonstrated remarkable utility in driving progress in programming languages, for example leading towards a better understanding of concepts such as abstract data types and polymorphism. One of the best known instances of the analogy actually rises to the level of an isomorphism: between Gentzen's natural deduction and Church's lambda calculus. However, as has been recognized for a while, lambda calculus fails to capture some of the important features of modern programming languages. Notably, it does not have an inherent notion of evaluation order, needed to make sense of programs with side effects. Instead, the historical descendents of lambda calculus (languages like Lisp, ML, Haskell, etc.) impose evaluation order in an ad hoc way.

This thesis aims to give a fresh take on the proofs-as-programs analogy---one which better accounts for features of modern programming languages---by starting from a different logical foundation. Inspired by Andreoli's focusing proofs for linear logic, we explain how to axiomatize certain canonical forms of logical reasoning through a notion of pattern. Propositions come with an intrinsic polarity, based on whether they are defined by patterns of proof, or by patterns of refutation. Applying the analogy, we then obtain a programming language with built-in support for pattern-matching, in which evaluation order is explicitly reflected at the level of types---and hence can be controlled locally, rather than being an ad hoc, global policy decision. As we show, different forms of continuation-passing style (one of the historical tools for analyzing evaluation order) can be described in terms of different polarizations. This language provides an elegant, uniform account of both untyped and intrinsically-typed computation (incorporating ideas from infinitary proof theory), and additionally, can be provided an extrinsic type system to express and statically enforce more refined properties of programs. We conclude by using this framework to explore the theory of typing and subtyping for intersection and union types in the presence of effects, giving a simplified explanation of some of the unusual artifacts of existing systems.

If you prefer denotational semantics to structural proof theory, Paul Levy's work on call-by-push-value is the place to look.

By neelk at Tue, 2009-05-19 14:09 | login or register to post comments

liking Zeilberger's approach

The thesis is rough going for me — wish I had time/youth to learn the background to this.

He says,

the answer to the question of eager vs. lazy evaluation is encoded in types, rather than being a global property of the language.
and from browsing the thesis it appears to me that his answer is successful.

The part of Paul Levy's work that I'm familiar with has a language that supports both call-by-value and call-by-name, but it does not express the duality that is so appealing, and which is present in Zeilberger's thesis.

In browsing the thesis I encountered his description of the primordial function space .

Because the primordial function space is fundamentally mixed polarity, to get the polarities to work out for call-by-value/call-by-name function spaces we have to insert shifts in different places.
This is something which I have wrestled with on my own. If we had a language in which functions were generally defined with types of the primordial mixed polarity, would they be useful in both call-by-value and call-by-name aspects? What kind of syntactic sugar would be needed? Maybe there's an answer in the thesis which further reading will provide.

By Scott Turner at Wed, 2009-05-20 01:01 | login or register to post comments