[Haskell-cafe] is there a way to prove the equivalence of these
two implementations of (Prelude) break function?
Alexander Solla
ajs at 2piix.com
Tue Jun 8 14:01:03 EDT 2010
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
More information about the Haskell-Cafe
mailing list