Lambda the Ultimate

1974 talk show style interview with the original developers of APL; complete with plaid jackets and a smoking host.

The Origins of APL Video

I've never used APL but I found the talk to be very interesting. They talk about how APL come about, its evolution and the character set. Worth watching.

The popular Glasgow Haskell Compiler extends the Haskell 98 type system with several powerful features, leading to an expressive language of type terms. In contrast, constraints over types have received much less attention, creating an imbalance in the expressivity of the type system.

In this paper, we rectify the imbalance, transferring familiar type-level constructs, synonyms and families, to the language of constraints, providing a symmetrical set of features at the type-level and constraint-level. We introduce constraint synonyms and constraint families, and illustrate their increased expressivity for improving the utility of polymorphic EDSLs in Haskell.

Atomic Install from Bracha's blog.

I'm happy to see people talking about this, mostly because it's a pet topic of mine. I think too much ink has been spilled trying to shoehorn "dynamic languages" (by which I mean the usual suspects: Smalltalk-esque, mostly, and Python, PHP, etc.) into the vocabulary and mindset of type theory. Meanwhile, the operational model of these languages is really fundamentally different, and they are mostly quite similar: the semantics defines some run-time data model for programs, and then the program updates that model, usually in a fairly straightforward procedural way. In this sense, most of these languages can really be viewed as data description languages in disguise. Ruby is a great example of this: all of it's OO constructs are best viewed as syntactic sugar (semantic sugar?) over a fairly simple set of hashtable updates.

