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.