racket - sub1的类型不匹配问题

我不知道为什么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))])))

最佳答案

您隐式地希望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中，并且它认识到else分支中的(sub1 x)必须在Natural - {0} = Positive-Integer中(通过occurrence typing)，从而使其能够成功进行类型检查程序。