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.

Answer 2

I assume it was created at some point after this question was asked, but there's a tjson package for Typed Racket JSON manipulation. It uses a recursive Json type defined as

(Rec (U String Boolean JsNull Number (Listof Json)
        (HashTable Symbol Json)))

that's mostly compatible with values that pass the json module's jsexpr?. The exceptions are in what it accepts as a valid JSON number, and that it looks like null is hard coded as the symbol 'JsNull instead of being controlled by a parameter, but it's easy to parameterize json code to use the same one.