# Kind

Everything is typed in Erg. Types themselves are no exception. **kind** represents the "type of type". For example, `Int`

belongs to `Type`

, just as `1`

belongs to `Int`

. `Type`

is the simplest kind, the **atomic kind**. In type-theoretic notation, `Type`

corresponds to `*`

.

In the concept of kind, what is practically important is one or more kinds (multinomial kind). One-term kind, for example `Option`

, belongs to it. A unary kind is represented as `Type -> Type`

^{1}. A **container** such as `Array`

or `Option`

is specifically a polynomial kind that takes a type as an argument.
As the notation `Type -> Type`

indicates, `Option`

is actually a function that receives a type `T`

and returns a type `Option T`

. However, since this function is not a function in the usual sense, it is usually called the unary kind.

Note that `->`

itself, which is an anonymous function operator, can also be seen as a kind when it receives a type and returns a type.

Also note that a kind that is not an atomic kind is not a type. Just as `-1`

is a number but `-`

is not, `Option Int`

is a type but `Option`

is not. `Option`

etc. are sometimes called type constructors.

```
assert not Option in Type
assert Option in Type -> Type
```

So code like the following will result in an error:
In Erg, methods can only be defined in atomic kinds, and the name `self`

cannot be used anywhere other than the first argument of a method.

```
# K is an unary kind
K: Type -> Type
K T = Class ...
K.
foo x = ... # OK, this is like a so-called static method
bar self, x = ... # TypeError: cannot define a method to a non-type object
K(T).
baz self, x = ... # OK
```

Examples of binary or higher kinds are `{T: U}`

(: `(Type, Type) -> Type`

), `(T, U, V)`

(: `(Type, Type, Type) - > Type`

), ... and so on.

There is also a zero-term kind `() -> Type`

. This is sometimes equated with an atomic kind in type theory, but is distinguished in Erg. An example is `Class`

.

```
Nil = Class()
```

## Containment of kind

There is also a partial type relation, or rather a partial kind relation, between multinomial kinds.

```
K T = ...
L = Inherit K
L<: K
```

That is, for any `T`

, if `L T <: K T`

, then `L <: K`

, and vice versa.

```
∀T. L T <: K T <=> L <: K
```

## higher kind

There is also a higher-order kind. This is a kind of the same concept as a higher-order function, a kind that receives a kind itself. `(Type -> Type) -> Type`

is a higher kind. Let's define an object that belongs to a higher kind.

```
IntContainerOf K: Type -> Type = K Int
assert IntContainerOf Option == Option Int
assert IntContainerOf Result == Result Int
assert IntContainerOf in (Type -> Type) -> Type
```

The bound variables of a polynomial kind are usually denoted as K, L, ..., where K is K for Kind.

## set kind

In type theory, there is the concept of a record. This is almost the same as the Erg record ^{2}.

```
# This is a record, and it corresponds to what is called a record in type theory
{x = 1; y = 2}
```

When all record values were types, it was a kind of type called a record type.

```
assert {x = 1; y = 2} in {x = Int; y = Int}
```

A record type types a record. A good guesser might have thought that there should be a "record kind" to type the record type. Actually it exists.

```
log Typeof {x = Int; y = Int} # {{x = Int; y = Int}}
```

A type like `{{x = Int; y = Int}}`

is a record kind. This is not a special notation. It is simply an enumeration type that has only `{x = Int; y = Int}`

as an element.

```
Point = {x = Int; y = Int}
Pointy = {Point}
```

An important property of record kind is that if `T: |T|`

and `U <: T`

then `U: |T|`

.
This is also evident from the fact that enums are actually syntactic sugar for refinement types.

```
# {c} == {X: T | X == c} for normal objects, but
# Equality may not be defined for types, so |T| == {X | X <: T}
{Point} == {P | P <: Point}
```

`U <: T`

in type constraints is actually syntactic sugar for `U: |T|`

.
A kind that is a set of such types is commonly called a set kind. Setkind also appears in the Iterator pattern.

```
Iterable T = Trait {
.Iterator = {Iterator}
.iter = (self: Self) -> Self.Iterator T
}
```

## Type inference for polynomial kinds

```
Container K: Type -> Type, T: Type = Patch K(T, T)
Container (K).
f self = ...
Option T: Type = Patch T or NoneType
Option(T).
f self = ...
Fn T: Type = Patch T -> T
Fn(T).
f self = ...
Fn2 T, U: Type = Patch T -> U
Fn2(T, U).
f self = ...
(Int -> Int).f() # which one is selected?
```

In the example above, which patch would the method `f`

choose?
Naively, `Fn T`

seems to be chosen, but `Fn2 T, U`

is also possible, `Option T`

includes `T`

as it is, so any type is applicable, `Container K , T`

also matches ` `->`(Int, Int)`

, i.e. `Container(`->`, Int)`

as ```Int -> Int`. So all four patches above are possible options.

In this case, patches are selected according to the following priority criteria.

- Any
`K(T)`

(e.g.`T or NoneType`

) preferentially matches`Type -> Type`

over`Type`

. - Any
`K(T, U)`

(e.g.`T -> U`

) matches`(Type, Type) -> Type`

preferentially over`Type`

. *Similar criteria apply for kind of 3 or more. - The one that requires fewer type variables to replace is chosen. For example,
`Int -> Int`

is`T -> T`

rather than`K(T, T)`

(replacement type variables: K, T) or`T -> U`

(replacement type variables: T, U). `(replacement type variable: T) is matched preferentially. - If the number of replacements is also the same, an error is given as being unselectable.

^{1} In type theory notation, `*=>*`

↩

^{2} There are subtle differences such as visibility. ↩