Lambda the Ultimate

BitC is back:

As I get ready to leave Microsoft, I'm once again thinking about BitC. I
want to get the implementation and the language definition to a point of
usability, and this seems like a good time to examine some of the things
that I think, in hindsight, were mistakes or might warrant re-examination.
Most of these issues are mundane practical things. A few of them are deeper
design choices/issues.

I didn't really look at BitC till the project went dormant. Now I have, I think it's great. Every language should have a BitC-like implementation layer.

I recently came across the concept of regular expression types, such as in XDuce. The idea seems promising, but the current implementations all seem excessively restrictive (disallowing nontrivial patterns), so I was wondering about the feasibility of further development in this area. The bottleneck for regular types would definitely be in trying to determine subsumption of these types in an automated manner, but I can't seem to find much literature on the subject.

Computationally how hard is it to determine equivalence/subsumption of regular languages in general. Finite? Hard? Easy?

For at least some languages (a+ <: a*) this sort of comparison seems plausible. If this comparison isn't plausible in general, is there any way to foresee which languages are easy to compare/hard to compare?

Ehud is about to be annoyed with me. :-)

I am lately suffering from doubts about whether the value of proof is justfied by its cost. Some questions, in no particular order:

• Proof seems to be an all-in or all-out exercise. There does not seem to be a viable strategy for initial, limited adoption followed by progressive improvement. Type systems seem to be more "continuous" in their adoption options. Given the (admittedly incomprehensible) expressive power of something like ATS, what is the real semantic gap between provers and type systems these days? Do type-based property embeddings offer the possibility of more incremental and more cost/benefit-aware adoption of checking techniques?
• The goal of proof isn't to be correct. It is to be confident. This has two parts: (1) confidence that you got something right, and (2) ability to convince a second party that your confidence is justified. Assume that you succeed in your proof. To what degree has use of a prover inherently failed objective [2]? If the final objective is credible correctness, then there is presumably a trade-off between accuracy and comprehensibility. Does proof (in its current form, at least) err too much on the side of accuracy?
• Given the likelihood of (possibly retrospective) failures of total abstraction, to what degree is confidence in proof misplaced? If so, is the cost of discharge justified?

There is no question in my mind that proof processes generate more robust code. Yet the general concensus seems to be that this robustness is much more an emergent consequence of rigorously understanding the problem then a result of the proof discharge. In this view, the primary benefit of proof (in the context of assurance) is largely to keep the specification "honest". If this is in fact the goal, is proof the best way to accomplish that goal? How much of that goal can be undertaken by type systems?

In a private conversation, Gernot Heiser (NICTA, OK Labs) was recently asked how use of proof impacted their QA costs. As I recall it, his answer was that they run between 1.5x and 2x the end-to-end cost of conventional development and testing, but they achieve much higher confidence. My questions:

• Might there be a better trade-point between cost and value (in the form of confidence)?
• To what degree is their confidence well-founded?

In a second private conversation, Eric Rudder observed that one of the costs of proof-based methodology was a loss of ability to rapidly adapt software to new requirements and new demands. It follows that proof is not always appropriate, and that a more continuous cost/time/benefit option space would be desirable.

My own observation is that in the end, systems need to be robust, and they include components that lie well outside our ability to prove them. In many cases, type can be usefully exploited when proof cannot, and there is a training cost to educating people in both domains.

So finally my question:

Once we step away from formal semantics and PL insights (which are certainly good things), what is the proper role of proof in real-world production? And what is the proper role of advanced type systems?

Hi LtU,

