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))))

The stair climbing robot

An interesting problem called "the stair climbing robot" was recently posted on LtU.

Your stair-climbing robot has a very simple low-level API: the "step" function takes no argument and attempts to climb one step as a side effect. Unfortunately, sometimes the attempt fails and the robot clumsily falls one step instead. The "step" function detects what happens and returns a boolean flag: true on success, false on failure. Write a function "step_up" that climbs one step up (by repeating "step" attempts if necessary). Assume that the robot is not already at the top of the stairs, and neither does it ever reach the bottom of the stairs. How small can you make "step_up"? Can you avoid using variables (even immutable ones) and numbers?

I thought I'll try to solve it using muSE's lcons lazy function. Here's a solution -

; A step function which fails 50% of the time.
(define (step) 
    (if (= 0 (rand 2)) 
        (do (print "DOWN") ()) 
        (do (print "UP") T)))
 
; Gets the second element of a list s,
; forcing the value of the first element if
; the list happens to be lazy.       
(define (forced-next s) (first s) (first (rest s)))

; (steps) generates a sequence of
; successful upward steps. To climb N steps,
; just take N elements from (steps).
(define (steps)
    (lcons (if (step)
                T
                (forced-next (rest (steps))))
            (steps)))

; Climb 1 step
(take 1 (steps))