Re: [Haskell-cafe] Total Functional Programming in Haskell

On Tue, Sep 30, 2008 at 4:37 AM, Robin Green wrote:

On Tue, 30 Sep 2008 03:27:09 -0600 "Luke Palmer" wrote:

...

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..] = _|_

Bear in mind, in Coq, the equivalent of [1..] is a stream, whereas the equivalent of [1,2,3] is a list.

You miss my point. Every value here is lifted to its domain before being reasoned about. So eg. [1,1..] is not the coinductive x = 1:x. Instead we model this example like so (this is my current direction, nothing tested or fully reasoned out, so I may be full of beans): [1..] is the limit [_|_, 1:_|_, 1:2:_|_, ...] length [1..] is the limit [_|_, _|_, _|_, ...] Every function we can write in Haskell is corecursive on this representation, because every such function is Scott-continuous. To prove the above property would amount to proving that every element of the resulting limit is _|_, so the whole limit is _|_. Luke