76 lines
2 KiB
Markdown
76 lines
2 KiB
Markdown
# 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):
|
|
|
|
```
|
|
given A, B
|
|
type TupleList := List[(A, B)]
|
|
```
|
|
|
|
Or in general terms:
|
|
|
|
```
|
|
type <type constructor> := <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:
|
|
|
|
```
|
|
given A, B
|
|
type TupleList := 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:
|
|
|
|
```
|
|
given A
|
|
type List is ???
|
|
|
|
given A, B
|
|
fn map_list: (List[A], (A) => B) => List[B]
|
|
|
|
given F[*]
|
|
type class Functor is
|
|
given A, B
|
|
fn map: (F[A])((A) => B) => F<B>
|
|
|
|
instance Functor[List] is
|
|
given A, B
|
|
fn map: (List[A])((A) => B) => [B] :=
|
|
(list)(f) => map_list (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.
|