Writing the Y combinator in typed/racket

Question

Let's say I have an untyped implementation of the Y combinator in Racket.

pasterack.org version

#lang racket

(define Y
  ((λ (f)
     (f f))
   (λ (z)
     (λ (f)
       (f (λ (x) (((z z) f) x)))))))

(define factorial
  (Y (λ (recursive-factorial)
       (λ (x)
         (if (<= x 0)
             1
             (* x (recursive-factorial (- x 1))))))))

(factorial 5)

How do I translate that into typed/racket?

N.B. I think this is not the cannonical way of writing the Y combinator, but it should be equivalent.

Answer 1

pasterack.org version

#lang typed/racket

(define Y
  (;(ann ;; Not needed
    (λ (f)
      (f f))
   ;(All (A) (→ (Rec r (→ r A)) A))) ;; Not needed
   (ann
    (λ (z)
      (λ (f)
        (f (λ (x) (((z z) f) x)))))
    (Rec r (→ r (All (T R) (→ (→ (→ T R) (→ T R)) (→ T R))))))))

(: factorial (→ Real Real))
(define factorial
  (Y (λ ([recursive-factorial : (→ Real Real)])
       (λ ([x : Real])
         (if (<= x 0)
             1
             (* x (recursive-factorial (- x 1))))))))

(factorial 5)

You can also inline the definitions, to avoid the need for (define Y …) and (define factorial …):

pasterack.org version

#lang typed/racket

((;; Y combinator
  (;(ann ;; Not needed
    (λ (f)
      (f f))
   ;(All (A) (→ (Rec r (→ r A)) A))) ;; Not needed
   (ann
    (λ (z)
      (λ (f)
        (f (λ (x) (((z z) f) x)))))
    (Rec r (→ r (All (T R) (→ (→ (→ T R) (→ T R)) (→ T R)))))))
  ;; Recursive function
  (λ ([recursive-factorial : (→ Real Real)])
    (λ ([x : Real])
      (if (<= x 0)
          1
          (* x (recursive-factorial (- x 1)))))))
 5)