Can't wrap my head around how to use Polymorphic functions in Typed Racket

I'm trying to extract the data from a xml file produced by the Tiled2D map editor. I originally had an untyped function that loaded all of this data into a Hash, but I switched to a struct because I'm not going to be adding additional data to the object once it's loaded, and the Hash was causing me issues due to mixed types of the values (and the polymorphic issues). After some help in the Racket Discord from @samth (who along with others have been wonderfully helpful with all my TR questions so far) I thought I was starting to get it, but once I started testing the function out on a real file everything fell apart.

Once I load the data into the objs var, it becomes unusable with polymorphic functions because I'm dumb and can't understand how to use them even after reading through the TR guide. So I get this error below. I thought maybe if I annotated the objs var it would work, but it's challenging to get the typing right due to it being a nested list of lists of lists. I should probably back pedal to trying to use polymorphic functions in a simpler situation, but I don't even know where to begin. Anyways I've listed the error, function, and xml below. If someone could give me some pointers that would be helpful. Even if it's just some more basic examples of using TR with polymorphism that would be great.

; c:\home\racket\tmx\tmx.rkt:37:18: Type Checker: Polymorphic function `map' could not be applied to arguments:
; Domains: (-> a b ... b c) (Listof a) (Listof b) ... b
;          (-> a c) (Pairof a (Listof a)) 
; Arguments: (All (a b c) (case-> (-> (List* a b c) b) (-> (Pairof a (Listof b)) b) (-> (Listof a) a))) (Listof (Listof Any))
; 
;   in: (map cadr objs)
; Context (plain; to see better errortrace context, re-run with C-u prefix):
;   c:\Program Files\Racket\share\pkgs\typed-racket-lib\typed-racket\typecheck\tc-toplevel.rkt:414:0 type-check
;   c:\Program Files\Racket\share\pkgs\typed-racket-lib\typed-racket\typecheck\tc-toplevel.rkt:653:0 tc-module
;   c:\Program Files\Racket\share\pkgs\typed-racket-lib\typed-racket\tc-setup.rkt:101:12
;   c:\Program Files\Racket\share\pkgs\typed-racket-lib\typed-racket\typed-racket.rkt:22:4
;   c:\home\.emacs.d\offline-packages\racket-mode-master\racket\syntax.rkt:66:0
> 

typed-xml.rkt is just a copy and paste of what's in the typed version of the xml lib and typed-xml-path.rkt is what is in the path file since they didn't make it into 8.4

#lang typed/racket/base
(require "typed-xml.rkt"
         "typed-xml-path.rkt")

(: load-tmx (-> Path-String  Tiled))
(define (load-tmx pth)
  ;; extract all the useful variables out of the tiled xml file and return an struct

  ;; Tiled xml contents
  (define content (xml->xexpr (document-element
                               (read-xml (open-input-file pth)))))

  ;; (: objs (List (Listof (List Symbol (Listof (List Symbol String))))))
  ;; list of collision squares from the objectgroup section of the xml
  (define objs (filter list? (se-path*/list '(objectgroup) content)))
  (define col-lst (map cadr objs))

  (define map-data (Tiled (assert (string->number (cast (se-path* '(map #:width) content) String)) exact-integer?)
                          (assert (string->number (cast (se-path* '(map #:height) content) String)) exact-integer?)                          
                          (assert (string->number (cast (se-path* '(map #:tilewidth) content) String)) exact-integer?)
                          (assert (string->number (cast (se-path* '(map #:tileheight) content) String)) exact-integer?)
                          (assert (string->number (cast (se-path* '(tileset #:firstgid) content) String)) exact-integer?)
                          (assert (cast (se-path* '(tileset #:source) content) String) string?)
                          (assert (cast (se-path* '(data #:encoding) content) String) string?)))
  map-data)

xml file

<?xml version="1.0" encoding="UTF-8"?>
<map version="1.8" tiledversion="1.8.1" orientation="orthogonal" renderorder="right-down" width="10" height="10" tilewidth="16" tileheight="16" infinite="0" nextlayerid="4" nextobjectid="24">
 <tileset firstgid="1" source="Overworld.tsx"/>
 <layer id="1" name="background" width="10" height="10" locked="1">
  <data encoding="csv">
1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1
</data>
 </layer>
 <layer id="2" name="midground" width="10" height="10" locked="1">
  <data encoding="csv">
0,0,0,0,0,0,0,0,0,0,
0,0,0,0,0,45,46,0,0,0,
0,0,0,0,0,85,86,0,0,0,
0,0,0,0,0,0,0,891,0,0,
0,0,204,205,206,0,0,931,0,0,
0,0,0,0,0,0,0,0,0,0,
0,0,0,0,0,0,0,236,237,0,
0,0,0,0,0,0,0,276,277,0,
0,0,0,0,204,205,206,0,0,0,
0,0,0,0,0,0,0,0,0,0
</data>
 </layer>
 <objectgroup id="3" name="Collisions">
  <object id="6" x="32.1424" y="64.1233" width="47.1638" height="15.5059"/>
  <object id="8" x="63.4773" y="128.408" width="48.779" height="15.6674"/>
  <object id="15" x="112.095" y="55.7243" width="15.5059" height="24.0664"/>
  <object id="22" x="85.5879" y="33.2204" width="22.4979" height="12.3499"/>
  <object id="23" x="86.641" y="26.5189" width="15.8922" height="6.1271"/>
 </objectgroup>
</map>

Hi @Decabytes,

When you pass polymorphic functions (cadr) to higher-order functions (map), you need to help Typed Racket figure out the types: 8 Caveats and Limitations .

More concretely:

(: objs (List (Listof (List Symbol (Listof (List Symbol String))))))
(define objs '(((a ((a "a"))) (b ((b "b"))))))
(map (inst cadr (List Symbol (Listof (List Symbol String)))) objs)

It should be easier to see where the type in inst comes from with type synonyms:

(define-type Elem (List Symbol (Listof (List Symbol String))))
(: objs (List (Listof Elem)))
(define objs '(((a ((a "a"))) (b ((b "b"))))))
(map (inst cadr Elem) objs)

Here's how I reasoned. First, find out the type of cadr in a Typed Racket prompt (you get it when evaluating a module with #lang typed/racket):

- : (All (a b c)
      (case->
       (-> (List* a b c) b)
       (-> (Pairof a (Listof b)) b)
       (-> (Listof a) a)))
#<procedure:cadr>

Never mind the first two clauses in case-> and just focus on (-> (Listof a) a). The error you are getting comes from the fact that Typed Racket has trouble inferring a. The role of inst is to tell Typed Racket what a is.

What is a? It's the type of an element on the list cadr is applied to. This is the part of your big type I factored out with the type synonym Elem. Therefore, when I tell Typed Racket that a is Elem by writing (inst cadr Elem), the code type checks successfully.

2 Likes

Thanks for the insight. The tip about refactoring helped but I'm still stuck at the inst part. I've created a smaller example which shows what objs should resolve to. Obj is a (Listof (List Symbol (Listof (List Symbol String))))

Example

#lang typed/racket

(define-type Collision-List (Listof (List Symbol (Listof (List Symbol String)))))

(: objs Collision-List)
(define objs '((object ((height "15.5059") (id "6") (width "47.1638") (x "32.1424") (y "64.1233"))) (object ((height "15.6674") (id "8") (width "48.779") (x "63.4773") (y "128.408"))) (object ((height "24.0664") (id "15") (width "15.5059") (x "112.095") (y "55.7243"))) (object ((height "12.3499") (id "22") (width "22.4979") (x "85.5879") (y "33.2204"))) (object ((height "6.1271") (id "23") (width "15.8922") (x "86.641") (y "26.5189")))))

(map (inst cadr (List Symbol (Listof (List Symbol String)))) objs)

I thought map would pass cadr (List Symbol (Listof (List Symbol String))) but when I type inst with that I get this error.

 Type Checker: Polymorphic function `map' could not be applied to arguments:
