racket - 在 typed/racket 中编写 Y 组合子

Question

假设我在 Racket 中有一个 Y 组合子的无类型实现。

pasterack.org 版本

#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)

我如何将其翻译成打字/球拍？

注意我认为这不是编写 Y 组合子的规范方式，但它应该是等价的。

Answer 1

pasterack.org 版本

#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 …)and (define factorial …)：

pasterack.org 版本

#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)