core.typed - Filters
core.typed includes an implementation of occurrence typing, which helps the type checker refine types according to control flow.
Occurrence typing helps core.typed infer a very accurate type for this expression
by recognising the semantics of predicates like symbol?
and number?
.
clojure.core.typed=> (cf (let [a (ann-form 1 Any)]
(cond
(symbol? a) a
(number? a) a)))
(U clojure.lang.Symbol java.lang.Number nil)
Filters
core.typed collects more information than just types for each expression.
A structure called a filter set is also inferred. A filter set is a collection of two filters:
- a filter that is true if the expression is a true value, called the
then
filter - a filter that is true if the expression is a false value, called the
else
filter
Trivial Filters
There are two trivial filters:
tt
, the trivially true filterff
, the impossible filter
We can use cf
to check the filters of expressions.
clojure.core.typed=> (cf 1)
[(Value 1) {:then tt, :else ff}]
The second place of the result vector is the filter set inferred for the expression.
{:then tt, :else ff}
reads: the expression could be a true value, but it is impossible
for it to be a false value. This of course aligns with the semantics of numbers in Clojure.
False values are never true:
clojure.core.typed=> (cf nil)
[nil {:then ff, :else tt}]
Positive and Negative Type Filters
Filters can hold information relating bindings to types.
A positive type filter refines a local binding to be a type.
This filter says that the local binding a
is of type Number
.
(is Number a)
A negative type filter refines a local binding to not be a type.
This filter says that the local binding a
is not of type Number
.
(! Number a)
Latent Filters
Filters almost never need to be written directly in normal code. Latent filters however are very useful, and provide the most useful information to core.typed.
A latent filter set is a filter set attached to a function type. It is latent because it is not used directly: instead when a function with a latent filter set is called, the filter set is instantiated in a way that makes sense in the current context before it is used like a normal filter.
Predicates
A very common place for a latent filters are in the types for predicates.
The type for symbol?
, is
[Any -> Boolean :filters {:then (is Symbol 0), :else (! Symbol 0)}]
First, notice that latent type predicates can also take an integer as an identifier.
The 0
represents the first argument of the function the latent filter set is attached to.
So the latent then
filter (is Symbol 0)
says the first argument to symbol?
is of type Symbol
if the whole expression is a true value. To retrieve a non-latent filter, the 0
is instantiated to
the appropriate local binding.
Note: Use `clojure.core.typed/print-filterset` to print the filter set of an expression.
clojure.core.typed=> (cf (let [a (ann-form 1 Any)]
(print-filterset "symbol filters"
(symbol? a))))
"symbol filters"
{:then (is clojure.lang.Symbol a), :else (! clojure.lang.Symbol a)}
empty-object
Flow tt
boolean
By printing the filter set of (symbol? a)
we can see this in work, which
has a non-latent filter set of {:then (is clojure.lang.Symbol a), :else (! clojure.lang.Symbol a)}
.
Paths and Objects
TODO