Haskell's kind system - a primer

[dcastro]

Comments left here will be displayed on this blog post: https://diogocastro.com/blog/2018/10/17/haskells-kind-system-a-primer/

[giuliohome]

Hi! thank you for this post. Quick question: assuming that Haskell types and kinds are awesome, don't you find a bit sad that there is no Haskell framework to effectively take advantage of them in a practical and modern i/o app for web or desktop or mobile development? Is it only a purely intellectual exercise?

[dcastro]

Thank you for the comment @giuliohome!

The good news is, there are! Yesod and Servant are two frameworks for web development that rely heavily on advanced type-level programming features, which would not be possible without a kind system in the first place.

A great chunk of the Haskell ecosystem is built on this foundation in one way or another, so it's far from being a purely intellectual exercise. For a casual Haskell user, this might not be obvious because the authors of these libraries/frameworks go to great lengths to make this as seamless as possible and to minimize the burden on their users.

[dpwiz]

Please enable NoStarIsType for the post :smile:

[pythonissam]

Great post! We'd like to translate this into Japanese and publish it on our site so that we can share such valuable information. May I ask your permission?

[dcastro]

@wiz I admit I wasn't counting on GHC 8.6 being released while I was writing this 😄 bad timing I guess.

@pythonissam Yes, of course, I'd be honoured! Let me know when it's done and I'll add a link to it here.

[pythonissam]

Thank you! I'm going to tell you when it's done:)

[juselius]

Excellent post! This is a really nice summary of Haskell kind level programming. Clear and readable. This should go into a textbook. Well done!

[ysharoda]

Thanks for the nice post.. I have a question that sounds very primitive:

NonEmpty [] Bool is a list of boolean values that is guaranteed to have at least one value

Why isn't the list part of the type written as [Bool], as would be written in Haskell normally?

[dcastro]

Thank you @ysharoda, that's a very pertinent question! And one that's not particularly easy to explain.

I'm guessing the point of confusion is probably related to lists/[] being a special built-in type in Haskell, with special syntax.

It might help to point out that [Bool] is just syntax sugar for [] Bool. The list type [] is parameterised over the type of its elements, Bool. This makes more sense when you compare [] Bool to other collection types, like Vector Bool or Tree Bool.

In light of this, NonEmpty [Bool] could be re-written as NonEmpty ([] Bool), without syntax sugar.

---

So now your question becomes: why is it written NonEmpty [] Bool instead of NonEmpty ([] Bool)?

Well, writing NonEmpty ([] Bool) wouldn't typecheck, because the NonEmpty type constructor expects two arguments, not one.

data NonEmpty f a = MkNonEmpty { head :: a, tail :: f a }

• f is a type variable of kind * -> *, i.e., the type of a generic container, like Vector, Tree, or [].
• a is a type variable of kind *, i.e., the type of the elements in the container, like Bool, Int, etc.

That's why the types [] and Bool have to be passed separately, one at a time, to the type constructor NonEmpty.

As an exercise, you can try writing a version of NonEmpty that takes a single type variable instead of two, and hopefully it'll become clear why it's defined the way it is.

If any part of this explanation is unclear or insufficient, please let me know, I'd be happy to clarify.

[cakraww]

This is very well-written, thank you. Looking forward to your next posts!

[theGhostJW]

Thanks for a great, clear post !!