Curry Howard isomorphism

Curry Howard isomorphism states that every logical proposition corresponds to a type. (See also Curry-Howard-Lambek correspondence.) I've been fascinated by this recently, in the context of Haskell, 'cos it yields very interesting and powerful functions. Often you can just take the type expression in Haskell and write a function that has the type.

For example, consider the trivial logic "theorem" -

If it is true that proposition A implies proposition B, then A is provable implies B is provable.

If you notate provability by the symbol #, you can write that as -

(A => B) => (#A => #B)

If you consider => to be the function type constructor (in Haskell), this gives you the type of fmap where # is any functor. It looks like you can uniformly map "is provable" to some kind of containment - like a list or a set.

Here's a very interesting function derived from another logic proposition - From Löb's Theorem to Spreadsheet Evaluation.

Here's an implementation of the loeb function in muSE -

; Limitation - fmap over lists only
(define (fmap f x) 
    (if x 
        (lcons (f (first x)) 
               (fmap f (rest x))) 
        ()))
(define (loeb x) (fmap (fn (a) (a (loeb x))) x))

.. and a variant on the author's example -

(define test
    (list   (fn (x) 17)
            (fn (x) (apply + (drop 3 x)))
            (fn (x) (* 2 (nth 3 x)))
            (fn (x) (+ (nth 4 x) (nth 5 x)))
            (fn (x) 3)
            (fn (x) (nth 0 x))))