ava/notes/types.md

Types

• The Ava Type System
• The Nothing Type
• Type Definitions
  • Type Constructors
• 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) and does support type classes.

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:

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.