[Haskell-cafe] Total Functional Programming in Haskell
lrpalmer at gmail.com
Tue Sep 30 10:16:54 EDT 2008
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 _|_.
More information about the Haskell-Cafe