Occurrence typing and Recursive Types

[mat...@flow.net]

Hi Ambrose,

I have this example of a recursive type that I believe should pass, but isn't:

(defalias Json (t/Rec [x] (U nil

                             String

                             Number

                             String

                             Boolean

                             (t/Map String x)

                             (t/Seq x))))

;; Try and use the `map?` function to cast to the type we want

(ann get-object [Json -> (t/Option (t/Map String Json))])

(defn get-object [in]

  (when (and in (map? in)) in))

The reasoning is that, by doing the (map?) check, the result can only be (t/Map String Json) or nil. However, this is the failure:

Type Error (rest_api/types.clj:369:28) Type mismatch:

Expected: (t/Option (t/Map String rest-api.types/Json))

Actual: (t/U (IPersistentMap String rest-api.types/Json) (t/I (IPersistentMap t/Any t/Any) (ISeq rest-api.types/Json)) (t/I (IPersistentMap t/Any t/Any) Number))

in: in

Some of the "Actual" types don't even make sense to me. How can a value be an intersection of a Map and a Number?

Thanks!

Matt

[Ambrose Bonnaire-Sergeant]

The reason this happens is the map? predicate casts `in` to

(I (IPersistentMap Any Any) Json)

The intersection is distributed over each element of the Json union:

(U (I (IPersistentMap Any Any) nil)

   (I (IPersistentMap Any Any) String)
   (I (IPersistentMap Any Any) Number)
   (I (IPersistentMap Any Any) Boolean)
   (I (IPersistentMap Any Any) (Map String Json))
   (I (IPersistentMap Any Any) (Seq Json)))

This simplifies to:

(U Nothing
   Nothing
   (I (IPersistentMap Any Any) Number)
   Nothing
   (IPersistentMap String Json)
   (I (IPersistentMap Any Any) (Seq Json)))

Unfortunately there's no way to know that a type cannot extend both IPersistentMap and Number, so we can't simplify to Nothing here.

A workaround might be to also test on (not (number? in)) and (not (seq? in)).

In a different world, this might be appropriate:

(defalias Json (t/Rec [x] (U nil

                             String

                             (I Number (Not (Map Any Any)))

                             String

                             Boolean

                             (t/Map String x)

                             (I (t/Seq x) (Not (Map Any Any)))))

However this probably doesn't work at the moment.

Thanks,

Ambrose

[mat...@flow.net]

Thanks Ambrose, this actually makes sense to me now. I didn't realize that, for example, the intersection of Map and Seq could be a thing. But I guess there's no reason why it couldn't be.

[Ambrose Bonnaire-Sergeant]

There are in fact data structures in the wild that are both a Map and a Seq. But probably not a Map and a Number.