Types of types: Haskell's Kind system

The more of Haskell's ideas that bleed into mainstream languages, the happier the world will become. It is just so beautiful how these higher abstractions can become so useful and powerful for tying all kinds of things together.

I've long suspected that one of the things that makes monads notoriously difficult to explain to people outside of the Haskell ecosystem is that very few other languages even have a kind system that you are allowed to manipulate in code (and in some, like C++, it's so esoteric that you basically never see it). First explaining that you can even abstract over "type->type" kinded things gets you a lot of the way towards monads without actually describing monads.

One thing I've noticed since I've become an engineer who gets to design the architecture:

No matter what I do, eventually algebraic structures like semi-groups and monads along with categorical structure like lenses and traversals keep popping up.

I really like the concept of dependent types, all type systems that I use rust or haskell have a very limited set of dependent types, but I do like the things that it let's you do

> These are the constructs we manipulate in our programs, things like 1, 2, True, "hello", etc… In functional programming contexts, they're also called "terms."

This is not correct. Terms are syntactic expressions in a program. For example, 1+2 is a term, but it’s not a value. At runtime, it evaluates to 3. As such, some terms correspond directly to values - like 1 - but other terms represent computations that will be performed at runtime.

tl;dr: terms are a syntactic concept, values are a runtime concept. Terms evaluate to values.