On Jun 8, 2010, at 2:38 AM, Alberto G. Corona wrote:
This is`t a manifestation of the Curry-Howard isomorphism?
Yes, basically.
If we rephrase the isomorphism as "a proof is a program, the formula
it proves is a type for the program" (as Wikipedia states it), we can
see the connection.
On Tuesday 08 June 2010 08:33:51, David Virebayre wrote:
> On Sun, Jun 6, 2010 at 5:10 AM, Thomas Hartman
wrote:
> > Here's two implementations of break, a snappy one from the prelude,
>
> ...
>
> > prelbreak p xs = (takeWhile (not . p) xs,dropWhile (not . p) xs) --
> > fast, more or less as impl
Hello David,
Tuesday, June 8, 2010, 10:33:51 AM, you wrote:
> ( my guess is USE_REPORT_PRELUDE compiles functions as defined in
> the haskell report, but the other version is faster and used by default. )
you are right
--
Best regards,
Bulatmailto:bulat.zigans...
> This isn`t a manifestation of the Curry-Howard isomorphism?
>
> 2010/6/8 Alexander Solla
>
>
>> On Jun 7, 2010, at 4:10 PM, Alexander Solla wrote:
>>
>>
>>> You might note how much like evaluating the function generating the
>>> analysis is.
>>>
>>
>>
___
On Sun, Jun 6, 2010 at 5:10 AM, Thomas Hartman wrote:
> Here's two implementations of break, a snappy one from the prelude,
...
> prelbreak p xs = (takeWhile (not . p) xs,dropWhile (not . p) xs) --
> fast, more or less as implemented in prelude iiuc
I had a look at the prelude, and I was surprise
On Sat, Jun 5, 2010 at 8:10 PM, Thomas Hartman wrote:
> Here's two implementations of break, a snappy one from the prelude,
> and a slow stupid stateful one.
>
> They are quickchecked to be identical.
>
> Is there a way to prove they are identical mathematically? What are
> the techniques involve
On Jun 7, 2010, at 4:10 PM, Alexander Solla wrote:
For exposition, I'll do the analysis for the Prelude function. You
might note how much like evaluating the function
Correction:
You might note how much like evaluating the function generating the
analysis is.
___
On Jun 5, 2010, at 8:10 PM, Thomas Hartman wrote:
Is there a way to prove they are identical mathematically? What are
the techniques involved? Or to transform one to the other?
Typically, the easiest way to prove that functions f g are equivalent
is to (1) show that their domains are the sa
Here's two implementations of break, a snappy one from the prelude,
and a slow stupid stateful one.
They are quickchecked to be identical.
Is there a way to prove they are identical mathematically? What are
the techniques involved? Or to transform one to the other?
import Control.Monad.State
imp
