如何解决此柯里化函数中的类型不匹配错误？

Question

我试图定义一个多态类型：

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

(struct Empty ()) (struct (a) Cons ([v : a] [w : (listt a)]))

还有一个柯里化函数：

;; 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 的来源，我能够弄清楚将这些放在哪里。