## 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 filter`ff`

, 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