CODEWITHSUNDEEP
rackettyped-racket
izuo
izuo

Reputation: 65

How to solve the type mismatch error in this currying function?

I tried to define a polymorphic type: 

(define-type (listt a)
  (U Empty
     (Cons a)))

(struct Empty ()) (struct (a) Cons ([v : a] [w : (listt a)]))

and a currying function:

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

but got error

;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

I'm confused about it， what did I do wrong?

Upvotes: 3

Views: 839

Answers (1)

Asumu Takikawa
Asumu Takikawa

Reputation: 8523

If you add a few type variable instantiations manually, this code actually type-checks. Like this:

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

The inst operator is for instantiating a type variable. In this case, for the recursive use of subst-c. I'm not sure why this needs to be manually instantiated here. I think it might be a bug/limitation with Typed Racket's type inference.

I was able to figure out where to put these in by looking at the type tooltips that pop up in DrRacket (hover your mouse over an expression to see the type) and seeing where the Nothing came from.

Upvotes: 4

Related Questions