core.typed - Polymorphic Functions
core.typed supports polymorphic function types. They allow us to specify function types which are both general and accurate.
All
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 [Keyword -> Keyword]
.
Bounds
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 Number
s 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.
Higher-kinded variables
Note: Experimental feature
A type variable can be of a higher-kind.
(def-alias AnyMonad
(TFn [[m :kind (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.