# [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...
{"ft_lang_label":"__label__en","ft_lang_prob":0.8472879,"math_prob":0.81704223,"size":1152,"snap":"2023-14-2023-23","text_gpt3_token_len":301,"char_repetition_ratio":0.108013935,"word_repetition_ratio":0.0,"special_character_ratio":0.2638889,"punctuation_ratio":0.139738,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.95106596,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2023-03-20T08:48:27Z\",\"WARC-Record-ID\":\"<urn:uuid:ee7508d4-876c-42ac-8664-8475d7e324c4>\",\"Content-Length\":\"4306\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:b07366f8-4be2-4742-baca-3fdce30c81c4>\",\"WARC-Concurrent-To\":\"<urn:uuid:f64fc69e-1808-45ab-b1d6-9084e40833cb>\",\"WARC-IP-Address\":\"23.253.242.70\",\"WARC-Target-URI\":\"https://mail.haskell.org/pipermail/haskell-cafe/2010-June/078712.html\",\"WARC-Payload-Digest\":\"sha1:KUCTTCRSKDHG4N6EQ3VQP3EOMUCWEN5Q\",\"WARC-Block-Digest\":\"sha1:2LFS2F7VJAMQRJ64IDGT62MWIRJS3GAR\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2023/CC-MAIN-2023-14/CC-MAIN-2023-14_segments_1679296943471.24_warc_CC-MAIN-20230320083513-20230320113513-00444.warc.gz\"}"}