Lambda the Ultimate

The Python Paradox

I mostly agree with the thrust of this piece, I think, but here's the most interesting bit (to me, at least):

Both languages [Python and perl] are of course moving targets. But they share, along with Ruby (and Icon, and Joy, and J, and Lisp, and Smalltalk) the fact that they're created by, and used by, people who really care about programming. And those tend to be the ones who do it well.

It's interesting that all of those languages are dynamic and thus favored by Paul Graham. Does he really think that, e.g., Haskell and Ocaml are being created by people who don't "really care about programming." Or is this just a cheap shot? Or are those languages really just completely off his radar?

Sometimes you just stumble across a project that you had in the back of your mind for a while: an XML standard for representing linear programming problem and solution instances

now I just have to find the time to write a solver.

I know that this was discussed on LtU already, but as "Why Types" discussion demonstrated, people can always come with new ideas on old topics.

From theoretical point of view, call-by-value and call-by-name are dual.

Does it mean that in practice PLs should support just one of them, and get "two-for-the-price-of-one"?

Or does usability demand supporting them both?

Is this decision similar to supporting just And-Not as opposed to full set of (redundant) logical operations?

Does the decision depend on type system, or is fully orthogonal to it?

Constraint-Based Type Inference for Guarded Algebraic Data Types

Quite a mouthful, but look:

Guarded algebraic data types, which subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, and phantom types, and are closely related to inductive types, have the distinguishing feature that, when typechecking a function defined by cases, every branch must be checked under different typing assumptions. This mechanism allows exploiting the presence of dynamic tests in the code to produce extra static type information.

I still have to grok this idea of "dynamic tests producing extra static type information" in its entirety, though.

it's never a language designer's job to define what's a sound software engineering practice. (on the Why Are Type Systems Interesting thread)

Setting aside the discussion on static vs. dynamic type checking, I must say that I find this statement rather puzzling. Aren't PL designers suposed to make SE easier? Isn't the best way to do this to evaluate and consider SE parctices? Isn't that what happens in practice (e.g., mining patterns for language features, library building etc.)?

When I created the software engineering department on LtU I wanted it to focus on language features and language design that are directly concerned with software engineering issues. But my view is perhaps even stronger than that: I think most PL issues are ultimately about SE.

Natrually, one approach is for the language to support whatever SE practices each and every programmer or team chooses. But isn't that simply an example of one sttitude towards the best way to handle the complexity of SE?

I find it incredible that some would argue that PL designers should be agnostics when it comes to SE.

The type systems thread is getting ridiculously long. Please continue the discussion here...

Slate 0.3 has been released. Slate is a language similar to Smalltalk with a prototype based object system and multi-method dispatch.

Daan Leijen. Submitted to the 32nd ACM Symposium on Principles of Programming Languages (POPL'05), Long beach California, January 12, 2005. (PDF, BibTeX)

This paper describes a type system for extensible records and variants with first-class labels; labels are polymorphic and can be passed as arguments. This increases the expressiveness of conventional record calculi significantly, and we show how we can encode intersection types, closed-world overloading, type case, label selective calculi, and first-class messages. We formally motivate the need for row equality predicates to express type constraints in the presence of polymorphic labels. This naturally leads to an orthogonal treatment of unrestricted row polymorphism that can be used to express first-class patterns. Based on the theory of qualified types, we present an effective type inference algorithm and efficient compilation method. The type inference algorithm, including the discussed extensions, is fully implemented in the experimental Morrow compiler.

Always trust Daan to come up with something both elegant and practical...! However the examples involving bottom (undefined) labels left me skeptical.

breve is a free software package which makes it easy to build 3D simulations of decentralized systems and artificial life. Users define the behaviors of agents in a 3D world and observe how they interact. breve includes physical simulation and collision detection so you can simulate realistic creatures, and an OpenGL display engine so you can visualize your simulated worlds.

I guess the on-topic bit is this:

breve simulations are written in an easy to use language called steve. The language is object-oriented and borrows many features from languages such as C, Perl and Objective C, but even users without previous programming experience will find it easy to jump in.

but frankly steve is probably not so interesting in itself; rather breve is just a lot of fun to play with.

Apparently, several AI/robotics groups use breve for their research, but it's very easy to get started and comes with a simple IDE and several demos, of which the most interesting is undoubtedly the Walker, a genetic algorithm which evolves four-limbed walking "plates".

Epigram: practical programming with dependent types

Find the type error in the following Haskell expression:

if null xs then tail xs else xs

Found it? Of course you haven't. But this program is obviously nonsense! Unless you're a typechecker, that is. The trouble is that only certain computations make sense if the null xs test is True, whilst others make sense if it is False. However, as far as the type system is concerned, the type of the then branch is the type of the else branch is the type of the entire if . . . then . . . else . . ..

Statically, the test is irrelevant. Which is odd, because if the test really were irrelevant, we wouldn't bother doing it.

We mentioned this issue in discussions. LtU recently featured Epigram with emphasis on its interactive programming abilities, but I would like to add that Conor McBride's papers are mostly about practical use of dependent types for programming. They are also fun to read, though I can easily imagine how his experiments with presentation, like this one, can annoy some people.