4 ms·

I like the definition of cons/car/cdr in terms of lambda. A cons cell is just a function you can call to get back the car or cdr. Once you have 'if' and any tw

• jules 12y ago
  There is also an encoding based directly on lambda: (define (cons a b) (lambda (f) (f a b))) (define (car c) (c (lambda (a b) a))) (define (cdr c) (c (lambda (a b) b))) No `if`, no `=`, no `:car/:cdr`. Only lambda!
  • jbert 12y ago
    Nice. It looks like that's effectively using true/false (as defined via lambda) as the two constants and inlining the "if true" and "if false"?
    • jules 12y ago
      Yes, that's easier to see if you wrote your version like this: (define mcons (lambda (a b) (lambda (c) (if c a b)))) (define (mcar p) (p true)) (define (mcdr p) (p false)) In type theory terms this expresses the isomorphism (A,B) ~= (b:Bool) -> (if b then A else B), where the latter is a type called a 'dependent function'. This is a function where the type of output depends on the value of the input. For example if you had (cons 42 "hello") then that would be a function that takes a boolean, and if the boolean is true then it returns the integer 42, and if the boolean is false then it returns the string "hello". So the type of the output depends on the value of the input. This is what dependent types are all about, but that hasn't yet penetrated into mainstream programming languages. Church pairs on the other hand express the isomorphism (A,B) ~= forall r. (A -> B -> r) -> r. For that I find it easier to think in terms of producers/consumers. You can ask yourself "what is a consumer of a pair of type (A,B)?" -> answer: it's a consumer of an A and a B. Therefore we can define cons like this: (define (cons car-value cdr-value) (lambda (consumer) (consumer car-value cdr-value))) Instead of thinking of a cons as a pair, we think of a cons as a function that takes a cons-consumer and it passes its data to the consumer. What kind of consumers can we write? For example, a consumer that sums the components: (define summer (lambda (car-value cdr-value) (+ car-value cdr-value))) Now given a cons, we can sum it like this: (define somecons (cons 4 5)) (somecons summer) -> 9 Now we can define a function sum that sums the components of a cons like this: (define (sum c) (c summer)) Similarly, we can define "cdr-ers" and "car-ers": (define car-er (lambda (car-value cdr-value) car-value)) (define cdr-er (lambda (car-value cdr-value) cdr-value)) Now we define car and cdr like this: (define (car c) (c car-er)) (define (cdr c) (c cdr-er)) The same sort of reasoning works for church booleans, church numerals, church lists, church binary trees, and so forth. That is, you could try to think about this in a dynamically typed framework, but for the more difficult church encodings that becomes almost impossible. At least for me, types really help to bring order to the madness of lambda. If I try to think about what a type like forall r. (F r -> r) -> r means in dynamic terms that causes instant brain melt, from the perspective of types it's a short and innocent expression.
      • jbert 12y ago
        Excellent post. Your type-based approach is a very useful tool for thinking about things which I find difficult. Thanks for that.