时间戳

首页 > 解决方案 > 你应该如何在 Typed Racket 的 letrec 中键入注解相互递归函数？

typed-racket - 你应该如何在 Typed Racket 的 letrec 中键入注解相互递归函数？

问题描述

如果我理解正确，这是注释letrecTyped Racket 中定义的函数的正确方法：

#lang typed/racket

(letrec ((is-even? (lambda ((n : Nonnegative-Integer))
                     : Boolean
                     (or (zero? n)
                         (is-odd? (sub1 n)))))
         (is-odd? (lambda ((n : Nonnegative-Integer))
                    : Boolean
                    (and (not (zero? n))
                         (is-even? (sub1 n))))))
  (is-odd? 11))

但是，这给出了错误消息：

Type Checker: insufficient type information to typecheck. please add more
              type annotations in: is-odd?

一种解决方法是：

(local ((: is-even? : Nonnegative-Integer -> Boolean)
        (define (is-even? n)
          (or (zero? n)
              (is-odd? (sub1 n))))
        (: is-odd? : Nonnegative-Integer -> Boolean)
        (define (is-odd? n)
          (and (not (zero? n))
               (is-even? (sub1 n)))))
  (is-odd? 11))

遗留符号的形式也可以使用，例如这个问题，但我希望也能够letrec使用当前符号进行注释。

标签： typed-racket

解决方案

您可以在 中的函数名称之后放置类型注释letrec，如下所示：

(letrec ([f1 : type1 expr1]
         [f2 : type2 expr2])
  body)

对于您的示例，这看起来像：

(letrec ([is-even? : (-> Nonnegative-Integer Boolean)
                   (lambda (n)
                     (or (zero? n)
                         (is-odd? (sub1 n))))]
         [is-odd? : (-> Nonnegative-Integer Boolean)
                  (lambda (n)
                    (and (not (zero? n))
                         (is-even? (sub1 n))))])
  (is-odd? 11))

为什么这行得通，但将类型注释放在里面lambda却行不通？

这是因为确保每个类型检查都lambda依赖于 和 的is-odd?类型is-even?。但是，如果您不直接注释函数名称，它只能尝试通过对 lambda 进行类型检查来推断这些类型。

直接注释函数名意味着它甚至不必查看 lambdas 就知道什么类型is-even?和is-odd?必须有什么类型。

推荐阅读