How can I solve this type mismatch issue in typed racket?

Question

I tried to rewrite the following SML code in typed racket, but got type mismatch error， I'm confused about it.

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

typed racket code here:

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

Type Checker: type mismatch ; expected: fish ; given: a ; in: t

Alex Knauth Alex Knauth · Accepted Answer · 2016-03-12T14:12:08

This is because you're implicitly expecting a to be a fish, but the typechecker looks at the type you gave it, so it doesn't know that. In an ML, if I understand correctly, it infers that the type of rem-fish should be fish (pizza fish) -> (pizza fish), not fish (pizza a) -> (pizza a). If you change your function to use that type, your code works:

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

The reason it has to be a fish and not a, is that when you use eq-fish on t, that t came from (pizza a) so it has type a. But that doesn't work because eq-fish expects a fish.

How can I solve this type mismatch issue in typed racket?

1 Answers