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

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来自哪里，从而找出将这些内容放入的位置。