Lambda the Ultimate

You might still apply for a grant, but time is short!

Only a tentative program is currently available, but I suppose the topics mentioned in it will remain in the final program, and many of them are interesting, and often discussed here on LtU.

Ωmega is a new programming language by Tim Sheard which is descended from Haskell and adds new facilities for defining static type constraints, such as allowing "users to write functions at the level of types, and then use those functions in the type of functions at value level". It also has "equality qualified types". See also Programming with Static Invariants in Omega and the manual for more information. Mentioned previously (in passing) on LtU.

What follows will be a very subjective and personal view, as much my own history and development in the field and how things looked through my eyes as about the development of the field itself.

This essay is a longer version of the introductory essay in (Partee 2004). The introductory essay was first written in this long form in February 2003, but had to be cut down to about half the size to fit in the book...

This essay is about natural language semantics, but you'll find old friends here: lambdas, bindings, types, quantifiers etc. If you are lazy, go directly to footnote 25...

No surprise, really, if you follow the links we give here from time to time about TLGs and such.

The Church Project investigates the foundations, design principles and implementation techniques of programming languages and related systems. The overall goal is the development of software technology that performs better and is more reliable. The project is named in honor of Alonzo Church, the inventor of the lambda calculus.

Four major research efforts (supported by various funding bodies including EC, EPSRC, and NSF) are presently undertaken by project participants:

• Compiling with Flow Types
• Compositional Analysis
• Programming with Dependent Types (DML) (Xanadu)
• Linear Naming and Computation

We previously linked to a document on this site, but not the site itself.

Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis. In this paper we prove that Amadio and Cardelli's type system with subtyping and recursive types accepts the same programs as a certain safety analysis. The proof involves mappings from types to flow information and back. As a result, we obtain an inference algorithm for the type system, thereby solving an open problem.

I believe it's instructive to see type systems in this light. Did we discuss something like this recently?

Poly* is a novel retargetable meta type system for various process and mobility calculi. Poly* is a direct descendant of PolyA, a type system for Mobile Ambients by Amtoft, Makholm, and Wells. Meta* is a generic process calculus that can be instantiated to specific process calculi like the Pi-calculus and Mobile Ambients by supplying reduction rules.

A web interface is available for experimentation after you can read the technical report and ESOP 2005 paper.

The list of common questions and answers about Poly* may be a good place to start if you are merely curious.

This PEP proposes an extension to "duck typing" called "monkey typing", that preserves most of the benefits of duck typing, while adding new features to enhance inter-library and inter-framework compatibility. The name comes from the saying, "Monkey see, monkey do", because monkey typing works by stating how one object type may mimic specific behaviors of another object type.

More here and here (from Guido).

Among the notions discussed: Interfaces and Design By Contract, Parameterized Types and Types vs. Classes.

Link: Guido van Rossum broaches the subject of type tagging for Python.

Optional static typing has long been requested as a Python feature. It's been studied in depth before (e.g. on the type-sig) but has proven too hard for even a PEP to appear. In this post I'm putting together my latest thoughts on some issues, without necessarily hoping to solve all problems.

Static vs. dynamic is a never-ending thread in most PL discussions these days. But designing a type system is a *hard* task, one which I'm not sure doesn't require from a ground on up approach. But it would be nice if you could choose to work your way into, though most of the Smalltalk crowd will inform us that Strongtalk never did quite catch on.


(accompanying discussion forum)

In an attempt to combine some of the benefits of lazy and eager evaluation, I have implemented a language with an evaluation strategy which is strict with respect to divergence, but performs lazy evaluation on certain intermediate subterms to allow a more expressive use of recursion.

Does anybody have any references to work on similar evaluation schemes?

Tim Sweeney started this interesting Types-list thread. A summary of the responses he receieved is here.