What.rkt

#lang plai-typed

(define-type-alias number-like-function (('n -> 'n) 'n -> 'n))
(define-type-alias (chooser-of 'm) ('m 'm -> 'm))
(define-type-alias (pair-of 'q) ((chooser-of 'q) -> 'q))
(define-type-alias (accessor-of 'r) ((pair-of 'r) -> 'r))


(define 
   (add1 [f : number-like-function]) : number-like-function
    (lambda ([g : ('t -> 't)] [t : 't]) : 't
      (f g (g t))))

(define 
   (con [a : 'a] [b : 'a]) : (pair-of 'a)
    (lambda ([choose : (chooser-of 'a)]) : 'a
      (choose a b)))

(define 
   (firs [pair : (pair-of 'a)]) : 'a
    (pair (lambda ([a : 'a] [b : 'a]) : 'a a)))

(define 
   (res [pair : (pair-of 'a)]) : 'a
    (pair (lambda ([a : 'a] [b : 'a]) : 'a b)))

(define 
   (sub1 [f : number-like-function]) : number-like-function
    (lambda ([h : ('c -> 'c)] [c : 'c]) : 'c
      (res
       (f
        (lambda ([p : (pair-of 'c)]) : (pair-of 'c)
          (con (res p) (h (firs p))))
        (con c c)))))

(define no-op (lambda (a) a))

(define two : number-like-function (lambda ([f : ('z -> 'z)] [z : 'z]) (f (f z))))
(define three : number-like-function (add1 two))

((sub1 three) no-op "a")
(three no-op "a")