3 ms·
> In this post we’ll have a look at some instances of such sitations, their “ad hoc” solutions provided at the language level, and finally at how these problems
by catnaroek 9y ago
> In this post we’ll have a look at some instances of such sitations, their “ad hoc” solutions provided at the language level, and finally at how these problems can be solved in a uniform way using Monads.
I wonder if the blog post's author is actually aware that the original application of monads to programming languages was precisely to give a denotational semantics to strict higher-order languages. In other words, you don't “add monads” to JavaScript. A monad, perhaps an entire monad transformer stack, is already hardwired into its semantics.
Now, I'm aware that the author says at the end:
> We’ve had a look at this from a syntactic perspective.
But monads are about semantics, not syntax. Of course, if you want uniform syntax for using monads, then say just that.
---
> For-loop Hell occurs when iteration through multiple dependent data sets is needed. Just as for null-checking, our code becomes deeply nested, with a lot of syntactic clutter and needless bookkeeping.
You know what's a simple, clean, straightforward solution to “for-loop hell”? Helper procedures. It baffles me why people always reach for the bazooka when a fly swatter will do.
> Both the State and ST monads bound the lifetime of a stateful computation, ensuring that programs remain easily reasoned about in the general case.
Yet neither can express the following very useful pattern:
allocate A
allocate B; use A B; deallocate A
allocate C; use B C; deallocate B
...
allocate Z; use Y Z; deallocate Y
deallocate Z
> The `ST` Monad provides more performant state with references, at the cost of some higher order behaviour.
`ST` is not about “performance”. It's about semantics. With `State`, you have to know beforehand the state type, and you cannot change it in the middle of the computation. With `ST`, you can allocate whatever you want in the middle of a computation, and it doesn't have to be reflected in the computation's type.
- tathougies 9y agoyou can use monads to do your last example....
- catnaroek 9y agoNo, you need proper substructural types. Not even monadic regions will help.
- tathougies 9y agoYou do not need a type system to use monads. In particular, your example could be written (in a statically typed Haskell-like language) using indexed monads. In a dynamically typed language, you wouldn't need that.
- catnaroek 9y agoOf course, you don't need types to write programs. Types are just a way to mechanically verify some desirable properties. But, as it turns out, resource management in large programs is pretty damned hard to get right without this kind of mechanical assistance. So, of course, when I say “it's inexpressible without <type system feature>”, what I mean is “it's impossible to mechanically verify it without <type system feature>”.
- tathougies 9y agoMonads have nothing to do with verification, so I'm now unsure what your original point was. It's not surprising that you can't use a banana to edit text, so it's not surprising you can't use the general idea of monad to do verification.
- catnaroek 9y ago> Monads have nothing to do with verification, so I'm now unsure what your original point was. Indeed, monads are about language semantics, prior to any verification attempt. Have you tried actually tried reading my original comment?
- tathougies 9y agoYour original comment was about language semantics. You then provided an example of something you claimed could not be done monadically. I pointed out that you could implement such a thing with "indexed monads", which are a subclass of monads (although not one that's easily used in any current programming language, Haskell included). You then claimed that in order to implement the memory allocation example you would need substructural types, which is not the case. Then you claimed that you needed the type system feature to verify the memory was allocated/released correctly. You are correct that you need an advanced type system and type checker to do the memory validation. However, the validator tool only needs to know about one monad (your resource one). This one monad is a small subset in the very large space of 'things that form a monad'. It's like if I said, 'groups are about arithmetic'. While true that many arithmetic operations can be expressed as a group, groups are not inherently about arithmetic. That would be conflating common use cases with the generalization.