Robin Green wrote:
2. Dependent types: By programming in a dependently-typed functional
programming language such as the research language Epigram, it is
possible to write functional programs whose types force them to be
correct. See for example "Why Dependent Types Matter" by Thorsten
Altenkirch, Conor McBride, and James McKinna. However, in my opinion
this is only useful for simple "sized types" such as "a list of length
6". For more complicated properties, I believe this approach is
unnecessarily difficult, and does not match how mathematicians or
programmers actually work. My approach (see above) clearly separates the
programming, the theorems and the proofs, and (in principle) allows all
three to be written in a fairly "natural" style. As opposed to dependent
types which, in Epigram at least, seem to require threading proofs
through programs (for some non-trivial proofs).
I would just like to point out that there is nothing that forces you
to "thread" the proofs through the programs. With dependent types you
have this option, but you can also write standard "Haskell" code and
have your proofs be separate. It's up to you to choose which way you
do things. (If you do separate proofs you can even add some construct
to the logic that makes it classical if you like.)
Furthermore, I don't see such a clear separation between your points
1 and 2. With dependent types you are making proofs and then using them
as programs. How much extraction you do is a matter of optimization,
I'd say. And how efficient the extracted program is depends on which
proof you choose to do.
-- Lennart
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
