How can I use JSON's `jsexpr?` predicate with Typed Racket?

Question

I'm trying to use the json package in Typed Racket, but I'm having some trouble handling how to type the jsexpr? predicate. My first attempt was simply using #:opaque.

(require/typed json
               [#:opaque JSExpr jsexpr?])

The trouble is that a jsexpr is not a struct, jsexpr? is simply a predicate that tests whether or not a given value fits a certain structure. In truth, a JSExpr type should look something like this.

(define-type JSExpr (U
                     'null Boolean String Integer Inexact-Real
                     (Listof JSExpr) (HashTable Symbol JSExpr)))

So then, I would just use that JSExpr type, but there's still a problem. Now I have a (U JSExpr EOF) type, and I need to convert it to a JSExpr type (I want to throw an exception if I get EOF). Therefore, I want to do something like this:

(cond
 [(jsexpr? json-data) json-data]
 [else (error "failed to parse JSON data")])

This should work with Racket's occurrence typing, but now I don't have jsexpr? defined! Fortunately, there exists define-predicate to generate that function for me. Unfortunately, it doesn't work with the JSExpr type because a predicate needs a flat contract, and potentially-mutable data structures such as HashTable require chaperone contracts.

Alright, well what about typing the actual jsexpr? predicate to occurrence-type for JSExpr?

(require/typed json
               [jsexpr? (-> Any Boolean : JSExpr)])

Unfortunately, this doesn't work, either, because filters can't be used in require/typed.

I understand that the real problem is most likely stemming from the fact that HashTable is mutable, but that's not something I can change. I suppose I could write my own (-> Any Boolean : JSExpr) function, but that would sort of defeat the purpose of using the library.

Is there any way at all to make this work? A simple ImmutableHashTable type would likely suffice here, but that doesn't seem to exist.

Answer 1

From the mailing list:

The problem is that typed racket doesn’t know that a value of type String for instance will be of type JSExpr or not, so you would have to put (assert x jsexpr?) around everything that you want to treat as a jsexpr.