Hi
I've been reticent to join this thread as it has the potential
to eat my life, but I thought I'd say some technical things.
On 30 Sep 2008, at 22:54, Derek Elkins wrote:
On Mon, 2008-09-29 at 20:02 -0700, Jason Dagit wrote:
Maybe instead of using (->) as the function constructor for total
On Mon, 2008-09-29 at 20:02 -0700, Jason Dagit wrote:
> 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_tur
On Tue, Sep 30, 2008 at 4:37 AM, Robin Green <[EMAIL PROTECTED]> wrote:
> On Tue, 30 Sep 2008 03:27:09 -0600
> "Luke Palmer" <[EMAIL PROTECTED]> 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 se
On Tue, 30 Sep 2008 03:27:09 -0600
"Luke Palmer" <[EMAIL PROTECTED]> 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
Hi
> 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..] = _|_
In a compiler, with:
default(Int)
main = print $ length [1..]
Results in 2147483647
I don't thin
2008/9/29 Jason Dagit <[EMAIL PROTECTED]>:
> 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
>
> I
Hi
1) Total Functional Programming is great. But a combination of Approve
and Catch gives you termination and pattern-match safety checks for
Haskell, giving you all the advantages of TFP without forcing you to
write total patterns etc. Plus you can use all the Haskell tools.
In reality, neither
