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

如何将这个转换为 Typed/Racket 代码？

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

- Suzanne Soy

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版本

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

- Suzanne Soy