2

I am trying to build lists of structs with apply in Typed Racket but cannot figure out how to make it work. My guess is that it has to do with the problem with polymorphic functions but I can't figure out a workaround.

This works:

(struct tt ([a : Integer]
            [b : Integer]))

(apply tt '(1 2))

But this doesn't (edited):

(struct tt2 ([a : String]
             [b : (Vectorof Any)]))

(apply tt2 (list "A" (vector 1 2 2)))

With the error:

 /usr/share/racket/collects/racket/private/kw.rkt:979:25: Type Checker: Bad
arguments to function in `apply':
Domain: String (Vectorof Any)
Arguments:  (List String (Vector Integer Integer Integer))

  in: (#%app apply tt23 (#%app list (quote "A") (#%app vector (quote 1) (quote 2) (quote 2))))

Is there any solution for this?

  • Double-check which program you're running. `(apply tt2 '(1 (1 2 2)))` works fine for me. It's `(apply tt2 '(1 '(1 2 2)))` that fails because of how `quote` works. I would recommend you avoid using `quote` for lists, and write it as `(apply tt2 (list 1 (list 1 2 2)))` instead. – Alex Knauth Jul 16 '18 at 15:11
  • If this is because you made the common mistake of thinking `'(1 '(1 2 2))` was the same as `(list 1 (list 1 2 2))`, then see [What is the difference between quote and list?](https://stackoverflow.com/questions/34984552/what-is-the-difference-between-quote-and-list). – Alex Knauth Jul 16 '18 at 15:15
  • 1
    I modified the example to make it closer to what I'm actually trying to do, which is working with vectors which can be of different types. I think this should now **not** work? – Matías Guzmán Naranjo Jul 16 '18 at 15:23
  • Okay. Vectors are a mutable data structure, and the possibility of mutation makes typechecking less intuitive. A `(Vectorof Integer)` cannot be used as a `(Vectorof Any)` because a `(Vectorof Any)` might be mutated later to include non-integers. The solution is to annotate each vector to its proper type when you *create* it. That means replacing `(vector ....)` with `(ann (vector ....) (Vectorof Any))`, if you need to use it as a `(Vectorof Any)`. – Alex Knauth Jul 16 '18 at 15:28

1 Answers1

2

Vectors are a mutable data structure, and the possibility of mutating the vector makes typechecking less intuitive.

A (Vectorof Integer) cannot be used as a (Vectorof Any) because a (Vectorof Any) might be mutated later to include non-integers. A program like this doesn't typecheck

#lang typed/racket
(struct tt2 ([a : Integer]
             [b : (Vectorof Any)]))

(: v (Vectorof Integer)
(define v (vector 1 2 2))
(apply tt2 (list 1 v))

because if it did, someone could write (vector-set! (tt2-b ....) 0 "not a number"), and then v would have the wrong type inside it.

The solution is to annotate every vector to its proper type whenever you create one. That means doing one of these things:

  1. Replacing (vector ....) with (ann (vector ....) (Vectorof Any)).
  2. If the vector is created directly as a variable v, replacing (define v (vector ....)) with (define v : (Vectorof Any) (vector ....)).

For example:

#lang typed/racket
(struct tt2 ([a : Integer]
             [b : (Vectorof Any)]))

(apply tt2 (list 1 (ann (vector 1 2 2) (Vectorof Any))))

And keep in mind this is usually necessary for mutable things like vectors, but not for immutable things like lists.

Alex Knauth
  • 8,133
  • 2
  • 16
  • 31