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.