On Dec 21, 2011, at 8:52 AM, Jesse Schalken wrote:
> I don't have experience with proof assistants, but maybe my answer to this
> thread can be summed up as giving Haskell that kind of capability. ;)
Okay, then suffice it to say that most of what you said *is* implemented in
real languages like Coq and Agda so you should check them out. :-)
Unfortunately there are two hurdles one faces when using these languages:
first, it is often very cumbersome to actually prove all of the invariants you
want to prove to make your code total, and second, there is not yet a nice way
of doing I/O actions and/or interfacing with external libraries written in
other languages.
However, until we have solved the problems that make working entirely in
dependently-typed languages a pain, we will need to stick with languages with
weaker type systems like Haskell, which means that we can't get around _|_
since we cannot encode all of our invariants into the type system.
Incidentally, I would highly recommend learning more about Coq and Agda. There
is a great textbook to start from available here:
http://adam.chlipala.net/cpdt/
It is valuable because it is not Coq-specific but rather is a good general
introduction to, exactly as the title promises, certified programming with
dependent types.
You should also really check out Agda; the main difference between it and Coq
is the language in which proofs are written. To make a long story short, in
Coq proofs are often easier to write because they use a specialized language
for that purpose but this often makes them a bit of a black box, whereas in
Agda the proofs are fully explicit which makes them much more transparent but
also more verbose and often harder to write. Unfortunately the documentation
for Agda tends to be sparse and split over several kinds of documents (such as
theses, papers, etc.) so isn't an obvious guide for me to recommend to you, but
if you look around you should find enough information to get you started. The
home page is
http://wiki.portal.chalmers.se/agda/pmwiki.php
For me part of the most exciting part was reading through the Agda standard
libraries, which you can download from
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
Just reading through their code is enlightening because it shows you just how
much power is available from dependent types; the standard library also covers
a lot more than Coq's does. Unfortunately it also showcases one of the
limitations of Agda, which is things can often get cryptic and arcane very
quickly, especially since Agda makes you work with "universes" explicitly (Coq
handles them implicitly) which adds another layer of complexity. :-) (FYI,
the universes are a hierarchy such that values are at the bottom, types of
values one rung up, types of types two rungs up, types of types of types three
rungs up, etc. Haskell is limited in only having a three-level hierarchy, with
values, types, and kinds.)
Cheers,
Greg_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
