Paul,
monads were not invented because I/O could not be presented in another way in Haskell. Monads are way older than Haskell. It is a concept of category theory which was developed in the 1950s. Actually some concepts of algebra that are even older turn out to be monads. Take Galois theory for example. Once you know the pattern, you find a monad under every stone you turn around. It's one of the luckiest things that people like Moggi and Wadler realized that monads can be applied to structure programs. And don't blame them that monads are not composable - it is simply a mathematical fact. Some monads do compose with any other monad, and those are the monad transformers. If you like Prolog's relational programming model so much, then you should play with those programs that have "no business value". Because Haskell's type inference algorithm, together with multi-parameter type classes and maybe type level natural numbers together give rise to Prolog-like capabilities. All the work is done by the compiler this way. What you say about FSM is certainly true to some extent - they are well understood, can be generated automatically, and there is decent theory to reason about them. That is why this model is used in safety-sensitive environments such as aviation. I once applied for a position in verification in the automotive industry, and the interview partner told me that they struggle mightily with the vast state spaces of the FSMs they are checking. All this speaks in favour of Haskell. The semantics is simple and beautiful, because it is a single-paradigm language. And because of that, clever people can leverage theorem provers to mathematically prove correctness of Haskell code. I don't know of many languages where that is possible. (But then, I'm not an expert on verification.) Olaf _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Hello, Olaf! It's very good point. I'll read more about it. May be I'm
wrong, but I don't remember any monads in CT, so my suggestion was that they were introduced in pure functional languages research (Hope, Haskell), not math itself. May be I'm not right. Thanks a lot! 15.07.2018 23:06, Olaf Klinke wrote: > Paul, > > monads were not invented because I/O could not be presented in another > way in Haskell. Monads are way older than Haskell. It is a concept of > category theory which was developed in the 1950s. Actually some > concepts of algebra that are even older turn out to be monads. Take > Galois theory for example. Once you know the pattern, you find a monad > under every stone you turn around. It's one of the luckiest things > that people like Moggi and Wadler realized that monads can be applied > to structure programs. And don't blame them that monads are not > composable - it is simply a mathematical fact. Some monads do compose > with any other monad, and those are the monad transformers. > > If you like Prolog's relational programming model so much, then you > should play with those programs that have "no business value". Because > Haskell's type inference algorithm, together with multi-parameter type > classes and maybe type level natural numbers together give rise to > Prolog-like capabilities. All the work is done by the compiler this way. > > What you say about FSM is certainly true to some extent - they are > well understood, can be generated automatically, and there is decent > theory to reason about them. That is why this model is used in > safety-sensitive environments such as aviation. I once applied for a > position in verification in the automotive industry, and the interview > partner told me that they struggle mightily with the vast state spaces > of the FSMs they are checking. > All this speaks in favour of Haskell. The semantics is simple and > beautiful, because it is a single-paradigm language. And because of > that, clever people can leverage theorem provers to mathematically > prove correctness of Haskell code. I don't know of many languages > where that is possible. (But then, I'm not an expert on verification.) > > Olaf _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
https://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf
On 07/16/2018 02:56 AM, PY wrote: > Hello, Olaf! It's very good point. I'll read more about it. May be I'm > wrong, but I don't remember any monads in CT, so my suggestion was > that they were introduced in pure functional languages research (Hope, > Haskell), not math itself. May be I'm not right. Thanks a lot! > > > 15.07.2018 23:06, Olaf Klinke wrote: >> Paul, >> >> monads were not invented because I/O could not be presented in >> another way in Haskell. Monads are way older than Haskell. It is a >> concept of category theory which was developed in the 1950s. Actually >> some concepts of algebra that are even older turn out to be monads. >> Take Galois theory for example. Once you know the pattern, you find a >> monad under every stone you turn around. It's one of the luckiest >> things that people like Moggi and Wadler realized that monads can be >> applied to structure programs. And don't blame them that monads are >> not composable - it is simply a mathematical fact. Some monads do >> compose with any other monad, and those are the monad transformers. >> >> If you like Prolog's relational programming model so much, then you >> should play with those programs that have "no business value". >> Because Haskell's type inference algorithm, together with >> multi-parameter type classes and maybe type level natural numbers >> together give rise to Prolog-like capabilities. All the work is done >> by the compiler this way. >> >> What you say about FSM is certainly true to some extent - they are >> well understood, can be generated automatically, and there is decent >> theory to reason about them. That is why this model is used in >> safety-sensitive environments such as aviation. I once applied for a >> position in verification in the automotive industry, and the >> interview partner told me that they struggle mightily with the vast >> state spaces of the FSMs they are checking. >> All this speaks in favour of Haskell. The semantics is simple and >> beautiful, because it is a single-paradigm language. And because of >> that, clever people can leverage theorem provers to mathematically >> prove correctness of Haskell code. I don't know of many languages >> where that is possible. (But then, I'm not an expert on verification.) >> >> Olaf > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. signature.asc (499 bytes) Download Attachment |
In reply to this post by Paul
Nicely written. To add to this monad transformers are ... monads them selves! e.g. `StateT s` is left adjoint functor from the category of monads to the category of monads which satisfy the `MonadState s m` constraint, the right adjoin is a forgetful functor.
The essential parts of the proof are here: https://github.com/coot/free-algebras/blob/master/src/Control/Algebra/Free.hs#L273 Cheers, Marcin @me_coot on twitter ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On July 16, 2018 9:56 AM, PY <[hidden email]> wrote: > Hello, Olaf! It's very good point. I'll read more about it. May be I'm > > wrong, but I don't remember any monads in CT, so my suggestion was that > > they were introduced in pure functional languages research (Hope, > > Haskell), not math itself. May be I'm not right. Thanks a lot! > > 15.07.2018 23:06, Olaf Klinke wrote: > > > Paul, > > > > monads were not invented because I/O could not be presented in another > > > > way in Haskell. Monads are way older than Haskell. It is a concept of > > > > category theory which was developed in the 1950s. Actually some > > > > concepts of algebra that are even older turn out to be monads. Take > > > > Galois theory for example. Once you know the pattern, you find a monad > > > > under every stone you turn around. It's one of the luckiest things > > > > that people like Moggi and Wadler realized that monads can be applied > > > > to structure programs. And don't blame them that monads are not > > > > composable - it is simply a mathematical fact. Some monads do compose > > > > with any other monad, and those are the monad transformers. > > > > If you like Prolog's relational programming model so much, then you > > > > should play with those programs that have "no business value". Because > > > > Haskell's type inference algorithm, together with multi-parameter type > > > > classes and maybe type level natural numbers together give rise to > > > > Prolog-like capabilities. All the work is done by the compiler this way. > > > > What you say about FSM is certainly true to some extent - they are > > > > well understood, can be generated automatically, and there is decent > > > > theory to reason about them. That is why this model is used in > > > > safety-sensitive environments such as aviation. I once applied for a > > > > position in verification in the automotive industry, and the interview > > > > partner told me that they struggle mightily with the vast state spaces > > > > of the FSMs they are checking. > > > > All this speaks in favour of Haskell. The semantics is simple and > > > > beautiful, because it is a single-paradigm language. And because of > > > > that, clever people can leverage theorem provers to mathematically > > > > prove correctness of Haskell code. I don't know of many languages > > > > where that is possible. (But then, I'm not an expert on verification.) > > > > Olaf > > Haskell-Cafe mailing list > > To (un)subscribe, modify options or view archives go to: > > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > > Only members subscribed via the mailman list are allowed to post. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Free forum by Nabble | Edit this page |