Writing Y combinator in typed / racket
Let's say I have an untyped implementation of the Y combinator in Racket.
#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 this into typed / racket?
NB I think this is not the canonical way to write Y combinator, but it should be equivalent.
+3
source to share
1 answer
#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 definitions to avoid the need for (define Y …)
and (define factorial …)
:
#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)
+2
source to share