Lambda the Ultimate

I don't know if this is the true explanation of the Zune blackout, but if it is it is bloody hilarious.

From by basic understanding, in System F, a polymorphic function is a single value that can be directly applied to an argument. I want to know: is there a formalism where a "polymorphic function" is really a declaration of a family of monomorphic functions, indexed by the types used for instantiation. Thus, two calls to the same [nominal] polymorphic function with different types would resolve to two calls to different monomorphic functions. Clearly this model is more towards the C++ idea of function templates than the FP idea of polymorphic functions.

For polymorphic functions with these semantics, it seems that there would be a more clear distinction of what can be resolved at compile-time, using the type information available at instantiation, and what needs run-time dispatch. Perhaps, then, this formalism could also be used as a target language of an optimization that specializes true (System F) polymorphic functions.

So, does anyone know any work in this direction?
Thank you!

In a recent discussion about adding some dependent typing capabilities in BitC, it was proposed that we should instead statically reject programs that contain unsolved constraints, and require that the programmer take responsibility for inserting checks explicitly. The idea is that these checks can still be compiled out, but making them visible to the developer may have the effect of diagnosing bugs or inducing better arrangements of code. I'm not yet fully convinced, but I'm thinking about it. Here is the "catch" that I see:

When unsolved constraints lead to compile-time program rejection, the behavior of the solver becomes part of the language specification. It becomes necessary to specify a standard set of verification conditions that the compiler must generate (which seems straightforward), a standard rule base over which the solver must operate, and a standard behavior by which the solver must combine these rules. Individual implementations are certainly free to use better solvers, rule bases, or verification conditions but the language specification must define precisely what constitutes a "compliant" program, and compilers must retain the capability to identify programs that are not transportable (that is: programs that would not be accepted if the enhanced solver were not applied). Finally, if the language definition is to be deterministic, it would seem to follow that the reference solver must operate by exhaustive search, and must be assured to terminate.

So two questions:

• Am I overly conservative when I say that the solver must be exhaustive and terminating? Can a precise baseline language definition be had with weaker restrictions?

• Has there been any work on specifying solver behavior in this sort of way? By specifying, I mean in the sense of a reference language specification, but also in the sense that the language reference solver specification could be handled properly when the programming language is to be embedded in a prover for verification purposes?

  An ad hoc specification in the form of a reference implementation is certainly possible, but this seems like a pretty weak way to go about specifying a language. Particularly so if later program verification is desirable.

Anyway, what is the state of the art concerning solver specification?

Wadler, for instance, makes the claim, in "The marriage of effects and monads" (pg. 1), that effects typing systems are usually found in strict languages, whereas monads are usually found in lazy languages. Why is this? Is there a technical reason, or just a difference in cultures between the two camps?

(I have seen others make an even stronger claim, that monads are especially suited for lazy languages, in some sense.)

Microsoft recently demoed a very interesting system for kids called Kodu. Kodu lets kids 'program' their own games for Xbox 360.

The language lets kids write programs like this:
when [game-pad] [left-click] do [fire] [at-monster]

Except game-pad, left-click, etc. are cartoonish icons kids pick out from context relevant lists.

This summary is based on watching two videos, at most a few minutes in length :) The video in the link is probably most relevant. There doesn't seem to be any more technical detail available on the web.

Greetings all. I just wanted to tell people that Jane Street is (still) interested in hiring functional programmers (of which many are of course denizens of LtU). Despite the problems besetting much of the financial industry, we have grown strongly in the last few years in our people, our technology, the scope of our business and its profitability. We now have over 30 OCaml developers, and we are actively looking to hire more in Tokyo, London and New York.

For someone who cares about functional programming, Jane Street is an interesting place to consider. Jane Street has invested deeply in OCaml, to the point where we now have the largest team of OCaml programmers in any industrial setting, and probably the world's largest OCaml codebase--almost a million lines. We really believe in functional programming, and use OCaml for everything from research to systems adminstration to trading systems.

The atmosphere is informal and intellectual, with a focus on learning. The work itself is deeply challenging, and you get to see the practical impact of your efforts in quick and dramatic terms. Jane Street is also a small enough place that people have the freedom to get involved in many different areas of the business.

Unlike many financial firms, software and technology are considered a core part of what we do, not some segmented-off cost center that the people who run the business don't think about. Jane Street is a place where people really care about the quality of the software, to the point that several of the most senior members of the firm, who do not have technology backgrounds, nonetheless review critical portions of the codebase before they can go into production.

If you'd like to learn more, here are some links. First, here's a paper I wrote for the Monad Reader:

http://www.haskell.org/sitewiki/images/0/03/TMR-Issue7.pdf

We also have a technically-oriented blog:

http://ocaml.janestreet.com

For a (recruiting-oriented) overview of Jane Street, here's the firm website:

http://janestreet.com

If you're interested, send a resume and cover letter to yminsky@janestreet.com

I am looking for references to the above, especially for implementations in ML-like languages.

Rationale, I needed to write a comparison function for the content of binary trees. Using a coalgebraic structure to decompose the two trees in steps was the only solution I could think of. I am looking for possible generalizations of what I used.

It looks like CPS, but it would be interesting to see it explained better.

I'm wondering how people would feel about setting up some way for companies that want to hire functional programmers to broadcast that fact on LtU. Jane Street is eagerly trying to hire the kinds of people who read LtU, but there's no natural place on LtU to communicate that fact. I've sent a number of messages over the years to a few FP mailing lists, but there's no natural place to post such a thing on LtU. Maybe it would make sense to set up some kind of job board? I know we'd be interested in using it, and I'm sure there are a few other companies who would be interested as well.

I just noticed that nearlyfreespeech.net provide cgi web hosting for Haskell, Lisp, OCaml, and Scheme and I thought this could be of interest to a few LtU members. (I wonder what the collective pronoun for "LtU members" is?)

Yesterday I signed up with them to transfer a couple of hardly used domains to them because I read some positive comments about them, and because I liked their prices and policies... and I was pleasantly surprised to see they support Haskell! The transfers went well, and I don't have any self-interest in promoting them; I am just a happy customer so far.

The paper of the subject title might be of interest.
A cursory search on "blame" didn't reveal any prior posting.