-
Notifications
You must be signed in to change notification settings - Fork 75
User Guide
core.typed is an optional type system for Clojure. If you are interested in how core.typed can help you verify your programs as correct, read on.
Many programmers use Clojure as relief from popular typed languages such as Java or C#. Java’s verbosity and redundant type annotations help make the move to Clojure feel liberating and enjoyable: so why go back to types?
core.typed has a different story to tell:
- type checking is optional
- only use the type system where you need it
- local type inference is used to infer local bindings
- locals rarely need type annotations
- it can type check normal Clojure code, driven by top-level annotations
- the Clojure you know and love!
If Java has driven you away from types, core.typed could be pleasant surprise. It might even become one of your go-to tools for code verification in Clojure.
This is a good question, especially in the context of a dynamically-typed (DT) language where we don’t have “types”.
We use the term “type” to mean static type and “tag” for runtime tags. Types only exist at compile time and are used by the static type system to model runtime invariants and properties.
Thinking of compile-time and runtime as distinct phases in terms of types often helps. The type system uses types to reason about the runtime behaviour of code, which can also include tag invariants.
There are no types in Clojure, only tags. We can also say that Clojure has exactly one type: Any (the supertype of all types).
The closest equivalent to types we have
are ad-hoc comments or doc-strings which describe the input/output behaviour
of functions.
For example, the number? predicate returns true if its (runtime) argument
has a tag that is a subtype of java.lang.Number, otherwise false. In core.typed
we use a type to model these invariants.
The tag of number? might be IFn, while its type is [Any -> boolean :filters {:then (is Number 0) :else (! Number 0)}].
In summary:
- types only exist at compile time
- tags only exist at runtime
The appeal of a static type checker begins with earlier and clearer type errors.
For example, you might observe:
- fewer “Boolean is not an ISeq” errors without line numbers in production
- more “Cannot pass Boolean to second argument of map” with line numbers at compile time in development.
Types, when coupled with an appropriate doc-string, are excellent machine checkable documentation. They never go out of date, and are often invaluable as a quick reminder of what a function does.
Types are useful when a program grows, especially when there are multiple contributors. If a contribution passes the type system, we know that it is type correct (type errors are amongst the most common user errors in programming).
Not quite. Types can help verify that a program is basically correct, but not if it does the right thing. Use as many verification techniques as you can: core.typed works great coupled with unit testing or generative testing.
Clojure simply is not built with static typing in mind. It is impractical to expect core.typed alone to prevent as many user errors as say Haskell’s type system: core.typed either needs to choose some subset of Clojure optimised for user error prevention, or attempt to check all Clojure code while making some compromises (it does the latter).
This might seem discouraging, but in practice core.typed will catch many kinds of type errors in your code. The problem is some Clojure idioms are so flexible it is often impossible to distinguish between intended and unintended usage.
A small example: map accepts either nil or a Seqable as a second argument. It is perfectly
valid to provide an argument that is always nil, but it’s probably not what the user intended.
So for best results, couple core.typed with all the usual testing/verification techniques.
There are some details to keep in mind when using core.typed before you jump in to use it.
Read the Quick Guide, and keep a copy handy when you follow along the rest of the tutorial.
core.typed requires a moderate amount of assistance from the user to help infer types.
There are two main things that need annotating:
- All vars must be annotated
- All function parameters must be annotated, or default to
Any.
From the provided annotations, core.typed uses local type inference to infer the types for local bindings, interop calls, and other expressions, mostly without further assistance.
When core.typed finds a var reference, def, binding, or some other var-related construct
that relies on the dereferenced value of a var, it requires an expected type.
clojure.core.typed=> (declare abc)
#'clojure.core.typed/abc
clojure.core.typed=> (cf abc)
Type Error (:) Unannotated var clojure.core.typed.test.core/abc
in: clojure.core.typed.test.core/abc
ExceptionInfo Type Checker: Found 1 error clojure.core/ex-info (core.clj:4327)Use clojure.core.typed/ann to associate a static type with a var.
clojure.core.typed=> (cf (ann abc Number))
[clojure.core.typed/abc java.lang.Number]
clojure.core.typed=> (cf (def abc 1))
(clojure.lang.Var Number)
clojure.core.typed=> (cf abc)
java.lang.Numberann qualifies the var in the current namespace if unqualified.
Sometimes vars from other namespaces need annotation. You can annotate them by providing a qualified symbol
to ann (namespace aliases are not supported).
clojure.core.typed=> (cf clojure.core/*compile-path*)
Type Error (:) Unannotated var clojure.core/*compile-path*
in: clojure.core/*compile-path*
ExceptionInfo Type Checker: Found 1 error clojure.core/ex-info (core.clj:4327)
(contains? (clojure.core/deref *var-annotations*) nsym)>
clojure.core.typed=> (cf (ann clojure.core/*compile-path* String))
[clojure.core/*compile-path* java.lang.String]
clojure.core.typed=> (cf clojure.core/*compile-path*)
java.lang.StringWe can instruct core.typed to ignore certain var definitions by adding :no-check metadata
to ann forms.
(ns typed.nocheck
(:require [clojure.core.typed :refer [ann check-ns]]))
(ann ^:no-check foo (Fn [Number -> Number]))
(defn foo [a]
'a)
(ann bar [Number -> Number])
(defn bar [b]
(+ 2 (foo b)))Notice we use both the shorthand [Number -> Number] and (Fn [Number -> Number]) to specify a function type. They are equivalent. (See Types).
After type checking has been performed, core.typed warns about vars that have been assigned types
but have no corresponding checked def form. The def must at least make a binding,
so it would be a warning if the var was only declared.
(ns clojure.core.typed.test.nocheck
(:require [clojure.core.typed :refer [ann check-ns]]))
(ann ^:no-check foo [Number -> Number])
(defn foo [a]
'a)
(ann bar [Number -> Number])
(defn bar [b]
(+ 2 (foo b)))
;clojure.core.typed.test.nocheck=> (check-ns)
; ...
; WARNING: Var clojure.core.typed.test.var-usage/foo used without checking definition
;=> nilNote that check-ns must be called at the REPL or in a unit test.
There are several ways to annotate a function type.
To annotate just the arguments of a fn, use the clojure.core.typed/fn macro,
which accepts optional annotations for the parameters and return type of the function.
clojure.core.typed=> (cf (fn [a :- Number] (+ a 1)))
[(Fn [java.lang.Number -> java.lang.Number]) {:then tt, :else ff}]All the usual destructuring is supported.
clojure.core.typed=> (cf (fn [{:keys [a b c]} :- '{:a Num, :b Long, :c Double}]
[a b c]))
[['{:a Num, :b Long, :c Double} -> '[Num Long Double]]
{:then tt, :else ff}]Often it is more useful to provide a full function type as a fn’s annotation. This
especially works well with Clojure’s anonymous function syntax.
clojure.core.typed=> (cf (ann-form #(inc %)
[Number -> Number]))
(Fn [java.lang.Number -> java.lang.Number])This way, you can also assign anonymous functions ordered intersection function types.
clojure.core.typed=> (cf (ann-form
(fn [a]
(cond
(number? a) 1
(symbol? a) 'a))
(Fn [Num -> Num]
[Sym -> Sym])))
(Fn [Num -> Num]
[Sym -> Sym])See Types.
core.typed supports polymorphic function types. They allow us to specify function types which are both general and accurate.
The primitive All constructor creates a polymorphic binder and scopes
type variables in a type.
The identity function has a simple polymorphic type:
(All [x]
[x -> x])Read: for all types x, a function that takes an x and returns an x.
Polymorphic types are introduced with annotations, but where are they eliminated? We use local type inference to infer type variable types based on how they are used.
(identity :a)In the above example, we infer x to be Keyword, and instantiate the polymorphic
type as [Kw -> Kw].
Type variables support upper and lower type bounds, which default to Any and Nothing
respectively.
Equivalently, the type:
(All [x] ...)is shorthand for:
(All [[x :> Nothing :< Any]] ...)We use bounds to ensure a type variable can only be instantiated to a particular type.
The type of an identity function that only accepts Numbers can be written:
(All [[x :< Number]]
[x -> x])Bounds do not seem as useful in core.typed as languages like Java or Scala. Often, combinations of ordered function intersections and unions are more useful.
Bounds are also recursive: a bound can refer to the variable it’s bounding. Type variables to the left of the type variable being bounded in the same binder are in scope in a bound.
A type variable can be bounded by a type of a higher-kind, or higher-rank.
(defalias AnyMonad
"A monad with bind, result, and optionally zero and plus."
(TFn [[m :< (TFn [[x :variance :covariant]] Any)]]
'{:m-bind (All [x y]
[(m x) [x -> (m y)] -> (m y)])
:m-result (All [x]
[x -> (m x)])
:m-zero (U (All [x] (m x)) Undefined)
:m-plus (U (All [x]
[(m x) * -> (m x)])
Undefined)}))In this type, x is a type function taking a type and returning a type.
For those familiar with Haskell, x is of kind * -> *.
The type function is also covariant, which further ensures x is instantiated
to a covariant type function.
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 Sym Num nil)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
thenfilter - a filter that is true if the expression is a false value, called the
elsefilter
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}]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)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.
A very common place for a latent filters are in the types for predicates.
The type for symbol?, is
[Any -> Boolean :filters {:then (is Sym 0), :else (! Sym 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 Sym 0) says the first argument to symbol? is of type Sym
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 Sym a), :else (! Sym a)}
empty-object
Flow tt
booleanBy printing the filter set of (symbol? a) we can see this in work, which
has a non-latent filter set of {:then (is Sym a), :else (! Sym a)}.
TODO
Protocol definitions should use clojure.core.typed/defprotocol whose syntax is reminiscent of defprotocol and typed fn:
(defprotocol IUnifyWithLVar
(unify-with-lvar [v u :- LVar s :- ISubstitutions] :- (U ISubstitutions Fail)))Polymorphic protocols are supported:
(defprotocol [a b] Lens
(-fetch [l x :- a] :- b)
(-putback [l x :- a v :- b] :- a))clojure.core.typed/ann-protocol annotates protocols.
Takes a name and a optionally a :methods keyword argument mapping method names to expected types.
(ann-protocol IUnifyWithLVar
unify-with-lvar [Term LVar ISubstitutions -> (U ISubstitutions Fail)])
(defprotocol> IUnifyWithLVar
(unify-with-lvar [v u s]))Each protocol method argument (including the first) is explicit in the type annotation.
Often, the the first argument (aka. this) will just be the protocol, but in some cases
it is convenient to add more general types.
clojure.core.typed/ann-datatype annotates datatypes.
Takes a name and a vector of fieldname/type type entries.
(ann-datatype Pair [lhs :- Term,
rhs :- Term])
(deftype Pair [lhs rhs]
...)Each protocol extended in deftype must have an annotated expected type with ann-protocol.
The types for Java interface method are inferred from their corresponding Java type.
Due to limitations in core.typed’s inference, we require using “typed” versions of several core forms.
Usages of loop should be replaced with clojure.core.typed/loop.
The syntax is identical except each loop variable requires a type annotation.
(loop [a :- Number, 1
b :- (U nil Number), nil]
...)Named fns require full annotation for accurate recursive calls inside the fn body.
clojure.core.typed=> (cf (ann-form (fn a [n] (+ (a 1) n))
[Number -> Number]))
(Fn [java.lang.Number -> java.lang.Number])Use clojure.core.typed/for instead of for.
for uses annotations to check the parameter and return types of
the expression. If omitted, they default to Any.
(for [a :- (U nil Int) [1 nil 2 3]
:when a]
:- Num
(inc a))Use clojure.core.typed/doseq instead of doseq.
doseq uses annotations to infer the parameter types of the expression.
If omitted, they default to Any
(doseq [a :- (U nil Int) [1 nil 2 3],
:when a]
(inc a))