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.
Top comments (1)
It happens that I currently work on the same subject, hence a few remarks:
*
), not only type constructors*
and a type constructor may have kind* -> *
for instance(* -> *) -> * -> *
for example