racket - 如何解决类型 Racket 中的这种类型不匹配问题？

Question

我试图在 typed racket 中重写以下 SML 代码，但出现类型不匹配错误，我对此感到困惑。

datatype 'a pizza = Bottom
                      | Topping of ('a * ('a pizza))

datatype fish = Anchovy
              | Lox
              | Tuna

fun eq_fish (Anchovy,Anchovy)
      = true
      | eq_fish (Lox,Lox)
        = true
      | eq_fish (Tuna,Tuna)
        = true
      | eq_fish (a_fish,another_fish)
    = false

fun rem_fish (x,Bottom)
  = Bottom
  | rem_fish (x,Topping(t,p))
    = if eq_fish(t,x)
      then rem_fish(x,p)
      else Topping(t,(rem_fish(x,p)))

在此输入 Racket 代码:

(define-type (pizza a)
  (U Bottom
     (Topping a)))

(struct Bottom ())
(struct (a) Topping ([v : a] [w : (pizza a)]))

(define-type fish
  (U Anchovy
     Lox
     Tuna))

(struct Anchovy ())
(struct Lox ())
(struct Tuna ())

(: eq-fish (-> fish fish Boolean))
(define (eq-fish f1 f2)
  (match f1
    [(Anchovy)
     (Anchovy? f2)]
    [(Lox)
     (Lox? f2)]
    [(Tuna)
     (Tuna? f2)]
    [_ false]))

(: rem-fish (∀ (a) (fish (pizza a) -> (pizza a))))
(define (rem-fish x pizza)
  (match pizza
    [(Bottom) (Bottom)]
    [(Topping t p)
     (if (eq-fish t x)
         (rem-fish x p)
         (Topping t (rem-fish x p)))]))

类型检查器:类型不匹配;预期:鱼;给出:一个;在:t

Answer 1

这是因为你隐含地期望 a 是一条 fish，但是类型检查器会查看你给它的类型，所以它不知道这一点。在 ML 中，如果我理解正确的话，它推断 rem-fish 的类型应该是 fish (pizza fish) -> (pizza fish)，而不是 鱼(披萨 a)->(披萨 a)。如果您更改函数以使用该类型，则您的代码有效:

(: rem-fish : fish (pizza fish) -> (pizza fish))
(define (rem-fish x pizza)
  (match pizza
    [(Bottom) (Bottom)]
    [(Topping t p)
     (if (eq-fish t x)
         (rem-fish x p)
         (Topping t (rem-fish x p)))]))

它必须是 fish 而不是 a 的原因是，当您在 t< 上使用 eq-fish 时，t 来自 (pizza a)，所以它的类型是 a。但这不起作用，因为 eq-fish 需要一条 fish。