# Types

- [The Ava Type System](#the-ava-type-system)
- [The Nothing Type](#the-nothing-type)
- [Type Definitions](#type-definitions)
    - [Type Constructors](#type-constructors)
- [Higher Kinded Types](#higher-kinded-types)

## The Ava Type System

Ava is based on a static type system with support for higher-kinded types. Ava
does not support inheritence. Ava _does_ support sum types 
([Enumerations](enumerations.md)) and _does_ support 
[type classes](type-classes.md).

## The Nothing Type

The special type, `Nothing`, cannot be instantiated. It can be used to describe
cases that cannot be expressed. For example, `Either[Nothing, String]` cannot
ever be a `Left`. `Nothing` can be used to satisfy any type requirement. For
example, `Either[Nothing, String]` satisfies `Either[Int32, String]`.

## Type Definitions

Types may directly, at the top level, be defined in terms of some 
[type constructor](#type-constructors):

```
type TupleList[A, B] is List[(A, B)]
```

Or in general terms:

```
type <type constructor> is <type definition>
```

### Type Constructors

Type constructors essentially allow for types to be defined in terms of some set
of type inputs. Consider the prior example:

```
type TupleList[A, B] is List[(A, B)]
```

The `TupleList` type requires two type arguments, `A` and `B`, to be constructed
as a concrete type. For example, `TupleList[String, Int32]` is a concrete type.

## Higher Kinded Types

Type constructors in Ava may be higher order (e.g. not order 1) functions:

```
// Assume this exists
type List[A] is ???
fn map[A, B]: (List[A], (A) => B) => List[B]

type class Functor[F[*]] is
    fn map[A, B]: (F[A])((A) => B) => F[B]

instance Functor[List] is
    fn map[A, B]: (List[A])((A) => B) => List[B] is
        (list)(f) => map(list, f)
```

In this example, `Functor[F[*]]` is a type constructor which accepts a single
type argument. That type argument is a type constructor that accepts a single
concrete (order 0) type argument.