racket - sub1的类型不匹配问题

Question

我不明白为什么 pick1 中的 sub1 函数有类型不匹配问题，但 pick0 没有

(define-predicate one? One)
(: pick1 (-> Positive-Integer (Listof Any) Any))
(define pick1
  (λ(n lat)
    (cond [(one? n) (car lat)]
          [else (pick1 (sub1 n)
                       (cdr lat))])))

我试过这个解决方法，
但我认为这不是解决此问题的正确方法。

(: pick1-workaround (-> Positive-Integer (Listof Any) Any))
(define pick1-workaround 
  (λ(n lat)
    (cond [(one? n) (car lat)]
          [else (pick1-workaround  (cast (sub1 n) Positive-Integer)
                                   (cdr lat))])))

pick0 没有这个问题。

;;(: pick0 (-> Natural (Listof Any) Any))
(define pick0
  (λ(n lat)
    (cond [(zero? n) (car lat)]
          [else (pick0 (sub1 n)
                       (cdr lat))])))

Answer 1

您隐含地希望 Typed Racket 推理的是，如果 x在 Positive-Integer - One ，然后 (sub1 x)在 Positive-Integer .虽然人类很容易看出这是真的，但我认为问题在于 Typed Racket 不知道如何描述 Positive-Integer - One = {2, 3, 4, ...} .

另一方面，您的 pick0作品。此版本pick1也有效:

(: pick1 (-> Positive-Integer (Listof Any) Any))
(define pick1
  (λ (n lat)
    (define n* (sub1 n))
    (cond 
      [(zero? n*) (car lat)]
      [else (pick1 n* (cdr lat))])))

我认为原因是 Typed Racket 知道如果 x在 Positive-Integer ，然后 (sub1 x)在 Natural ，并且它识别出 (sub1 x)在 else 分支中必须在 Natural - {0} = Positive-Integer (通过 occurrence typing )，允许它成功键入检查程序。