2008/9/29 Jason Dagit
Hello,
I recently had someone point me to this thread on LtU: http://lambda-the-ultimate.org/node/2003
The main paper in the article is this one: http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0...
It leaves me with several questions: 1) Are there are existing Haskell-ish implementations of the total functional paradigm? 2) Could we restructure Haskell so that it comes in 3 layers, total functional core, lazy pure partial functional middle, and IO outer layer?
Aye. I'd say you pretty much need dependent types if you want to do interesting things and prove totality at the same time. Or that might be better stated as: as long as you're proving totality, why not use dependent types? :-) But I *want* to do something like that with Coq (I prefer it to Agda for little more than personal taste). In particular, I'd like to see a reasoning framework for partial functions, so you could state and prove a property like: length [1..] = _|_ As well as generate Haskell code for the partial functions which you are reasoning about. I've been idly pondering how to do this. Does anyone know about something like this for coq or agda? Luke