Types of types: Haskell's Kind system
thunk.blog
thunk.blog
EDIT: also the links to GitHub on https://lsalpha.com/systems are 404ing for me, so I exited your site without an example of what a real implementation might look like.
It has a lot of excellent ideas and devilishly clever abstractions, but in Haskell they tend to remain incomplete and awkward to use. They tend to only mature by translation to other languages.
For some simple examples see https://github.com/stefan-hoeck/idris2-tutorial
Oops, your advice came ten years and millions of dollars of value generated too late for me :(
All jokes aside, it isn't impossible to use Haskell for a commercial project, but in my opinion you are making things needlessly difficult for yourself - especially in the pre-AI era. There's only a certain hours in a week, so do you want to spend those writing business logic, or building libraries to make up for the gaps in the ecosystem?
Take Ruby, for example. It is by most metrics not exactly a great language, and I reckon there are very few applications where the language itself is the best option. But take Ruby on Rails and you've suddenly got an opinionated batteries-included web app stack, where you can spend 99% of your time writing only the business logic that matters. No need to spend days fighting with Servant to get its not-quite-there-yet typed DSL to let you write basic CRUD, you can just focus on your MVP.
Want to send some email? You can either write your own Haskell integration of their REST API - orrr use their first-party C# SDK. Rinse and repeat for a dozen dependencies.
And all of that is before it turns out that some of your developers aren't the 20x rockstars you thought they were, and some of their clever high-level abstractions are horribly broken and doing more harm than good...
Haskell for me is "the one that got away". I really like the core language and I really want to use it for absolutely everything, but the ecosystem and culture around it just make that impossible.
Is most of the "business" within the inner logic, and you've got a complicated internal logical process you want to keep safe and solid? Haskell shines.
Do you have a fairly (internally) simple app that does a lot of reaching in and out to the messy outside world? Haskell might not be the most pleasant experience, to put it lightly.
This is due to how it easily lends itself to transforming unstructured inputs into structured outputs, and also because of its amazing asynchronous programming model.
To make a serious rejoinder to a light-hearted comment, I couldn't have, because without Haskell I would have been so annoyed with programming I would have gone into management or something, so that I didn't have to use a "more programmer-friendly" language and want to tear my eyeballs out 8 to 10 hours a day. Seriously. Haskell is the only language I've used which I don't feel gets in my way.
Sure some folks will be able to look under the hood, like the ones writing language runtimes nowadays, transitioning into writing agentic runtimes.
This seems like a contradiction to me. Programming languages are formalisms. What kind of formalisms are you referring to ?
Huh, I thought a monad is just a monoid in the category of endofunctors, what's the problem?
I will say that explaining functors to my coworkers was always much simpler, and then naturally led to monads
For haskellers, it is writing a monad tutorial
For javascripters, it is writing a framework
For make-stuff-with-LLM people, it is producing a diagram explaining your code generation factory
... and so on
In both cases what they really are is an abstract concept defined by things that satisfy some definitions, but in practice it's easier to just look at a few concrete examples like Maybe.
You start from a functor which is a data type that admits a map operation.
Then you add of, or pure, to make an applicative functor, and then you add flatmap to make a monad.
That's quite a hateful way to describe lack of knowledge.
There are some prerequisites that make it easier to understand monads, and a lot of programmers don't even know those. That can make learning monads difficult right off the bat.
It's really basic concepts, much easier than the analysis you do in high school.
But people would rather sit through monad as boxes or burritos cringe tutorials.
Your next step could be to blame the school systems if you want, but that doesn't help the situation at hand.
> Your math explanation starts with a math concept that the vast, vast, vast majority of people will have never even heard of, even in math-adjacent fields
Let me take this apart.
1. a data type that admits a map operation
Present in most languages including JavaScript. Not a mathematical issue.
2. add of, or pure, to make an applicative functor
I had to look this up. It was new content for me, maybe 5 or 10 minutes believing I would get it.
3. add flatmap
This didn’t scare me but maybe it scares others. Not a mathematical issue here, though. Being in C++ doesn’t make this concept mainstream, I guess?
It's a pair of a type constructor F(a) and a map operation a -> b to get an F(b).
The two "non-trivial" details are the fact that the map operation has to respect identity, map(id) = id, and function composition: map(g ∘ f) = map(g) ∘ map(f)
None of those concepts is any difficult, nor requires any "math major" or non-trivial details, because the are not there.
Namely, the section on "Mapping knowledge webs" (around 3:33). It explains people can struggle to adopt concepts that are too far outside their current knowledge, but that it can still be possible for them to pick it up if they can build a path to it from their current knowledge. (This often presents itself as the "depth-first" learning style)
A lot of commenters here, talking about how monads are so simple and how not being able to learn them is just lazy, are misunderstanding how learning fundamentally works. You have to expand the knowledge graph in the direction of monads before it will be easy to pick up monads. You have to build a path. You cannot simply teach monads right off the bat and expect someone to intuitively "get it". People who intuitively "get it" are people who already have a path.
But in practice, I think monads are a poor tool for large-scale software development. I spent a long time trying to build a large game in Haskell and eventually gave up out of frustration with the complexity they introduced.
Monads make sense as a way to manage effects in pure languages like Haskell/Lean/Idris/Agda. But outside that context, I don’t think the additional abstraction is worth the cost.
Understanding how monads work is one thing. Understanding why they’re needed in the first place, and when they’re not, is another.
What sort of situations would you want to give up a little purity or error handling at the type level? Maybe at a boundary where you can just write a very ugly imperative but quarantined section to give it a simpler type?
fmap f Nothing = Nothing
fmap f (Just x) = Just (f x)
pure x = Just x
Nothing >>= f = Nothing
Just x >>= f = f xOtherwise memorize a little bit and dispose of the mystery. It’s not that far out.
You don't need List<A> to write an IntList, nor do you need + to work on different integers in order to have a particular integer.
I still have an old book Putting Metaclasses to Work - A New Dimension in Object-Oriented Programming by Forman et.al somewhere.
There is also the classic The Art of the Metaobject Protocol by Kiczales et.al which is quie relevant here - https://en.wikipedia.org/wiki/The_Art_of_the_Metaobject_Prot...
The key difference is that the Type guys do it at compile time (correctness) while the OO guys do it at runtime (flexibility).
A monad is any construct of abstraction that obeys the Monad Laws. This may seem a useless definition, but my point is that deriving a useful intuition for the concept of the monad is necessarily challenging because they cannot readily be boiled down any further than that without loss of information.
The best intuitive explanation I've developed so far is that a monad is an abstraction over structures of ordered computations. The most ready examples for non-functional programmers are probably exceptions (and their handlers) and nullable types (typically called "optional types" in languages with first-class handling of such things, unlike Java).
This is something you see a lot once you know what you're looking for.
And if you're really lucky, these two are nicely compatible:
For example there are two ways to get from L(L(L(X))) to L(X): By either flattening first in the inside or first on the outside.
And for a monad, you get the same result either way.
And the computational part is then really more of a consequence: If you've got some function of type X->L(Y) and another one of type Y->L(Z) then you can compose them to a function of type X->L(Z).
map :: (a -> b) -> (t a -> t b) -- Functor
bind :: (a -> t b) -> (t a -> t b) -- Monad
cobind :: (t a -> b) -> (t a -> t b) -- Comonad
ap :: t (a -> b) -> (t a -> t b) -- Applicative
The "ordered computation" isn't unique to monads, it applies to all of these when you chain them. For monads particularly though, you can't begin the continuation until the previous result has been generated - whereas with a comonad, you can begin the continuation right away and extract the value afterwards (inside the continuation).
Can also think of it like a producer/consumer or push/pull thing. Monads push values into some type `t`, and comonads pull values out of `t`.
The naming of `return` is perhaps unfortunate as it gives the impression you're returning a value (done to make do-notation look like imperative code) - but monads don't return values. `return` produces a computation.
`coreturn` is usually called `extract`, which is better naming - it extracts a value from a computation.
The order of arguments is also unfortunate because it makes the above pattern less obvious - they're usually written as:
fmap :: f a -> (a -> b) -> f b
bind :: m a -> (a -> m b) -> m b
I like monads as a concept, but in practice I find them frustrating and unnecessarily complicated. I worked on a large game written in Haskell and eventually gave up because dealing with monads made development so cumbersome.
I love the idea, but for real-world projects I’d rather avoid the complexity.
ArrayList's kind is type->type
ArrayList<A>'s kind is type.
The A is what plugs into type on the LHS of the arrow, leaving only the RHS remaining.
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 used to be a big Haskell fan, until I discovered languages like Lean, Agda, and Idris 2 and realized how much cleaner and more coherent the whole thing could be with dependent types built in from the start.
I highly recommend Haskell fans explore Lean/Agda/Idris. They make Haskell feel like a pile of spaghetti by comparison.
It seems a tale about abstraction land, and how it never allows you to exit it again. How you pay taxes for every day spent in it, sold to you as a solution to a problem you didn't think you had.
As any problem can be expressed in C, how would what the author did look like in C? KISS. Abstraction land clearly protects one from such vulgarities.
For a concrete example, suppose that you want to define a data type for JSON objects. You would likely need to choose a type to represent JSON arrays (such as `ArrayList`, in Java), as well as a type to represent JSON objects (such as `HashMap`). However, what if the client wanted to use `TreeMap` instead of `HashMap`?
With "kinds," you would be able to define the JSON data type as something abstract like `JSON<ArrayType, MapType>`, and allow the client to instantiate it as `JSON<ArrayList, HashMap>` or `JSON<ArrayList, TreeMap>`. Unfortunately, in a language such as Java, this is not possible, because `ArrayList`, `HashMap`, and `TreeMap` are themselves generic types, while only non-generic types (such as `Integer`, `String`, or `HashMap<String, Integer>`) can be type parameters. However, in a language with higher-kinded types, such as Scala, this becomes possible.
In these higher-kinded languages, a type such as `Integer` or `HashMap<String, Integer>` would have a "kind" of `*`, while a generic type such as `ArrayList` would have a kind of `* -> *` (meaning: a generic type of one, non-generic type parameter), and `HashMap` and `TreeMap` would both have a "kind" of `* -> * -> *` (meaning: a generic type of two, non-generic type parameters).
C++'s templates permit a similar abstraction to higher-kinded types, and the library nlohmann::json (https://json.nlohmann.me/api/basic_json/) in fact does something very similar to the JSON example that I describe. Namely, it uses `std::vector` as the default for `ArrayType` and `std::map` as the default for `MapType`, but also allows the client to parameterize the underlying container of choice. However, C++ templates need to be fully expanded in order to be typechecked, leading to compile-time error messages that can be long and difficult to read. A "kind" system basically solves this issue by imposing a proper type system onto templates, allowing for more understandable error messages.
See also: Concepts for higher-kinded types in C++20 - https://mmore500.com/cse-491/blog/2020/02/24/concepts-monads...
This is C.
void * bsearch (const void *key, const void *array, size_t count, size_t size, comparison_fn_t compare)
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.
> Types are groups of related values.
This is an operational perspective which misses one of the most important aspects of types: in a statically typed language, types are a way to classify terms, i.e. they're not just about values.
As an example of why this distinction matters, consider this expression: 1 + "hello". In most statically typed languages, this will be rejected at compile time. It doesn't have to be evaluated (i.e. at runtime) to be rejected - it's invalid because the types of the terms - 1 and "hello" - aren't compatible.
This compile-time rejection is only possibly because types apply to terms, and terms aren't values. This is critical to the usefulness of statically-typed languages - without this, they'd have to run the program to detect type errors.
Benjamin Pierce's book "Types and Programming Languages" has some great coverage of this topic.
Also, 1 + "hello" is "1hello", obviously. Have you never read JavaScript? :)
What trips us up is having existing expectations for what an operator called + should do.
Exactly. And if that were the case, you couldn't do very much type checking at compile time.
Javascript, or more specifically Typescript, is precisely why I wrote "In most statically typed languages..."
In Typescript, you can write `1 + "hello"` and the type system will infer that the type of that term is 'string'. It doesn't change anything I wrote above.
No, it's obviously "ello" have you not heard of C?
In "Simply Typed Lambda Calculus" (STLC) there are two grammars for a legal expression.
1) Type Grammar - Type ::= inbuilt types | Type1->Type2 (function)
2) Term Grammar - Term ::= constant | variable | lambda abstraction : "Type" | lambda application.
Note how in (2) above "Type" comes into the picture. During compilation, the expression's structure is analyzed and verified against the Typing Rules aka "Type Checking". Once this is passed the expression is considered sound and can be evaluated at runtime.
In "Calculus of Constructions" (CoC) the two grammars are unified into one which gives us powerful concepts like dependent types, polymorphism etc. - https://news.ycombinator.com/item?id=50137880
Why do you think so? It's a completely standard usage. For example, we can ask MathWorld:
> In logic, a term is a variable ['a', 'f'], constant ['1', '"hello"'], or the result of acting on variables and constants by function symbols ['1+2', 'f(a)'].
(I've added the bracketed material, which provides examples of the senses that MathWorld gives. https://mathworld.wolfram.com/Term.html )
In particular, note that by this wording, if you're looking at '1+2', the "term" is not the string '"1+2"' but the result of adding '1' to '2', which is '3'.
You can talk about 'terms' in the context of how a compiler views source code. Or you can talk about 'terms' in the context of how type theory applies to some computation. They'll be called 'terms' either way; you seem to have staked out the position that the compiler context is obligatory and the type theory context is somehow in error.
In fact the "Calculus of Constructions" (CoC) derived from Typed Lambda Calculus unifies everything into a Term like so;
Term ::= variable | lambda abstraction | lambda application | dependant product | sorts (type of types)
For reference see Brandl's work that i list here - https://news.ycombinator.com/item?id=50028902
In Computation this is just made explicit and clear using a "eval function".
Do you seriously want to argue this point?
> you seem to have staked out the position that the compiler context is obligatory and the type theory context is somehow in error.
I used the compiler to illustrate the issue to people who clearly aren’t familiar with type theory. You imply that you are, but in that case, how do you justify the nonsense quoted above?