Написание комбинатора Y в типизированном/ракетке

Question

Предположим, у меня есть нетипизированная реализация комбинатора Y в 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) 

Как перевести это в набранный/ракетку?

N.B. Я думаю, что это не канонический способ написания комбинатора Y, но он должен быть эквивалентным.

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) 

Вы можете также встраивать определения, чтобы избежать необходимости (define Y …) и (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)