Как я могу решить этот тип несоответствия probem в типизированной ракетке?

Question

Я попытался переписать следующий код 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))) 

напечатал ракетка код здесь:

(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)))])) 

Тип проверки: несоответствие типов ; ожидается: рыба ; данный: a ; in: t

Answer 1

Это потому, что вы неявно ожидаете, что a будет fish, но typechecker смотрит на тип, который вы ему дали, поэтому он этого не знает. В ML, если я правильно понимаю, это означает, что тип rem-fish должен быть fish (pizza fish) -> (pizza fish), а не fish (pizza a) -> (pizza 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, является то, что при использовании eq-fish на t, что t пришел из (pizza a) поэтому он имеет тип a. Но это не работает, потому что eq-fish ожидает fish.