## DEV Community

liron_hazan

Posted on • Updated on

# Type thinking P1 - Types

Types addiction.. no "taxes" or bulshit ;)

Prologue: This post is the 1st of a series of short posts on comparing type exists in Haskell to their Typescript & Rust equivalents.
For the past few months I've been on/off learning Rust and Haskell and that's an excuse to practice while wondering some fun theoretical stuff..

What are types?
Type Theory?
What's HKT (Higher kind types) - typing types ?

# Types as explained by the Haskell perspective:

Instead of pasting the wikipedia explanation of a type system, let's review the Haskell like explanation from learnyouhaskell:

" A type is a kind of label that every expression has. It tells us in which category of things that expression fits. The expression True is a boolean, "hello" is a string, etc. "

# Type Theory

My guess is that I'm NOT gonna be an expert in Category, Types or Sets theories, but learning in high level and slowly deeping the knowledge is a good thing… and grasping types is an integral part of our logic.

I recently discovered nLab (kind of a wiki for our topic but not exactly..) for future digging in theories, follows is the nLab definition of type theory:

" Explicitly, type theory is a formal language, essentially a set of rules for rewriting certain strings of symbols, that describes the introduction of types and their terms, and computations with these, in a sensible way."

# HKT - higher kinded types

Let's start demystifying the big words…

• A kind is the type of a type constructor.
• A type constructor is a feature of a typed formal language that builds new types from old ones.

Higher Kinded Types are types who take types and construct a new type of them.
In Haskell the kind of Maybe is * -> *.

We don't have HKT on Typescript (not sure we need another abstraction, TS transpiled to JS anyway and it's not statically typed, it's gradually typed meaning we can still have untyped variable by using "any"..)

My first thought of HKT was: "we have Generics" but that's wrong cause Generics let us describe data types (values) and a Generic cannot use another Generic.

``````interface TypeA<T> {
foo: T
}

// I want to describe a type that is of Type A or null
// type maybe_A = TypeA<*> | null; // I can't

type maybe_any_A = TypeA<any> | null; // I can do that but I guess the point of HKT will be lost

type maybeA = <T>(t: T) => TypeA<T> | null; // now the type of maybe A is a function that maybe returns A
``````

Feel free to feedback if you think I've got that wrong :)

References:

Bartosz Milewski Category Theory series
Dr. Erik Meijer - Functional Programming Fundamentals (C9)
https://ncatlab.org/nlab/show/type+theory

Cheers,
Liron.

• Every type has a kind (denoted as `*`), not only type constructors
• A proper type has kind `*` and a type constructor may have kind `* -> *` for instance
• it may have kind `(* -> *) -> * -> *` for example