(Of course, the runtime data model may be abstract, as in JIT compiled code, and the runtime may not need to actually build and maintain it in a naive way, but that's hidden from the programmer.)

Anyway, given the above, it has for a long time struck me that a better direction for providing safety and static checking in such languages may be to borrow techniques from transaction processing. One might define suitable notions of data consistency and then insist that at particular semantic checkpoints, those consistency properties are guaranteed to hold. Atomic install is exactly what one such a mechanism might look like.

Is there work in the PL literature on this topic?

I'm reading Bolingbroke and Peyton Jones' excellent paper Types Are Calling Conventions, and following along by building a quick-and-dirty interpreter for their proposed intermediate language.

There are a couple of options for how to structure the branching construct in such an intermediate language, and I'm curious if anyone has explored the advantages and disadvantages. Bolingbroke and Peyton Jones' have a case expression (branching on values only, since the whole language is in ANF and the idea is to make strictness/laziness explicit) and a very simple pattern language (a wildcard, literals, and unwrapping a single layer of data constructor binding it's arguments), along with an operational semantics that (if I'm reading it correctly) requires evaluating the list of alternatives in order.

Is this easier to work with than an if/then/else expression? Is it to be preferred simply because it doesn't require distinguishing a Boolean type in the intermediate language?

It's clearly equivalent and easy to understand either way, but I'm wondering if one or the other makes it easier to express common optimizations/transformations. Are there other sensible options besides these two?

William Cook gave an interesting speech at ECOOP 2009. When discussing his career path, he touches on PLT research,

One thing I learned is that programming languages is a very small research area. As a grad student I thought we were big, because everyone in knew did it. But I found out that we are small, smaller perhaps than database research. We are also very fragmented, into functional, OO, typed and untyped, etc. This tends to lead dilute our influence on the community, I think.

differences between academia and industry

Academia is like page-rank: your value is defined by what everybody else thinks of you. And what you think of everybody else contributes to (or subtracts from!) their net academic worth. It is a closed hermetic self-referential system. The commercial value system is obviously different: it's all about money. In a way this is similar to page-rank as well. The difference is that the money comes from outside the community, from customers.

and a few other PLT morsels that might interest LtUers.

William Cook was the prinicpal lead for creating AppleScript. His HOPL paper was discussed on LtU before but I can't currently find the reference.

LP has been mentioned a number of times on LtU but never featured as a topic of discussion in its own right. On the face of it, it seems like an eminently sensible way to program. Why hasn't it taken the whole world by storm? Knuth puts forward Jon Bentley's observation as one possible answer: "a small percentage of the world's population is good at programming, and a small percentage is good at writing; apparently [Knuth is] asking everybody to be in both subsets."

To discuss this and other theories on their merits, a quick refresher on the basics of LP is in order. As usual, the relevant Wikipedia article is informative but bland. As Knuth pointed out, original sources are often best. Here are two good ones:

1. Programming Pearls: Literate Programming by Jon Bentley and Don Knuth; CACM, Vol. 29, No. 5, May 1986. (A bootleg copy available here.)
2. Programming Pearls: a Literate Program, by Jon Bentley, Don Knuth, and Doug McIlroy; CACM, Vol. 29, No. 6, June 1986. (Bootleg copies available here and here.)

The second paper is the more interesting of the two. It contains a literate program by Knuth and a review of the same by McIlroy:

Knuth has shown us here how to program intelligibly, but not wisely. I buy the discipline. I do not buy the result. He has fashioned a sort of industrial-strength Fabergé egg -- intricate, wonderfully worked, refined beyond all ordinary desires, a museum piece from the start.

I, too, buy the discipline for programming in the small but can't really see how CWEB-like systems can be adapted to and adopted by multi-hacker teams working on very large code bases written in a mixture of different languages. Ramsey's Literate Programming on a Team Project enumerates some of the problems.

Can LP be used for anything other than small-to-medium programs written by a single person in a single language?

Suppose a small language with a few primitive types (number, boolean, string) and first-class procedures from and to these types with arbitrary but fixed arity, and the usual syntax (if, let, top-level definitions), but without type declarations. And suppose that the types of all primitive procedures (which are monomorphic) are given, and so is the type of the top-level procedure ("main", a procedure that is not invoked by any procedure, also monomorphic). The language is strict, if it matters.

What I'd like to have is an algorithm that can find the unique monomorphic type of all other procedures in a closed program, or prove that there is none. For example, in main = λ() f0; f = λ(x) gx; g = λ(x) fx, the procedures f and g have no unique monomorphic type, despite being Hindley-Milner typeable. So far I have figured out how to type a fair number of special cases, but I have no clue when to stop looking, or what to do when I run out of heuristics. It's definitely important that procedures can have procedure-valued arguments whose exact types (not merely the fact of being a procedure) must be reconstructed; without those, the problem is easily solved.

Can anyone help?

(Update: Actually, I'm wrong; that example is typeable. As I said, it's procedure-valued arguments that create problems.)

With its focus on sharing practical experiences, Code Generation 2010 is the ideal opportunity for software practitioners to understand how to benefit from emerging tools, technologies and approaches in the broad area of Model-Driven Software Development.

Accepted speakers have their conference fees waived.

For full details and instructions on how to submit a session please visit: http://www.codegeneration.net/cg2010/speak.php

Hear what participants thought about this year's conference in this short video clip:
http://www.youtube.com/watch?v=OsKQeuCCSvg

Call for Speakers:
Submission Deadline: Friday January 15th 2010

We are seeking high-quality session proposals covering topics in model-driven software development (including Domain-Specific Languages (DSLs), Model-Driven Architecture (MDA), Executable UML, Software Factories & Software Product Lines, Generative Programming and related areas). Sessions could cover topics such as:

- Tool and technology development and adoption
- Code Generation and Model Transformation tools and approaches
- Defining and implementing modelling languages
- Domain Analysis and Domain Engineering
- Language evolution and modularization
- Meta Modelling
- Runtime virtual machines versus direct code generation

Case studies and interactive sessions based on these and related approaches are particularly encouraged although more theoretical sessions are also welcome.

Take part in Code Generation 2010 and find out why it is Europe's leading event on Model-Driven Software Development.

What people said about our previous events:

"I've been working in domain-specific modelling for a dozen years … and in this time this has been the highest-quality conference on this topic that I've been to - and I've been to a few."

"The presentations were all top quality, making it often difficult to decide between the concurrently running sessions. The wealth of MDD knowledge present at the event was impressive, not only from the presenters, but from the other delegates as well."

Code Generation 2010 is organised by Software Acumen and supported by InfoQ.com, OMG, ACCU and SkillsMatter.

After going through both of the Types and Programming Languages books, I am starting to feel confident in my understanding of Type Systems in terms of how they would be implemented. However, I still feel uncomfortable with the theoretical foundations; even after going through the proofs it still seems like a lot of hand-waving when defining what is a type. So to try to find a good mental model of what a type is I thought I would ask LtU: what is a type?

The reason for my uneasiness probably stems from my background programming in both static and dynamic type systems. The static definition of types seems to tend more towards what can be proven at compile time. This definition seems to put more emphasis on creating type systems which are strongly normalizing. However, in dynamic type systems, types are often manipulated as terms. Trying to find a consistent mental model for these two usages of the term (especially after the introduction of subtyping) I am currently stuck with defining them as propositions which map terms to truth values. The intuition is that a type is a proposition, nothing more. I can't seem to find much theory for such a model and that prompted this post. Is this highly inconsistent with current theory?

More formally, what would your initial reaction be to a system where:

λt:T.x  →  λt. if T(t) then x else TypeError

I just came across this and thought it might be of interest to LtU readers:

http://openendedgroup.com/field

It's a hybrid textual and visual programming environment developed by the MIT Media Lab, with some pretty interesting ideas. For example: you can arrange blocks of code visually and scrub over them with an execution marker; you can embed bits of code which execute inside other applications; and it can show graphical representations of values.

Any thoughts?