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
https://gist.github.com/gcanti/2b455c5008c2e1674ab3e8d5790cdad5

Cheers,
Liron.

Comments

[Iven Marquardt]

It happens that I currently work on the same subject, hence a few remarks:

• 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
• a type constructor is like a value constructor (or function in TS) but exists only on the type level
• a higher-kinded (or higher-order) type is a type constructor that takes another type constructor and the necessary number of types to create a new type
• a higher-kinded type constructor is like a higher-order function but exists only on the type level
• it may have kind (* -> *) -> * -> * for example