racket - 如何解决柯里化(Currying)函数中的类型不匹配错误？

Question

我尝试定义一个多态类型:

(define-type (listt a)
  (U Empty
     (Cons a)))

(结构空())
(struct (a) Cons ([v : a] [w : (listt a)]))

和柯里化(Currying)函数:

;; a better name for subst-c is subst-currying
(: subst-c : (∀ (a) ((-> a Boolean) -> a (listt a) -> (listt a))))
(define (subst-c pred)
  (lambda (n listt)
    (match listt
      [(Empty)
       (Empty)]
      [(Cons e t)
       (if (pred e)
           (Cons n ((subst-c pred) n t))
           (Cons e ((subst-c pred) n t)))])))

但出现错误

;Type Checker: type mismatch
;   expected: Nothing
;   given: a
;   in: n
;Type Checker: type mismatch
;   expected: (U Empty (Cons Nothing))
;   given: (U Empty (Cons a))
;   in: t

我很困惑，我做错了什么？

Answer 1

如果您手动添加一些类型变量实例化，此代码实际上会进行类型检查。像这样:

(: subst-c : (∀ (a) ((-> a Boolean) -> a (listt a) -> (listt a))))
(define (subst-c pred)
  (lambda (n listt)
    (match listt
      [(Empty)
       (Empty)]
      [(Cons e t)
       (if (pred e)
           (Cons n (((inst subst-c a) pred) n t))      ;; <-- Right here
           (Cons e (((inst subst-c a) pred) n t)))]))) ;; <-- and here

inst 运算符用于实例化类型变量。在本例中，用于递归使用subst-c。我不确定为什么需要在这里手动实例化。我认为这可能是 Typed Racket 类型推断的错误/限制。

通过查看 DrRacket 中弹出的类型工具提示(将鼠标悬停在表达式上以查看类型)并查看 Nothing 的位置，我能够弄清楚将它们放在哪里来自。