Types: (-> a b ... b c) (Listof a) (Listof b) ... b -> (Listof c)
       (-> a c) (Pairof a (Listof a))  -> (Pairof c (Listof c))
Arguments: (case-> (-> (List* (List Symbol (Listof (List Symbol String))) Any Any) Any) (-> (Pairof (List Symbol (Listof (List Symbol String))) (Listof Any)) Any) (-> Collision-List (List Symbol (Listof (List Symbol String))))) Collision-List
Expected result: AnyValues
 in: (map (inst cadr (List Symbol (Listof (List Symbol String)))) objs)

So Unfortunately it still isn't right. Ideally I'd like to this output and end up with this output

'(((height "15.5059") (id "6") (width "47.1638") (x "32.1424") (y "64.1233"))
  ((height "15.6674") (id "8") (width "48.779") (x "63.4773") (y "128.408"))
  ((height "24.0664") (id "15") (width "15.5059") (x "112.095") (y "55.7243"))
  ((height "12.3499") (id "22") (width "22.4979") (x "85.5879") (y "33.2204"))
  ((height "6.1271") (id "23") (width "15.8922") (x "86.641") (y "26.5189")))

which is (List (Listof (List Symbol String)))

This is exactly what map applies cadr to, but you should tell inst what the type of the element of the list is, not what the type of the list is. In your case, the elements of the list are either Symbol or (Listof (List Symbol String)), so:

(map (inst cadr (U Symbol (Listof (List Symbol String)))) objs)

Unfortunately, the typing gets a little complicated, so Typed Racket tells you that the result of this is (Listof Any). Fortunately, it's easy to cast the result to the type you want:

