[Haskell-cafe] Total Functional Programming in Haskell

[Luke Palmer]

On Tue, Sep 30, 2008 at 4:37 AM, Robin Green <greenrd at greenrd.org> wrote:
> On Tue, 30 Sep 2008 03:27:09 -0600
> "Luke Palmer" <lrpalmer at gmail.com> 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