-
Notifications
You must be signed in to change notification settings - Fork 74
Types
Every type is a subtype to Any, written x <: Any for all types x. Equivalently, any place that Any is valid,
any other type can be used. Any is also known as the "Top" type.
Conversely, there are no types that are subtypes to Nothing, except itself. For all types x
it holds that Nothing <: x. Put another way, Nothing is a valid type to use
in positions expecting any other type. In practice, Nothing is not as useful as Any,
and is usually used internally to detect dead code and other code properties.
It does not make sense to assign a binding the type Nothing.
One common usage is an empty sequence, which is inferred to be of type (Seqable Nothing).
The result type of throw is also Nothing.
core.typed has a special function type, which is an ordered intersection of arities. It allows us to specify fine grained function invariants.
Starting simply,
(Fn [Any -> Any])is a function taking one argument of type Any. [Any -> Any]
is an equivalent shorthand for single-arity function types.
We can specify multiple arities:
(Fn [Any -> Any]
[Any Any -> Any])Here we can call a function of this type with either one or two arguments. In this case, the ordered intersection type acts as a simple overloading on arity.
Finer invariants can be expressed by specifying multiple arities of the same arity:
(Fn [Sym -> Num]
[Num -> Sym])This function returns a Num if passed a Sym, and returns a Sym if passed a Num.
The exact return type for a function application expression involving multiple arities
is chosen by matching the actual types provided with each arities, top-to-bottom
(this explains why our functions are "ordered" intersections).
In this case, each arity is disjoint because no combination of arguments could
potentially trigger both arities. More concretely, there is no type that is both
a Sym and a Num, so at most one arity triggers for any given arguments.
Overlapping arities hints at the power of ordered intersections.
(Fn [Long -> Sym]
[Num -> Kw])This type always returns a Sym for Long arguments.
Beware, swapping the arities produces different results!
(Fn [Num -> Kw]
[Long -> Sym])The first arity always "wins" because Num is strictly more general than Long.
Arities are usually ordered from more-specific parameters to less-specific parameters.
What about arities that have partially overlapping parameters? Consider:
(Fn [Long Any -> Kw]
[Any Num -> Sym])Calling with Long Long arguments gives Kw,
and Num Long gives Sym.
Flipping the arities gives different results:
(Fn [Any Num -> Sym]
[Long Any -> Kw])Now Long Long gives Sym, and Num Long gives Sym.
Partially overlapping arities can be tricky and can unexpectedly trigger earlier arities,
so care must be taken here.
Finally, a common idiom is to provide a base arity, which has arguments at least as general as the ones above it.
For example, we might want our function of type (Fn [Long -> Sym] [Num -> Kw]) to handle the case where
the argument is either a Long or a Num.
We can express this by using a union (to express a least-upper-bound of Long and Num).
(Fn [Long -> Sym]
[Num -> Kw]
[(U Long Num) -> (U Sym Kw)])Note the result type is sufficiently general to show the result type is either a Sym or Kw.
Rest parameters are specified using a *.
eg.
(Fn [Any Num * -> Any])is a function taking at least one parameter, and any number of parameters after it
of type Num.
Keyword parameters are specified using & after the fixed domain.
eg.
(Fn [Any & :optional {:a Num} -> Any])is a function that takes a fixed parameter and an optional keyword argument :a, of
type Num.
We can also specify mandatory keyword parameters:
(Fn [Any & :mandatory {:a Num} -> Any])is the same function, except the keyword argument :a now must be present when calling.
We can express finer grained invariants by combining keyword types and ordered function intersection types:
(Fn [Any & :mandatory {:a Num :b Num} -> Num]
[Any & :optional {:a Num :b Num} -> Any])This function type returns a Num if provided both :a and :b parameters,
otherwise returns Any if some other combination of :a and :b is provided.
core.typed reuses Java and clojure.lang.* classes. The normal scoping rules apply in types,
e.g., use :import to bring classes into scope.
Note: java.lang.* classes are implicitly in scope in Clojure namespaces.
core.typed follows the normal rules that apply to Clojure code.
clojure.core.typed=> (cf 1 Long)
java.lang.Long
clojure.core.typed=> (cf 1.1 Double)
java.lang.Double
clojure.core.typed=> (cf "a" String)
java.lang.String
clojure.core.typed=> (cf \a Character)
java.lang.CharacterSymbols and Keywords are instances of their corresponding clojure.lang classes.
clojure.core.typed=> (cf 'a clojure.lang.Symbol)
clojure.lang.Symbol
clojure.core.typed=> (cf :a clojure.lang.Keyword)
clojure.lang.KeywordThe aliases Sym and Kw are shorthands for these types.
Seqables extend (Seqable a), which is covariant in its argument.
Types that extend (Seqable a) are capable of creating a sequence
(aka. an (ISeq a)) representation of itself via functions like seq.
clojure.core.typed=> (cf {'a 2 'b 3} (Seqable '[Sym Num]))
(Seqable '[Sym Num]))
clojure.core.typed=> (cf [1 2 3] (Seqable Num))
(Seqable Num)
clojure.core.typed=> (cf '#{a b c} (Seqable Sym))
(Seqable Sym)Seqs extend (Seq a), which is covariant in its argument.
clojure.core.typed=> (cf (seq [1 2]))
(Seq Num)Lists extend (List a), which is covariant in its argument.
clojure.core.typed=> (cf '(1 2))
(List Num)Vectors extend (Vec a), which is covariant in its argument.
clojure.core.typed=> (cf [1 2])
(Vec Number)Maps extend (Map a b), which is covariant in both its arguments.
clojure.core.typed=> (cf {'a 1 'b 3})
(Map Sym Long)Sets extend (Set a), which is covariant in its argument.
clojure.core.typed=> (cf #{1 2 3})
(Set Number) An Atom of type (Atom2 w r) can accept values of type w and provide values of type r.
It is contravariant in w and covariant in r.
Usually w and r are identical, so an alias (Atom1 wr) is provided,
which is equivalent to (Atom2 wr wr).
core.typed isn't smart enough to infer mutable types like atoms without annotations.
clojure.core.typed=> (cf (atom {}) (Atom1 (Map Sym Num)))
(Atom1 (Map Sym Num))The helper macro atom> makes this a little nicer.
clojure.core.typed=> (cf (atom> (Map Sym Num) {}))
(Atom1 (Map Sym Num))A rough grammar for core.typed types.
Type := nil | true | false
; Union type
| (U Type*)
; Intersection type
| (I Type+)
| FunctionIntersection
| (Value CONSTANT-VALUE)
| (Rec [Symbol] Type)
| (All [Symbol+] Type)
| (All [Symbol* Symbol ...] Type)
; HMap syntax
| (HMap :mandatory {LiteralKeyword Type*}
:optional {LiteralKeyword Type*}
:absent-keys #{LiteralKeyword*}
:complete? Boolean) ;eg (HMap :mandatory {:a (Value 1), :b nil})
; Mandatory, non-complete HMap syntax
| '{Keyword Type*} ;eg '{:a (Value 1), :b nil}
| (HVec [Type*])
| '[Type*]
| (Seq* Type*)
| (List* Type*)
| Symbol ;class/protocol/free resolvable in context
FunctionIntersection := ArityType
| (Fn ArityType+)
ArityType := [FixedArgs -> Type]
| [FixedArgs RestArgs * -> Type]
| [FixedArgs DottedType ... Symbol -> Type]
FixedArgs := Type*
RestArgs := Type
DottedType := Type
nil, true and false resolve to the respective singleton types for those values
(I Type+) creates an intersection of types.
(U Type*) creates a union of types.
A function type is an ordered intersection of arity types.
There is a vector sugar for functions of one arity.
A heterogeneous map type represents a map with some information about specific keyword keys.
Heterogeneous maps support:
- presence of specific keys
- absence of specific keys
- optional keys
- fully-specified
The main constructor for heterogeneous maps is the HMap constructor.
HMap takes a :mandatory keyword argument specifying the entries that always occur in this type.
clojure.core.typed=> (cf {:a 1} (HMap :mandatory {:a Num}))
;=> (HMap :mandatory {:a Num})
clojure.core.typed=> (cf {} (HMap :mandatory {:a Num}))
;Type Error (clojure.core.typed:1:30) Expected type: (HMap :mandatory {:a Num})
;Actual: (HMap :mandatory {} :complete? true)We can forget extra keys with just :mandatory (because :complete? defaults to false).
clojure.core.typed=> (cf {:a 1 :b 'a} (HMap :mandatory {:a Num}))
;=> (HMap :mandatory {:a Num}):optional keys specify entries that may or may not occur. If the entry does occur, the respective value is of the type specified in the :optional map.
We use :optional often in combination with :mandatory:
clojure.core.typed=> (cf {} (HMap :optional {:a Num}))
;=> (HMap :optional {:a Num})
clojure.core.typed=> (cf {:a 1 :b 'a} (HMap :mandatory {:a Num} :optional {:b Symbol}))
;=> (HMap :mandatory {:a Num} :optional {:b Symbol})
clojure.core.typed=> (cf {:a 1} (HMap :mandatory {:a Num} :optional {:b Symbol}))
;=> (HMap :mandatory {:a Num} :optional {:b Symbol}):absent-keys declares a set of specific keys do not appear. This is useful for more accurate types with lookups on absent keys.
The first input below shows we get type Any if we lookup a key we don't know any information about. The second input shows :absent-keys is used to infer lookups on absent keys as nil.
clojure.core.typed=> (cf (let [m (ann-form {:a 1} (HMap :mandatory {}))]
(:a m)))
;=> Any
clojure.core.typed=> (cf (let [m (ann-form {:a 1} (HMap :absent-keys #{:a}))]
(:a m)))
;=> nilFinally, :complete? says that there are no further entries in this map. It takes a boolean value, defaulted to false.
clojure.core.typed=> (cf (let [m (ann-form {} (HMap :complete? true))]
(:a m)))
;=> nilLiteral maps without keyword keys are inferred as APersistentMap.
clojure.core.typed=> (cf {(inc 1) 1})
[(clojure.lang.APersistentMap clojure.core.typed/AnyInteger (Value 1)) {:then tt, :else ff}]A HSequential is an immutable heterogeneous collection that satisfies (Coll a)
and clojure.lang.Sequential.
(HSequential [Num Sym]) represents a collection of count 2 like [1 'a] or '(1 a).
Rest and dotted rest arguments are supported with similar syntax to Fn.
eg. (HSequential [Num Sym *])
(HSequential [Num b ... b])
(HVec [(Value 1) (Value 2)]) is a Vec of count 2, essentially
representing the value [1 2]. The type '[(Value 1) (Value 2)] is identical.
HVecs are subtypes of HSequentials.
Rest and dotted rest arguments are supported with similar syntax to Fn.
eg. (HVec [Num Sym *])
(HVec [Num b ... b])
The binding form All introduces a number of free variables inside a scope.
Optionally scopes a dotted variable by adding ... after the last symbol in the binder.
eg. The identity function: (All [x] [x -> x])
eg. Introducing dotted variables: `(All [x y ...] [x y ... y -> x])
Rec introduces a recursive type. It takes a vector of one symbol and a type.
The symbol is scoped to represent the entire type in the type argument.
; Type for {:op :if
; :test {:op :var, :var #'A}
; :then {:op :nil}
; :else {:op :false}}
(Rec [x]
(U '{:op (Value :if)
:test x
:then x
:else x}
'{:op (Value :var)
:var clojure.lang.Var}
'{:op (Value :nil)}
'{:op (Value :false)}))))