> (cast result (Listof (Listof (List Symbol String))))
- : (Listof (Listof (List Symbol String)))
'(((height "15.5059") (id "6") (width "47.1638") (x "32.1424") (y "64.1233"))
  ((height "15.6674") (id "8") (width "48.779") (x "63.4773") (y "128.408"))
  ((height "24.0664") (id "15") (width "15.5059") (x "112.095") (y "55.7243"))
  ((height "12.3499") (id "22") (width "22.4979") (x "85.5879") (y "33.2204"))
  ((height "6.1271") (id "23") (width "15.8922") (x "86.641") (y "26.5189")))

Mind the Listof at the top of the resulting type, instead of List.

1 Like

Thanks @scolobb that was a tough one. This is my final solution. The type checker has been satisfied.

#lang typed/racket

(define-type Collision-List (Listof (List Symbol (Listof (List Symbol String)))))

(define-type Collision-Coordinates (Listof (Listof (List Symbol String))))

(: objs Collision-List)
(define objs '((object ((height "15.5059") (id "6") (width "47.1638") (x "32.1424") (y "64.1233"))) (object ((height "15.6674") (id "8") (width "48.779") (x "63.4773") (y "128.408"))) (object ((height "24.0664") (id "15") (width "15.5059") (x "112.095") (y "55.7243"))) (object ((height "12.3499") (id "22") (width "22.4979") (x "85.5879") (y "33.2204"))) (object ((height "6.1271") (id "23") (width "15.8922") (x "86.641") (y "26.5189")))))

;; Have to cast because the result of the map is a (Listof Any) and we want a (Listof (List Symbol String))
(define collisions (cast (map (inst cadr (U Symbol (Listof (List Symbol String)))) objs) Collision-Coordinates))
1 Like

This code is not correct, since collisions ends up with the wrong value. I think you want to map (lambda (x) (car (cadr x))) over the list.

Also, you are ending up with Any because you want to supply an additional type argument to cadr.

(: collisions (Listof (List Symbol String)))
(define collisions (map (λ ([x : (List Symbol (Listof (List Symbol String)))]) (car (cadr x))) objs))
1 Like

I just tested out the above code. collisions1 is the original way, and collisions2 is your way

 collisions1
- : Collision-Coordinates
'(((height "15.5059") (id "6") (width "47.1638") (x "32.1424") (y "64.1233"))
  ((height "15.6674") (id "8") (width "48.779") (x "63.4773") (y "128.408"))
  ((height "24.0664") (id "15") (width "15.5059") (x "112.095") (y "55.7243"))
  ((height "12.3499") (id "22") (width "22.4979") (x "85.5879") (y "33.2204"))
  ((height "6.1271") (id "23") (width "15.8922") (x "86.641") (y "26.5189")))

> collisions2
- : (Listof (List Symbol String))
'((height "15.5059") (height "15.6674") (height "24.0664") (height "12.3499") (height "6.1271"))

Collisions1 is what I want. I do want to store all the coordinates in a list of lists. Collisions2 only collects the heights from each list. I intend to modify the whole collisions definition to produce a list of structs later to reduce the amount of nestedness but this is fine for now. I do like the method of wrapping the cadr in a lambda and just typing the value of x though. I do this in collisions3 and I think it's a little more bit easier to understand IMO. So I think a combination of the above two solutions works the best in my case for me.

#lang typed/racket

(define-type Collision-List (Listof (List Symbol (Listof (List Symbol String)))))

(define-type Collision-Coordinates (Listof (Listof (List Symbol String))))

(: objs Collision-List)
(define objs '((object ((height "15.5059") (id "6") (width "47.1638") (x "32.1424") (y "64.1233"))) (object ((height "15.6674") (id "8") (width "48.779") (x "63.4773") (y "128.408"))) (object ((height "24.0664") (id "15") (width "15.5059") (x "112.095") (y "55.7243"))) (object ((height "12.3499") (id "22") (width "22.4979") (x "85.5879") (y "33.2204"))) (object ((height "6.1271") (id "23") (width "15.8922") (x "86.641") (y "26.5189")))))

;; Have to cast because the result of the map is a Listof Any and we want a (Listof (List Symbol String))
(define collisions1 (cast (map (inst cadr (U Symbol (Listof (List Symbol String)))) objs) Collision-Coordinates))

(: collisions2 (Listof (List Symbol String)))
(define collisions2 (map (λ ([x : (List Symbol (Listof (List Symbol String)))]) (car (cadr x))) objs))

(: collisions3  (Listof (Listof (List Symbol String))))
(define collisions3 (map (λ ([x : (List Symbol (Listof (List Symbol String)))]) (cadr x)) objs))

In that case, the inst expression you want is (inst cadr Symbol (Listof (List Symbol String))).

1 Like