Lambda the Ultimate

Yeah, in the end, the key point seems to be that dependent types give you more practical leverage from the Curry-Howard Correspondence (which, thanks to this forum, now always sounds in my head like "Dear Ma, Larry boinked me in the eyes again today...") than other systems do. On one hand, that is indeed a "no kidding" point, as anyone using any of the good theorem provers can tell you—and I do intend to review Coq'Art after I've gotten a bit farther through it.

But what's nice to see in this paper is how much Epigram succeeds at seeming like just a more powerful programming language, without the fumbling around with tactics and the "great, here's my proof; how do I get a program out of it?" aspect of even very good "certified program generating" theorem provers such as Coq. I think this is unbelievably important, and honestly I think that even a lot of programmers who have heard of the Curry-Howard Correspondence would be surprised to find that their software in a language like Epigram was simply "correct by construction" some of the time, and that some fraction of the rest of the time could still be expressed within the language itself. Results like that are why we care about type theory in the first place.

Agreed.

I have to say though that I do believe we won't see languages as powerful as epigram gain widespread use until there are some compilers that can propagate the types down to the assembly level, play nice with seperate compilation, and do a respectable amount of interesting optimizations.

The FLINT project and related projects are close to that. I would be more surprised if there wasn't a compiler that fit those requirements somewhere (depending on what "interesting" means). Incidentally, the paper should also have impact on proof carrying code and related techniques (i.e. it should be much easier to generate PCC for more sophisticated properties given a more typed language).

ooops, I was imprecise in what I was saying.

I meant type preserving compilation for type systems at least as powerful as those of Epigram or Coq. This turns out to be a technically challenging problem, because one has to find a point in the design space where issues such as termination, and phase distinction (to name but a few) are dealt with in a satisfactory manner. I claim that all currently existing approaches fall short.

Augustsson's Cayenne compiler throws away the type information and then just runs the LML compiler with type checking turned off.

Xi's work with ATS and such, while enabling the programmer to prove theorems about the program, is still not quite the right way to go. The explicit seperation between proofs and programs (while good from an erasure standpoint) makes learning to use those features just that more challenging, and moreover the type system doesn't make the language more expressive, it is instead meant to more precisely capture the invariants needed to rule out errors that are possible with ML's type system (eg tail [] )

epigram's compilation style doesn't play nice with seperate compilation, and thats not good.

coq's extraction to OCaml doesn't count, because of the need to introduce copious uses of magic coercions, and the added dependency of relying on the Ocaml compiler correctness (though thats probably not an issue in pratice).

I do think we'll be seeing compilation technology that plays nice with the intersection of type preserving compilation, seperate compilation and powerful type theories such as that of Epigram sometime in the next year or so , but as yet it doesn't exist.

I continue to wonder why we don't see more research around principal typings, especially given the results in ML Has Principal Typings. Since someone recently asked, a good starting point for learning more about principal typings is Trevor Jim's What are principal typings and what are they good for?. Of course, now I need to learn what the relationship between dependent types and principal typings is.

I should point out that the notion of principal typings (while a property of a type system) has to do with type inference. So I suppose there is a connection in the sense that (partial) type inference for dependent types is in many respects an open problem, but thats about it.

by the way
Has anyone included a link to Barendregt's paper Lambda calculi with types in the tutorial section? Its a nice document that goes from the simply typed lambda calculus all the way to pure type systems and goes over the both church and curry presentations of type systems.

heres the link ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps

We're apparently both being vague today. :-)

I meant that type systems with principal typings (vs. principal types!) support nice features such as incremental type inference and separate compilation, to your point about separate compilation. But it occurred to me that this might not be a win if we can't come up with a dependent type system that has principal typings! In googling around, it appears that most principal typings research has occurred in the context of intersection types, and there are some rumblings around dependent types and intersection types, but I still have a tremendous amount to learn about both, so I'll shut up now.

actually, i think theres a bunch of work on dependent intersection types for Nurpl or Metaprl... I don't have any links handy, but i do know that the work was done by some folks at cornell.

Why is separate compilation necessary? Incremental compilation a la Epigram 1 seems to reduce (if not eliminate) the need for it.

The only application I see is for non-free software libraries, which I have little interest in. Is this anything more than a political issue?

I would think that seperate compilation is vital for any massive collaborative project... Especially if various parties are working on discrete components that serve as libraries to other components.

If memory serves, Epigram 1 (as described in Edwin Brady's thesis), tranforms the code into a bunch of supercombinators. Thats not amenable to incremental compilation, thats as whole program as compilation schemes get!

This paper describes a certified program verifier constructed by propagating safety properties that arise from a high level language's type system down through a few steps through assembly. It seems this work uses Coq as a dependently-typed programming language, mostly reserving the use of automation to constructing proof terms.

I'm a neophyte in this discussion (er, and I am with most of what is on LtU), but I think terms have gotten confused along the way of this discussion :-) It wasn't incremental compilation, it was separate compilation: how do you have Epigram slap together disparate modules (some from raw source, some already "compiled") to support component-oriented production?

To continue on that riff, how do you get it to talk to libraries that were not written in Epigram? Does it have a good debugger? What about a profiler? Basically, how does one do "real" software production? (Presumably, one might take issue with how "real" software production is done today and outline how Epigram etc. might offer an importantly different approach.)