[Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?

[Alexander Solla]

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.  The "characterization" of prelBreak I gave is a  
"type" for prelBreak.  The type is richer than we can express in the  
Haskell type system ("prelbreak accepts a proposition p and a list xs,  
and returns a pair whose first element is the largest prefix of xs for  
which no x satisfies p, and whose second element is the complement of  
the first, taken in xs."), but we can still reason about the richer  
type mathematically, and the Curry-Howard isomorphism applies to it.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100608/119b5a88/attachment.html