A common language for dependently-typed programming?
The Haskell project was begun in order to unify "more than a dozen non-strict, purely functional programming languages". (mirror) We are rapidly approaching that many viable choices for programming with dependent types.
- Epigram
- ATS (successor to Dependent ML and Xanadu)
- Agda (successor to Cayenne)
- Ωmega
- NuPrl
- Twelf
- Isabelle
- Coq
- Delphin
- Concoqtion
- Aldor
- Guru (successor to RSP1)
- Some of the items on this list are theorem provers first and dependently-typed programming languages second. Adam Chlipala argues that this is not such a problem for Coq.
- This list does not include several languages that are new or new variants (PIE, Matita), not checked at compile-time (Sage), or not actively maintained (most proof assistants, Charity).
- Some of these choices may not be real options for programing with dependent types. Twelf is designed for programming about programming languages, and, if I remember correctly, doesn't have parametric polymorphism because of something having to do with higher-order abstract syntax. Aldor can't understand most type equalities, making its dependent types somewhat weak, though Atypical and Aldor-- aimed to remedy this five years ago. Agda and Epigram have New Exciting Versions 2 coming out, so they suffer from the Osborne Effect.
I'm not sure, though deciding how to ensure termination seems particularly tricky. Nonetheless, there are other decisions that aren't as directly related to the central dependent type issues, like syntax, functional purity (though this is related to termination), and editing environment. Maybe these issues will divide the ecosystem into a few niches, each dominated by one player. In the meantime, it's tough to choose.
9 comments:
This is certainly a good question. My feeling is that we're not yet in a good place to standardize, but that it's certainly worth trying to figure out where there are too many or too few good ideas.
Too many ideas: there's a gap between what we might call the "System F + static terms" approach and the "dependent type theory as a programming language" approach. ∀ in the former and Π in the latter really are different beasts, and Σ is yet more divisive. Variations on System F fit directly with existing compiler technology and are in any case closer to people's comfort zones. The type theorists are much better at manging the complexity of dependency, but have yet to deliver a convincing run-time model (as opposed to strong normalization for proof-checking) integrated with a programming language: the pieces exist, but are lying around on the floor.
Too few ideas: there are lots of issues where people are thinking interesting thoughts, but where no coherent treatment has yet emerged. Programming in the presence of effects (eg nontermination) is one such. There are some good ideas about the semantics of effects (parametrized monads, coinductive treatments of partiality, etc), but we still don't know what the programs should look like.
Another major design challenge is to cope with our new freedom to shift the precision of data structures (lists, vectors, sorted lists; raw terms, typed terms). Our current languages (with the honourable exception of those featuring refinement types) allow datatypes to be invented out of the blue, but not designed in relation to other datatypes. Hence we have a proliferation problem with no way just now to express and exploit the systematic connections between types which are variations on a theme. If we want a language with a library, not just a gallery, then we need a more coordinated approach to this problem.
At the moment, I think it's good that there's a lot of diversity, because it gives people freedom to tackle design challenges with relatively little baggage. It's tempting, I know, to push for a standard, and then an "industrial strength" implementation, but I'd argue that any standard we chose now, we'd come to regret only a few years down the line, because we just don't know enough.
I'm heartened with the direction Haskell (a notable exception from your list) has taken lately, in that it provides access (by decreasingly devious means) to the basics of dependently typed programming. I'd like to help that trend continue. Haskell's success buys us freedom to think more creatively about how dependent types can change programming for the better. We should standardize when we can see a coherent way to deliver generational change.
Agda does not suffer from the Osborne effect. Version 2 can be downloaded here: http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php
The link in my last comment doesn't seem to have come out right. Download Agda2 here
Josef,
The Agda homepage says Agda2 is in alpha testing. Also, is there documentation for Agda2, other than Ulf Norell's Ph.D. thesis?
Actually, when I last checked, there were at least three pages, each on three different servers, masquerading as "the" Agda home page!
Clearly, someone needs to mark the old pages as deprecated or turn them into HTTP redirects.
Jim,
First of all, I'm not working with Agda in any way. I only have my office in the same building as some of those that do.
It is true that the design of Agda 2 is not finalized. But it seems unlikely that any major changes will be made now and it is very usable as it is right now.
As for the link you provided, I wouldn't trust it when it comes to Agda 2. Version 2 development has been done mostly at Chalmers, the Japanese guys are mostly users of the Agda system. Some very sparse documentation on Agda 2 can be found via the link I posted. More helpfully perhaps are the examples that comes with the download.
I think I understand now. Nonetheless, I'd be hesitant to use a PL that didn't have a reference manual.
I think lack of a reference manual is a very good reason not to use a language for serious application development. But it's a lame excuse for failing to engage with ideas. You need to clarify in what ways you're interested "to use a PL". If you want to deliver software written in a dependently typed style, don't bother with any of the above: use Haskell. If you want to experiment with possibilities, technologies, and approaches, many of your list have interesting lessons to teach. I have no hesitation recommending Agda 2 as a source of education and entertainment. The materials available (including Ulf's thesis) are more than enough to get you moving. That's certainly been my experience, and that of several friends and colleagues.
The situation is that you're remarkably lucky if have to choose between writing the reference manual and writing the next grant application. Reality usually delivers your kicking much earlier in the process.
Things have got a bit heated, and I didn't mean for that to happen.
It's tricky to say what the proper balance is between language stability and getting to using the exciting new stuff. I'm not willing to defend a particular point in that continuum, because it's too tricky for me and because each project probably has its own complex considerations. I don't think Agda 2 is so undocumented as to be uninteresting for education, experimentation, or entertainment.
I do get more out of exploring well-documented languages than those where the presentation I need to understand the PL behavior is just not available. If I don't understand what's going on with a Coq script, there are lots of documents I can go to for help. If I don't understand what's going on with an Agda 2 program, I may have to convince someone to help me with something basic when that person would be much better off writing grant applications. Wouter (Swierstra, I assume) may have said it better:
"I sometimes run into problems with implicit arguments, indexing data types by a function, modules, etc. Usually I manage to solve this by e-mailing Ulf, but I would like to see more exact specifications of what you can and cannot do. Even if it just consists of a well-documented, nicely formatted list of examples - it would make a big difference."
Perhaps more to the Osborne example, since 2.0.0 just came out six months ago, I think it's quite possible that more documentation is coming, and until then, it is tempting to direct my attention to the many other interesting projects available.
Post a Comment