4 ms·
I used the ‘(correct)’ there to notate a little bit of pedantry :) You can of course write interesting things about monads in languages without HKTs, and use th
by Twey 3y ago
I used the ‘(correct)’ there to notate a little bit of pedantry :) You can of course write interesting things about monads in languages without HKTs, and use them as a bridge to explain the operations of real monads — but those things will not, strictly speaking, _be_ monads, which are a sort of type constructor (map on objects) with some extra operations.
You can of course also always implement a language with HKTs in a language without HKTs, deciding which parts of the language should be read as types and which as terms, but it's unclear to me once you start doing that exactly where we should say you're no longer expressing the concept in the meta-language.
- scotty79 3y agoThere is a lot of theory but it is way more informative to say that a monad is just type (in colloquial sense of the word) of containers that have few particular behaviors associated that do wrapping and unwrapping and applying functions to their contents. The problem with that is that all of that is trivial and barely a curiosity. To make monads interesting you have to show specific instances of monads like Maybe. So the monad part is not interesting. The interesting part is what they do besides being a monad. And in some cases you need to depart from monadic purity pretty quickly to get useful behavior (Promises). So I suspect that people talk about monads mostly in the context of HKTs because that's the only place they can seem impressive. To give analogy, I'm sure that integrals in formalization of Lebesgue are super impressive but when you try to teach someone new about integrals you don't start with that and the minutia of all the math notation required for correct formalization, because "area under the curve" or "inverse of differentiation" are way better as they have immediate utility and operate in the context of what the learner already most likely knows.
- Twey 3y agoThere's a problem in the teaching of monads that containers are the easiest ones to explain, but also the least interesting in practice :) >To make monads interesting you have to show specific instances of monads like Maybe. While individual monads are useful by themselves, the _concept_ of ‘monad’ is only interesting once you can generalize over it. If you can't write (interesting) code that's generic over an interface, there's not much point in doing the work to generalize from the specific instances of that interface. But part of why monads are interesting is that it turns out a lot of natural ‘sequential’ code that one might write in a procedural language actually generalizes naturally to an arbitrary monad, in ways that make the resulting code drastically (even unintuitively, for someone used to thinking in terms procedural code just meaning single-valued strictly-ordered sequencing) more powerful. I think to me the idea that talking about monads as monads is only useful once you can generalize over monads, and HKTs are necessary to effectively generalize over monads (‘effectively’ meaning without undue cognitive or syntactic load), is a much more likely explanation than the slightly uncharitable one that people are pulling in HKTs as a smokescreen for bloviation. > In some cases you need to depart from monadic purity pretty quickly to get useful behavior One of the main motivations for introducing the monad interface to semantics, and thence to programming, is that notions like stateful, multivalued, or asynchronous execution that are ‘impure’ (i.e. outside the model) when considering a program as a function (Scott semantics) can in fact be reasoned about in a ‘pure’ way by adding a monad to the codomain of the function. So things like `Promise` are not ‘departing from monadic purity’, they're good and true examples of upstanding monads :) Even ‘naughty’ monads like Haskell's `IO` can notionally be thought of as pure — the fact that the interpretation of the monad is done by a magical external runtime and not by pure functional code that passes the world around is more an artefact of the external code of the OS/computer you're running on, and you can think of it as a sort of implementation detail/performance optimization. > "area under the curve" or "inverse of differentiation" are way better as they have immediate utility and operate in the context of what the learner already most likely knows. Fully agree with you there, but you don't then try to explain algebraic topology in terms of the area under the curve. You can (and generally should!) start from a point the reader is already familiar with, but it's a perfectly defensible decision to go from there on a path through intermediate concepts that make explaining the target notion easier, rather than throwing the reader straight into the deep end. Of course the choice of how long or short the path should be (and therefore how big the jumps one expects the reader to make) is a decision that is the writer's responsibility.