Types of types: Haskell's Kind system

(thunk.blog)

43 points | by Thom2503 3 days ago

5 comments

  • adamddev1 3 hours ago
    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.
    • thomasfromcdnjs 2 hours ago
      I've been vibe coding my own language and it's compiler is in Haskell, it's been great for the agents to be inspired by Haskell and I'm having fun just adding random language features, currently implementing prophecy ghost variables. Not really a public project but can suss it out for now at http://lsalpha.com
      • bigmadshoe 2 hours ago
        This is super cool! You should put a clear example implementation of a feed forward network, transformer block, loss function, or something more ML specific on the homepage, assuming you're primarily targeting that domain.

        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.

        • entropy47 38 minutes ago
          Neatly summarises my experience of most vibe coded projects unfortunately.
  • i2talics 2 hours ago
    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.
    • taolson 1 hour ago
      That may be true for functions which operate on a generic Monad typeclass, but typeclasses (Higher kinded types) aren't required to implement concrete Functor / Applicative / Monad instances for a particular type, e.g. Maybe:

          fmap f Nothing = Nothing
          fmap f (Just x) = Just (f x)
      
          pure x = Just x
      
          Nothing >>= f = Nothing
          Just x >>= f = f x
      • fn-mote 20 minutes ago
        When people say they don’t understand Monad, my first assumption is that they are wearing their ignorance as a badge of honor.

        Otherwise memorize a little bit and dispose of the mystery. It’s not that far out.

    • caaqil 2 hours ago
      > things that makes monads notoriously difficult to explain to people outside of the Haskell ecosystem

      Huh, I thought a monad is just a monoid in the category of endofunctors, what's the problem?

      • girvo 2 hours ago
        And here I was convinced that they’re burritos!

        I will say that explaining functors to my coworkers was always much simpler, and then naturally led to monads

        • hexasquid 3 minutes ago
          I suspect all branches of tech have their rite of passage.

          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

    • rramadass 1 hour ago
      Some OO languages have a parallel concept in "Metaclass" (https://en.wikipedia.org/wiki/Metaclass) i.e. the class of a class which is structurally similar to "Kind" though of course the mechanics are quite different.

      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).

    • epolanski 2 hours ago
      The thing that makes monads difficult is laziness and the anti math circle jerk.

      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.

      • windward 1 hour ago
        It's odd, the stereotype of software developers is a know-it-all attitude, but start talking about types and you get excuses that boil down to 'I'm incapable of learning to understand the thing you learned to understand'.
      • LoganDark 2 hours ago
        > The thing that makes monads difficult is laziness and the anti math circle jerk.

        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.

        • epgui 51 minutes ago
          Lack of knowledge is not the problem at all. Anti-intellectualism is.
          • LoganDark 43 minutes ago
            You can try to blame lack of knowledge on anything you want, but at the end of the day Hacker News is for intellectual curiosity and even HN readers don't all know what monads are.
        • epolanski 1 hour ago
          No there's no complexity behind monads except laziness and anti math circle jerk.

          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.

          • xboxnolifes 1 hour ago
            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. It's not anti-math reasoning. It's a lack of self-awareness that your background is very math heavy, which makes that particular explanation make sense to you. I've gone my entire schooling, as a student who was always one of the few who were "good at math", all the the way through my CS education, without ever having heard of a functor until I came across the Haskell monad explanation meme.

            Your next step could be to blame the school systems if you want, but that doesn't help the situation at hand.

            • fn-mote 9 minutes ago
              >> 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.

              > 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?

              https://en.cppreference.com/cpp/container/flat_map

  • vatsachak 1 hour ago
    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.

    • ivanjermakov 40 minutes ago
      In my experience such categories pop up when dealing with immutable data, which is common in many domains.
  • cat-whisperer 1 hour ago
    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
  • antonvs 2 hours ago
    > 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.

    • thaumasiotes 54 minutes ago
      > This is not correct.

      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.

    • antonvs 1 hour ago
      Following on from the above, this statement is also incomplete at best:

      > 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.

      • LoganDark 1 hour ago
        Do you mean that if types had only to do with values, you would have to evaluate the term to determine type?

        Also, 1 + "hello" is "1hello", obviously. Have you never read JavaScript? :)