4 ms·

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

> 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 ago
Your 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.
- catnaroek 9y ago
  > You then provided an example of something you claimed could not be done monadically. Using a monad, i.e., an endofunctor with unit and join that satisfies the well-known laws, you cannot do it. > 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). Is a so-called “indexed monad” really a monad, now? > You then claimed that in order to implement the memory allocation example you would need substructural types, which is not the case. It is the case. What else could be the point to the threaded typestate in the definition of so-called “indexed monads”? Moreover, even with the threaded typestate, so-called “indexed monads” may fail to achieve the desired goal of manipulating resources linearly, e.g. the “indexed list monad” provides no such guarantees.

tathougies 9y ago

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

catnaroek 9y ago
> You then provided an example of something you claimed could not be done monadically. Using a monad, i.e., an endofunctor with unit and join that satisfies the well-known laws, you cannot do it. > 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). Is a so-called “indexed monad” really a monad, now? > You then claimed that in order to implement the memory allocation example you would need substructural types, which is not the case. It is the case. What else could be the point to the threaded typestate in the definition of so-called “indexed monads”? Moreover, even with the threaded typestate, so-called “indexed monads” may fail to achieve the desired goal of manipulating resources linearly, e.g. the “indexed list monad” provides no such guarantees.