Monads because of I/O?
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
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
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.
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.h...
Cheers,
Marcin
@me_coot on twitter
‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On July 16, 2018 9:56 AM, PY
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.
participants (4)
-
Marcin Szamotulski -
Olaf Klinke -
PY -
Vanessa McHale