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

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

Проверка типов: несоответствие типов; ожидается: рыба ; дано: а; в: т


racket typed-racket
person izuo    schedule 12.03.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Это связано с тем, что вы неявно ожидаете, что a будет fish, но средство проверки типов смотрит на тип, который вы ему дали, поэтому оно этого не знает. В 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.

person Alex Knauth    schedule 12.03.2016
comment
Большое спасибо, я понял. - person izuo; 12.03.2016
comment
В SML он может вывести тип val rem_fish = fn : fish * fish pizza -> fish pizza. Могу ли я внести некоторые изменения, чтобы получить его в типизированном рэкете? - person izuo; 12.03.2016
comment
Что ты имеешь в виду? В SML это должно быть fish pizza, поэтому в машинописном рэкете это должно быть (pizza fish). - person Alex Knauth; 12.03.2016
comment
Я имею в виду, может ли типизированная ракетка определить тип без аннотации типа здесь. но я нахожу ответ в Указание типов3.2.1 - person izuo; 13.03.2016