Skip to end of metadata
Go to start of metadata

Problem

In Clojure we are free to extend datatypes with any combination of protocols and interfaces. To make our type predicates useful, there are sets of protocols/interfaces that should never be extended simultaneously by the same type.

For example, IMap and IVector should probably never be extended by the same type. To see why core.typed needs to know this information, we define a function that takes an argument that can be an IMap or IVector, then we pick a branch based on whether it implements IVector.

Let's assume core.typed knows about which protocols are "compatible". Occurrence typing updates the type for each branch as follows:

  • then branch: ais restricted by (IVector Any)
    • Restrict (U (IMap Any String) (IVector String)) by (IVector Any)
      • (IVector String) restricted by (IVector Any) = (IVector String)
      • (IMap Any String) restricted by (IVector Any) = Nothing
        • IMap and IVector are not compatible
      • Combine: (IVector String) + Nothing = (IVector String)
    • a :- (IVector String)
  • else branch: a is restricted by not (IVector Any)
    • Intersect: (U (IMap Any String) (IVector String)) and not (IVector Any)
      • (IVector String) intersect not (IVector Any) = Nothing
      • (IMap Any String) intersect not (IVector Any) = (IMap Any String)
      • Combine: Nothing + (IMap Any String) = (IMap Any String)
    • a :- (IMap Any String)
What happens if core.typed does not know about compatible protocols? The case in red then becomes:
  • (IMap Any String) restricted by (IVector Any) = (Extends [(IMap Any String) (IVector Any)])
    • IMap and IVector are compatible

Unfortunately, we now have inferred type (Extends [(IMap Any String) (IVector String)]) on the first branch.

We can fix this locally by using the Extends constructor's :without argument, which specifies protocols which are explicitly not extended.

We regain our accurate type, at the cost of more verbose types. The case becomes:

  • (Extends [(IMap Any String)] :without [(IVector Any)])  restricted by (IVector String) = Nothing
    • (Extends [..] :without [(IVector Any)]) is incompatible with types that are subtype to (IVector Any)

Interestingly, this forces us to be very explicit about which protocols we expect to be implemented at certain points in the code.

However, this rarely reveals anything interesting, and quickly becomes a chore.

How do we express disjoint types to avoid this kind of annotation, while still being careful enough to not lose soundness?

 

Labels: