8 ms·

Haskell's kind system: a primer

221 points by ristem 8y ago

tiniuclx 8y ago
I've been writing a lot of Haskell recently. I had to switch to embedded C and the difference between the two was striking. The C program I was editing compiled, but failed to do anything useful. To fix that, I had to reorder the stateful functions and #define the right things without much help from the compiler. Had I been using Haskell and a reasonably well designed library, these mistakes could've been caught at compile time, with the compiler telling me exactly what I did wrong. The kind system described in the article is how you would implement such a library, or something even more advanced. Sure, comparing embedded C to Haskell is disingenuous, but it does show how far programming languages have come. And I think my experience could definitely happen in many other mainstream languages.
- m_mueller 8y ago
  What exactly is it that stops Haskell from being used in embedded? GHC has an LLVM backend, and LLVM should support most embedded architectures, am I mistaken there? I have some suspicions of what it could be, but it would be interesting to read your opinion/experience first.
  - tiniuclx 8y ago
    Sure, you could likely compile a Haskell program to an embedded architecture, but Haskell is a garbage collected language. Allocating memory takes a long, nondeterministic amount of time on a microcontroller. And microcontroller are often used in control systems, where latency kills. Haskell also suffers from space leaks due to its lazyness. Microcontrollers have memory in the order of kilobytes, sometimes even less than that. You simply can't risk running out of memory, which is why micros are programmed in C or assembly, where you have a vice-like grip on how much RAM you use. For a higher-level look at the problem, consider that embedded systems are a high volume product. Saving a penny by using a cheaper, weaker micro adds up very quickly when you're shipping tens, or hundreds of thousands of devices. At that scale, it's profitable to spend more on non-recurring engineering (programmer time) in order to reduce the cost of manufacturing. If you want a functional-style language that is likely very well suited to embedded devices, look no further than Rust. While I haven't had the time to learn it (maybe next year), the language looks very promising due to its memory model.
    - m_mueller 8y ago
      Thanks! That‘s pretty much exactly what I thought and I agree Rust looks promising for this purpose. On the other hand this is a variation of the two-language-problem and I wonder if it couldn’t in theory be solved with an approach like in Julia (even though it hasn’t so far in practice).
    - setr 8y ago
      There’s not really any reason you couldn’t have a language that eventually offer almost all of haskell’s compile-level safety features, while keeping the vice grip, is there? Most of haskell’s benefits comes from its “sufficiently advanced compiler”, without reliance on gc benefits, I would think. Other than laziness, is haskell-the-language actually that dependent on a gc?
      - m_mueller 8y ago
        A language is not just a set of possible semantics, it‘s also an ecosystem that herds people towards using it in a certain way. If that ecosystem breaks down under certain conditions the language becomes unusable. I think that aspect of language design is often underappreciated and maybe the main reason why we don’t have (and maybe will never) a one language to rule them all.
    - pjmlp 8y ago
      While you are kind of right, when comparing managed languages with modern micro-controllers, people should go back and check the hardware capabilities of those 70's mainframes running Lisp binaries. A PIC won't do it, but there are others that will surely be able to.
      - pflanze 8y ago
        The PIC18 can run the following Scheme implementation: https://github.com/stamourv/picobit https://github.com/stamourv/picobit (The (last of the original) main author(s) has stopped maintaining it, although there are many forks, some of which might be maintained, I haven't checked.)
  - kccqzy 8y ago
    Mostly the large runtime. Which requires pretty extensive OS features. But check out Haskell-based unikernels.
- dllthomas 8y ago
  Note, though, that even in C you can get some super useful help from the compiler if you structure your code for it.
ainar-g 8y ago
This was the clearest introduction into types vs kinds in Haskell that I have ever read. Definitely going to recommend to my friends. Are there other good articles by the author?
- rnavarro 8y ago
  His typeclasses article is also fantastic: https://diogocastro.com/blog/2018/06/17/typeclasses-in-perspective/ https://diogocastro.com/blog/2018/06/17/typeclasses-in-persp...
MaxBarraclough 8y ago
I had no idea Haskell used 'kind' to refer to something codified and concrete in this way -- usually we see the word 'type' used to refer to the concrete type-systems stuff, and 'kind' to refer to the fuzzier, less precise idea of, uh, what it is the data is. Type theorists say things like "Type systems let us reify what kind of data we are dealing with". It's a bit like when Java took the fuzzy term 'interface' and made it a concrete technical concept, or when Apple added closures to Objective-C and called them 'blocks', which was previously a fuzzy term. Will we have to start using another word to refer to the fuzzier concept, if not 'kind'? 'Sort' is already taken. 'Category' is already taken. Perhaps the 'nature' of the data?
- lmm 8y ago
  Kinds are a distinct concept from types, and that concept needs a name, and it's best to choose a name where the intuitive meaning of the name aligns with the technical one (indeed Haskell attracts a lot of criticism when it uses names like "monad" that don't have a "fuzzy" meaning). It goes even further: types-of-kinds are called "sorts", though in Haskell there's only one possible sort of kind. There are only two hard problems in computer science, after all.
  - jacobush 8y ago
    Naming and ?? (Computability?)
    - hiker 8y ago
      "There are only two hard things in Computer Science: cache invalidation and naming things." -- Phil Karlton But I do like "Computability and naming things" better.
      - gpderetta 8y ago
        There are only two hard things in Computer Science: cache invalidation, naming things and off by one errors. -- Anonymous
divan 8y ago
The article is exemplary – it's reasonably short, concise, beautifully visualized and explains a complex topic with simple terms. I'm confused with "type promotion" in the `ConnectionStatus` example, though. When we promote `Open` and `Closed` from terms to types, we make it easy to create a variable that can be either `Open` or `Closed`, but we're also breaking the mental model of the whole thing. `Open`/`Closed` is a property – not a "type" in a traditional way of thinking about types. For me, the type should map onto some abstraction in your mental world map, and `Open`/`Closed` is definitely not a good fit here. How do Haskell programmers address this problem? Do they think about types more in mathematical terms, rather than as tools for describing mental maps of the problem domain?
- tiniuclx 8y ago
  Open/Closed would still conceptually act as properties, but by promoting them to types you enforce the property at compile time rather than runtime. Note that they are not used on their own, but to describe a `Connection`. This lets you statically enforce the fact that you must only send data through an open connection, for example.
  - divan 8y ago
    Right, that's the obvious benefit for the compiler (statically enforcing behaviour, etc), but I'm struggling with not seeing here a detremential effect for the human. To me, when you write code, you're encoding your understanding of the problem domain (mental map) into the code, describing it in a way that permits to restore it back. By reading a code your coworker or you 6 month later should be able to restore the same mental map you had while writing the code. And using type system to describe properties (there is another way to do it already in place – fields in structs), seems like complicating this task and it eventually should hurt readability.
    - almostdeadguy 8y ago
      The advantage is you basically don't have to think about the provenance of data (in this example what state is a connection in? was it closed before being given to me? etc.). It allows the compiler to ensure the user of this code can't perform operations that lead to error states by allowing the programmer to express the state transitions of a connection in their function declarations, as the provided example shows: newConnection :: Address -> Connection Closed openConnection :: Connection Closed -> Connection Open closeConnection :: Connection Open -> Connection Closed connectionAddress :: Connection s -> Address From a readability perspective, I would love this, it's effectively a state machine diagram explained by your function types.
deleted 8y ago
[deleted]
fmap 8y ago
That's a really beautiful article! Using kinds to keep track of the concrete representation of a reference to a type (rather than the concrete representation of the type itself) is one of the real gems in GHCs design. However, one problem with it is that a polymorphic type, such as [] of kind "* -> *", or a function like map of type "forall a b. (a -> b) -> [a] -> [b]" really only works with boxed types. I always wondered how expensive it would be to monomorphize everything at the level of kinds and have what GHC calls levity polymorphism by default. Languages like Rust and C++ always monomorphize everything and while this does get slow it is still not the exponential blowup that theory suggests. In fact, there is an ML compiler (MLton) which does the same and it is still not too bad. Doing it at the level of reference representation - which is where the generated code actually needs to change - should be much cheaper and definitely a practical default. The only real problem I see is that you could in principle write code that does "kind polymorphic" recursion, which couldn't be compiled away. But that sounds seriously crazy and I see no reason to allow it in the first place...
- lmm 8y ago
  > The only real problem I see is that you could in principle write code that does "kind polymorphic" recursion, which couldn't be compiled away. But that sounds seriously crazy and I see no reason to allow it in the first place... Wouldn't you want kind-polymorphic recursion for implementing recursion-schemes like patterns at the type level?
- Athas 8y ago
  > However, one problem with it is that a polymorphic type, such as [] of kind "* -> ", or a function like map of type "forall a b. (a -> b) -> [a] -> [b]" really only works with boxed types. Can you explain why this is, or provide a reference to literature where it was investigated? I still (even after getting a PhD in compiling functional languages!) do not understand why you could not create code parameterised over the sizes of the arguments. For example, a 'cons' cell could be represented as first the size of the 'car' in bytes, then the 'car' value inline/unboxed, then a pointer to the 'cdr' cell. The Sixten language[0] does this, although it's still very early in its development. I'm not saying this is necessarily a good solution, I just wonder why I have never seen it seriously considered (and perhaps rejected). In practice, I do believe that monomorphisation is very often a good strategy. [0]: https://github.com/ollef/sixten https://github.com/ollef/sixten
state_less 8y ago
I always thought it was beautiful that Haskell turned type construction into just another function on a different domain. What do people call this abstraction?
- danharaj 8y ago
  Pronounced System F Omega. https://en.wikipedia.org/wiki/System_F#System_F%CF%89 https://en.wikipedia.org/wiki/System_F#System_F%CF%89
- kccqzy 8y ago
  Type-level functions are called type families. They are really not just another function. But if you appreciate that beauty, check out a dependently types language like Idris where normal functions can be used on the type-level as well. So you might have a vector type with a length computed by a complicated expression.
calebh 8y ago
Once you understand kinds, it's not so hard to understand typeclasses and monads. Type classes are a way to overload functions in a controlled way, by defining a set of function signatures where the overall typeclass is parameterized by a type constructor of arbitrary kind. I cover this in my blog post here: http://www.calebh.io/Monads-as-Programmable-Semicolons/ http://www.calebh.io/Monads-as-Programmable-Semicolons/
mlevental 8y ago
what is this blog format/static site generator thing?

221 points by ristem 8y ago

I've been writing a lot of Haskell recently. I had to switch to embedded C and the difference between the two was striking. The C program I was editing compiled, but failed to do anything useful. To fix that, I had to reorder the stateful functions and #define the right things without much help from the compiler. Had I been using Haskell and a reasonably well designed library, these mistakes could've been caught at compile time, with the compiler telling me exactly what I did wrong. The kind system described in the article is how you would implement such a library, or something even more advanced. Sure, comparing embedded C to Haskell is disingenuous, but it does show how far programming languages have come. And I think my experience could definitely happen in many other mainstream languages.

m_mueller 8y ago
What exactly is it that stops Haskell from being used in embedded? GHC has an LLVM backend, and LLVM should support most embedded architectures, am I mistaken there? I have some suspicions of what it could be, but it would be interesting to read your opinion/experience first.
- tiniuclx 8y ago
  Sure, you could likely compile a Haskell program to an embedded architecture, but Haskell is a garbage collected language. Allocating memory takes a long, nondeterministic amount of time on a microcontroller. And microcontroller are often used in control systems, where latency kills. Haskell also suffers from space leaks due to its lazyness. Microcontrollers have memory in the order of kilobytes, sometimes even less than that. You simply can't risk running out of memory, which is why micros are programmed in C or assembly, where you have a vice-like grip on how much RAM you use. For a higher-level look at the problem, consider that embedded systems are a high volume product. Saving a penny by using a cheaper, weaker micro adds up very quickly when you're shipping tens, or hundreds of thousands of devices. At that scale, it's profitable to spend more on non-recurring engineering (programmer time) in order to reduce the cost of manufacturing. If you want a functional-style language that is likely very well suited to embedded devices, look no further than Rust. While I haven't had the time to learn it (maybe next year), the language looks very promising due to its memory model.
  - m_mueller 8y ago
    Thanks! That‘s pretty much exactly what I thought and I agree Rust looks promising for this purpose. On the other hand this is a variation of the two-language-problem and I wonder if it couldn’t in theory be solved with an approach like in Julia (even though it hasn’t so far in practice).
  - setr 8y ago
    There’s not really any reason you couldn’t have a language that eventually offer almost all of haskell’s compile-level safety features, while keeping the vice grip, is there? Most of haskell’s benefits comes from its “sufficiently advanced compiler”, without reliance on gc benefits, I would think. Other than laziness, is haskell-the-language actually that dependent on a gc?
    - m_mueller 8y ago
      A language is not just a set of possible semantics, it‘s also an ecosystem that herds people towards using it in a certain way. If that ecosystem breaks down under certain conditions the language becomes unusable. I think that aspect of language design is often underappreciated and maybe the main reason why we don’t have (and maybe will never) a one language to rule them all.
  - pjmlp 8y ago
    While you are kind of right, when comparing managed languages with modern micro-controllers, people should go back and check the hardware capabilities of those 70's mainframes running Lisp binaries. A PIC won't do it, but there are others that will surely be able to.
    - pflanze 8y ago
      The PIC18 can run the following Scheme implementation: https://github.com/stamourv/picobit https://github.com/stamourv/picobit (The (last of the original) main author(s) has stopped maintaining it, although there are many forks, some of which might be maintained, I haven't checked.)
- kccqzy 8y ago
  Mostly the large runtime. Which requires pretty extensive OS features. But check out Haskell-based unikernels.
dllthomas 8y ago
Note, though, that even in C you can get some super useful help from the compiler if you structure your code for it.

ainar-g 8y ago

This was the clearest introduction into types vs kinds in Haskell that I have ever read. Definitely going to recommend to my friends. Are there other good articles by the author?

rnavarro 8y ago
His typeclasses article is also fantastic: https://diogocastro.com/blog/2018/06/17/typeclasses-in-perspective/ https://diogocastro.com/blog/2018/06/17/typeclasses-in-persp...

MaxBarraclough 8y ago

I had no idea Haskell used 'kind' to refer to something codified and concrete in this way -- usually we see the word 'type' used to refer to the concrete type-systems stuff, and 'kind' to refer to the fuzzier, less precise idea of, uh, what it is the data is. Type theorists say things like "Type systems let us reify what kind of data we are dealing with". It's a bit like when Java took the fuzzy term 'interface' and made it a concrete technical concept, or when Apple added closures to Objective-C and called them 'blocks', which was previously a fuzzy term. Will we have to start using another word to refer to the fuzzier concept, if not 'kind'? 'Sort' is already taken. 'Category' is already taken. Perhaps the 'nature' of the data?

lmm 8y ago
Kinds are a distinct concept from types, and that concept needs a name, and it's best to choose a name where the intuitive meaning of the name aligns with the technical one (indeed Haskell attracts a lot of criticism when it uses names like "monad" that don't have a "fuzzy" meaning). It goes even further: types-of-kinds are called "sorts", though in Haskell there's only one possible sort of kind. There are only two hard problems in computer science, after all.
- jacobush 8y ago
  Naming and ?? (Computability?)
  - hiker 8y ago
    "There are only two hard things in Computer Science: cache invalidation and naming things." -- Phil Karlton But I do like "Computability and naming things" better.
    - gpderetta 8y ago
      There are only two hard things in Computer Science: cache invalidation, naming things and off by one errors. -- Anonymous

divan 8y ago

The article is exemplary – it's reasonably short, concise, beautifully visualized and explains a complex topic with simple terms. I'm confused with "type promotion" in the `ConnectionStatus` example, though. When we promote `Open` and `Closed` from terms to types, we make it easy to create a variable that can be either `Open` or `Closed`, but we're also breaking the mental model of the whole thing. `Open`/`Closed` is a property – not a "type" in a traditional way of thinking about types. For me, the type should map onto some abstraction in your mental world map, and `Open`/`Closed` is definitely not a good fit here. How do Haskell programmers address this problem? Do they think about types more in mathematical terms, rather than as tools for describing mental maps of the problem domain?

tiniuclx 8y ago
Open/Closed would still conceptually act as properties, but by promoting them to types you enforce the property at compile time rather than runtime. Note that they are not used on their own, but to describe a `Connection`. This lets you statically enforce the fact that you must only send data through an open connection, for example.
- divan 8y ago
  Right, that's the obvious benefit for the compiler (statically enforcing behaviour, etc), but I'm struggling with not seeing here a detremential effect for the human. To me, when you write code, you're encoding your understanding of the problem domain (mental map) into the code, describing it in a way that permits to restore it back. By reading a code your coworker or you 6 month later should be able to restore the same mental map you had while writing the code. And using type system to describe properties (there is another way to do it already in place – fields in structs), seems like complicating this task and it eventually should hurt readability.
  - almostdeadguy 8y ago
    The advantage is you basically don't have to think about the provenance of data (in this example what state is a connection in? was it closed before being given to me? etc.). It allows the compiler to ensure the user of this code can't perform operations that lead to error states by allowing the programmer to express the state transitions of a connection in their function declarations, as the provided example shows: newConnection :: Address -> Connection Closed openConnection :: Connection Closed -> Connection Open closeConnection :: Connection Open -> Connection Closed connectionAddress :: Connection s -> Address From a readability perspective, I would love this, it's effectively a state machine diagram explained by your function types.

deleted 8y ago

[deleted]

fmap 8y ago

That's a really beautiful article! Using kinds to keep track of the concrete representation of a reference to a type (rather than the concrete representation of the type itself) is one of the real gems in GHCs design. However, one problem with it is that a polymorphic type, such as [] of kind "* -> *", or a function like map of type "forall a b. (a -> b) -> [a] -> [b]" really only works with boxed types. I always wondered how expensive it would be to monomorphize everything at the level of kinds and have what GHC calls levity polymorphism by default. Languages like Rust and C++ always monomorphize everything and while this does get slow it is still not the exponential blowup that theory suggests. In fact, there is an ML compiler (MLton) which does the same and it is still not too bad. Doing it at the level of reference representation - which is where the generated code actually needs to change - should be much cheaper and definitely a practical default. The only real problem I see is that you could in principle write code that does "kind polymorphic" recursion, which couldn't be compiled away. But that sounds seriously crazy and I see no reason to allow it in the first place...

lmm 8y ago
> The only real problem I see is that you could in principle write code that does "kind polymorphic" recursion, which couldn't be compiled away. But that sounds seriously crazy and I see no reason to allow it in the first place... Wouldn't you want kind-polymorphic recursion for implementing recursion-schemes like patterns at the type level?
Athas 8y ago
> However, one problem with it is that a polymorphic type, such as [] of kind "* -> ", or a function like map of type "forall a b. (a -> b) -> [a] -> [b]" really only works with boxed types. Can you explain why this is, or provide a reference to literature where it was investigated? I still (even after getting a PhD in compiling functional languages!) do not understand why you could not create code parameterised over the sizes of the arguments. For example, a 'cons' cell could be represented as first the size of the 'car' in bytes, then the 'car' value inline/unboxed, then a pointer to the 'cdr' cell. The Sixten language[0] does this, although it's still very early in its development. I'm not saying this is necessarily a good solution, I just wonder why I have never seen it seriously considered (and perhaps rejected). In practice, I do believe that monomorphisation is very often a good strategy. [0]: https://github.com/ollef/sixten https://github.com/ollef/sixten

state_less 8y ago

I always thought it was beautiful that Haskell turned type construction into just another function on a different domain. What do people call this abstraction?

danharaj 8y ago
Pronounced System F Omega. https://en.wikipedia.org/wiki/System_F#System_F%CF%89 https://en.wikipedia.org/wiki/System_F#System_F%CF%89
kccqzy 8y ago
Type-level functions are called type families. They are really not just another function. But if you appreciate that beauty, check out a dependently types language like Idris where normal functions can be used on the type-level as well. So you might have a vector type with a length computed by a complicated expression.

calebh 8y ago

Once you understand kinds, it's not so hard to understand typeclasses and monads. Type classes are a way to overload functions in a controlled way, by defining a set of function signatures where the overall typeclass is parameterized by a type constructor of arbitrary kind. I cover this in my blog post here: http://www.calebh.io/Monads-as-Programmable-Semicolons/ http://www.calebh.io/Monads-as-Programmable-Semicolons/

mlevental 8y ago

what is this blog format/static site generator thing?