Lennart Augustsson wrote:
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.
But wouldn't that alternate way break the principle, recommended by
Cardelli, that all code should be well-typed and the types of all terms
should be, shall we say, "plainly" deducible from the code alone (i.e.
not requiring any "difficult" reasoning on the part of the human
reader)? If not, could you give an example to illustrate your point?
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.
Well I thought someone might say something like that - which is why I
called them "angles" on the question. :)
But while statements about types and statements about values might be
inter-convertable, I think they look different and one can be more
convenient than the other for various purposes. I've only used dependent
types trivially so I could be wrong.
--
Robin
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
