Function Types

; The universal property of function objects:
; For any g : z × a → b, there exists a unique
; h : z → (a => b) such that eval ∘ (h × id) = g
;
; eval : (a => b) × a → b
; eval "applies" a function object to an argument.

(define (my-eval func-and-arg)
  ((car func-and-arg) (cdr func-and-arg)))

; A function object: the set of all functions from Bool to Int
; Bool = {#t, #f}, so a function Bool→Int is a pair of Ints.
(define (bool->int-1 b) (if b 10 20))
(define (bool->int-2 b) (if b 99 0))

; eval applies the function to the argument
(display "eval(f1, #t): ") (display (my-eval (cons bool->int-1 #t))) (newline)
(display "eval(f1, #f): ") (display (my-eval (cons bool->int-1 #f))) (newline)
(display "eval(f2, #t): ") (display (my-eval (cons bool->int-2 #t))) (newline)

; The exponential Int^Bool has |Int|^2 inhabitants.
; Each function is determined by two choices: what #t maps to, what #f maps to.

; curry : ((a × b) → c) → (a → (b → c))
; uncurry : (a → (b → c)) → ((a × b) → c)
;
; These are inverses: uncurry(curry(f)) = f, curry(uncurry(g)) = g

(define (my-curry f)
  (lambda (a)
    (lambda (b)
      (f (cons a b)))))

(define (my-uncurry g)
  (lambda (pair)
    ((g (car pair)) (cdr pair))))

; A function on pairs: add two numbers
(define (add-pair p) (+ (car p) (cdr p)))

; Curry it: now takes one arg, returns a function
(define add-curried (my-curry add-pair))

(display "uncurried: ") (display (add-pair (cons 3 4))) (newline)
(display "curried:   ") (display ((add-curried 3) 4)) (newline)

; Round-trip: uncurry(curry(f)) = f
(define add-back (my-uncurry add-curried))
(display "round-trip: ") (display (add-back (cons 3 4))) (newline)

; Partial application falls out for free
(define add10 (add-curried 10))
(display "add10(5):  ") (display (add10 5))

; Demonstrate the isomorphism with finite types.
; Bool → (Bool → Bool): how many inhabitants?
; (Bool^Bool)^Bool = (2^2)^2 = 4^2 = 16
; (Bool × Bool) → Bool: how many inhabitants?
; Bool^(Bool×Bool) = 2^(2×2) = 2^4 = 16  ✓ Same!

; Let's enumerate some:
; Uncurried: takes a pair of bools, returns a bool
(define (f-and p) (and (car p) (cdr p)))
(define (f-or p) (or (car p) (cdr p)))
(define (f-xor p) (not (eq? (car p) (cdr p))))

; Curried versions:
(define c-and (lambda (a) (lambda (b) (and a b))))
(define c-or  (lambda (a) (lambda (b) (or a b))))
(define c-xor (lambda (a) (lambda (b) (not (eq? a b)))))

; They compute the same thing:
(display "AND pair:    ") (display (f-and (cons #t #f))) (newline)
(display "AND curried: ") (display ((c-and #t) #f)) (newline)
(display "OR pair:     ") (display (f-or (cons #f #t))) (newline)
(display "OR curried:  ") (display ((c-or #f) #t)) (newline)
(display "XOR pair:    ") (display (f-xor (cons #t #t))) (newline)
(display "XOR curried: ") (display ((c-xor #t) #t))
; Same answers. The isomorphism preserves behavior.

; Counting functions between finite types.
; |b^a| = |b|^|a|

; Bool = {#t, #f}           |Bool| = 2
; Three = {0, 1, 2}         |Three| = 3

; All functions Three → Bool: 2^3 = 8
; Each function picks a bool for each of 0, 1, 2.

(define (enumerate-three->bool)
  (let loop ((i 0) (count 0) (results '()))
    (if (>= i 8) (list count results)
        (let* ((b0 (if (zero? (modulo i 2)) #f #t))
               (b1 (if (zero? (modulo (quotient i 2) 2)) #f #t))
               (b2 (if (zero? (modulo (quotient i 4) 2)) #f #t)))
          (loop (+ i 1) (+ count 1)
                (cons (list b0 b1 b2) results))))))

(define result (enumerate-three->bool))
(display "Number of functions {0,1,2} → Bool: ")
(display (car result)) (newline)
; 8 = 2^3

; Algebraic laws:
; a^0 = 1    (one function from Void: absurd)
; 1^a = 1    (one function to Unit: always ())
; a^1 = a    (functions from Unit ≅ elements of a)
(display "a^0 = 1: unique function from empty set") (newline)
(display "1^a = 1: every input maps to ()") (newline)
(display "a^1 = a: picking a function Unit→a = picking an element of a")

; Cartesian closed: terminal object + products + exponentials.
;
; In Set:
;   Terminal object = {()}       (unit / singleton set)
;   Product a × b  = {(x,y) | x ∈ a, y ∈ b}
;   Exponential b^a = {f | f : a → b}
;
; The lambda calculus is the internal language of a CCC.
; Every lambda term is a morphism in a CCC.

; Terminal object: unit
(define unit '())

; Product: pairs
(define (make-pair a b) (cons a b))

; Exponential: lambda
; (lambda (x) body) is an element of the exponential b^a

; The CCC structure gives us:
; 1. Pairing:  a → b → a × b
; 2. Projecting: a × b → a,  a × b → b
; 3. Currying: (a × b → c) → (a → b → c)
; 4. Eval: (b^a) × a → b

(define (fst p) (car p))
(define (snd p) (cdr p))

(display "fst(3, 7): ") (display (fst (make-pair 3 7))) (newline)
(display "snd(3, 7): ") (display (snd (make-pair 3 7))) (newline)

; Eval in a CCC = function application
(display "eval(add1, 5): ") (display (my-eval (cons (lambda (x) (+ x 1)) 5)))

; Every well-typed program in a functional language
; is a proof that the corresponding CCC diagram commutes.

; The algebra of types:
; 0 = Void (initial object / empty type)
; 1 = Unit (terminal object)
; a + b = Either a b (coproduct)
; a × b = (a, b)    (product)
; b^a = a → b       (exponential)
;
; Laws (all are type isomorphisms):
; a^0 = 1           Void → a  has exactly one function (absurd)
; 1^a = 1           a → ()    has exactly one function (const ())
; a^1 = a           () → a    ≅ picking an element of a
; a^(b+c) = a^b × a^c   Either → a  ≅  pair of functions
; (a^b)^c = a^(b×c)     currying!
; (a×b)^c = a^c × b^c   c → (a,b)   ≅  pair of functions from c

; Let's verify: a^(b+c) = a^b × a^c
; A function from Either takes a Left or Right,
; so it's equivalent to two separate functions.

(define (either-fn e)
  (if (eq? (car e) 'left)
      (* (cdr e) 2)       ; handle Left (numbers)
      (string-length (cdr e))))  ; handle Right (strings)

; Split into two functions:
(define (left-fn n) (* n 2))
(define (right-fn s) (string-length s))

(display "either-fn(Left 5):    ") (display (either-fn (cons 'left 5))) (newline)
(display "left-fn(5):           ") (display (left-fn 5)) (newline)
(display "either-fn(Right "hi"): ") (display (either-fn (cons 'right "hi"))) (newline)
(display "right-fn("hi"):       ") (display (right-fn "hi")) (newline)
; Same results. One function from a sum = two functions.
; a^(b+c) = a^b × a^c

; Curry-Howard correspondence:
; Types         ↔  Propositions
; Functions     ↔  Proofs
; a → b         ↔  a ⇒ b (implication)
; (a, b)        ↔  a ∧ b  (conjunction)
; Either a b    ↔  a ∨ b  (disjunction)
; Void          ↔  ⊥ (false)
; Unit          ↔  ⊤ (true)

; eval proves modus ponens:
; ((a ⇒ b) ∧ a) ⇒ b
; "If you have a proof of a⇒b and a proof of a, you get a proof of b."

(define (modus-ponens proof-and-evidence)
  ((car proof-and-evidence) (cdr proof-and-evidence)))

; Proof that "even? ⇒ not-odd?" (a specific implication)
(define proof-even-implies-not-odd
  (lambda (n) (not (odd? n))))

; Apply modus ponens: given the proof and evidence (4 is even)
(display "modus ponens: ")
(display (modus-ponens (cons proof-even-implies-not-odd 4)))
(newline)

; Currying proves the deduction theorem:
; To prove a ⇒ (b ⇒ c), assume a and b, then prove c.
; curry : ((a ∧ b) ⇒ c) → (a ⇒ (b ⇒ c))
(display "Deduction theorem = currying")