Проблема несоответствия типов sub1

Я не могу понять, почему функция sub1 в pick1 имеет проблему с несоответствием типов, а 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))])))

racket typed-racket
person Lyu Yao Ting    schedule 16.11.2019    source источник

Ответы (1)


arrow_upward
5
arrow_downward

Вы неявно хотите, чтобы 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 (через вхождение ввода), что позволяет успешно проверить тип программы.

person Sorawee Porncharoenwase    schedule 16.11.2019