I'm working on the design of a programming language (as I'm sure many of you are). And sometimes I feel the need to brainstorm about a new idea. LtU looks exactly like the kind of community I want to reach. My experience with different programming languages is limited (I'm basically a C++ guy) and I want to learn.

The LtU forum is not meant for design discussions, but I've been allowed to post a link to another discussion group. If you would like to respond, please do it there, not here. Any thoughts would be most appreciated!

Type system design choices

The program for this year's Code Generation conference is now available at: http://www.codegeneration.net/cg2010/programme.php

The conference, now in its fourth year, is Europe's leading event on Model-Driven Software Development.

Highlights include:

- keynotes from (Pragmatic) Dave Thomas and Eelco Visser (Delft University of Technology)

- Language Extension with MPS: Markus Völter (independent/itemis AG) / Konstantin Solomatov (JetBrains, s.r.o.)

- Proven best practices for successful MDD adoption: Steven Kelly & Juha-Pekka Tolvanen (MetaCase)

An early-bird booking period runs until 1st April with up to 20% off booking fees. Full-time academics can also claim a further 20% discount.

The event takes place 16-18 June 2010 in Cambridge, UK.

Visit http://www.codegeneration.net/cg2010/ for more information.

C. Guy Yarvin recently published an interesting new project in language/systems design. It includes a simple formal model of computation called Nock ("comparable to the lambda calculus, but meant as foundational system software rather than foundational metamathe­matics") and a self-hosted language called Watt that compiles to Nock. The motivation? To provide a fully-specified foundation for Urbit, a hypothetical system architecture that uses content-centric networking to distribute code and data in a functional global namespace.

Yarvin's own descriptions are rather lengthy, so I tried to provide a shorter introduction here.

Interesting questions for LtU readers: Nock formulas are terribly inefficient for real computation (for example, decrement(n) is an O(n) operation). Yarvin intends to make Watt efficient by writing fast implementations (in C, say) for standard "kernel" functions like decrement, add, multiply, and more. He calls these fast native implementations "jets." So how one can trust that jets are equivalent to the functional Nock/Watt code that they replace? Yarvin has proposed the classic n-version software engineering trick of comparing both implementations with the same inputs, but in addition the classic problems with that approach, there is the additional hurdle that the pure Nock code might be so inefficient that it is impractical to run it on most inputs. Is the goal of a minimal pure standard compromised by the need to implement a common set of "impure" jets too?

I came across this paper proposing that Let Should Not Be Generalized (TLDI 2010, Vytiniotis, Peyton Jones, and Schrijvers).

While generalisation for local let bindings is straightforward in Hindley-Milner, we show that it becomes much more complicated in more sophisticated type systems. The extensions we have in mind include functional dependencies, GADTs, units of measure, and type functions. The only technically straightforward way to combine these developments with let-generalisation has unpalatable practical consequences, that appear to be unavoidable.

I'm actually fairly convinced by this. Among other things, it provides a fairly clear path to eliminating the monomorphism restriction:

Our [] proposal completely subsumes the [Haskell monomorphism restriction] for local let bindings, so the MR would then only apply to top-level bindings. In that case the arguments for its abolition, or for generating a warning rather than rejecting the program, would become very strong. A nasty wart would thereby be removed from the face of Haskell.

Are they right? Are they wrong? Has anyone laid out the case for the defense?

I am pleased to announce that LaTiKi is now available as a public beta.

LaTiKi accepts LaTeX syntax as input rather than the wiki syntax that is
standard across many wiki implementations. This Wiki enables LaTeX users to
collaborate on papers, edit, and track each paper. It is entirely based upon
the open-source and widely used platform MediaWiki. I am looking for
interested users to contribute, try out how well the system works and how
useful the system really is. I also hope that any major underlying bugs are
identified.

I have prepared a sandbox wiki with some of Philip Wadler's papers on the
site to demonstrate how the system works. Note that to be able to edit
papers on the sandbox you MUST sign up to the site and confirm your email
address. This is available at http://www.stuartbeard.com/wiki
Feedback is greatly appreciated.

If any readers are interested in this project and would like to do a similar
thing with their own papers then a tarball is available
at http://www.stuartbeard.com/project or http://www.mediafire.com/file/lymzlwz3m0m/latexwiki-1.0.1b.tar

I've been watching the interpreter and JIT compiler competitions a bit in the JavaScript and Lua worlds. I haven't collected much organized data but the impression I'm getting is that tracing JIT's are turning up as the winners: sometimes even beating programs statically compiled with GCC. Is there a growing body of evidence that tracing JIT compilers are the horse to bet on? Will a more static style JIT like Google's V8 be able to keep up?

Thanks,
Peter

[I promoted this item to the front page, since the discussion is highly interesting & informative. -- Ehud]

didn't see it mentioned yet. i would excerpt the abstract were it not for the fact that the pdf is horribly broken such that no spaces are copied-and-pasted. yay usability.

the gist: statically typed collections library ends up with duplication, ironically? and new advances let it be excitingly refactored to make everybody happy again. i think that is interesting because i do believe static typing has some gotchyas.