[Haskell-cafe] Total Functional Programming in Haskell

Luke Palmer lrpalmer at gmail.com
Tue Sep 30 05:27:09 EDT 2008


2008/9/29 Jason Dagit <dagit at codersbase.com>:
> 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_0768_turner.pdf
>
> 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


More information about the Haskell-Cafe mailing list