[Haskell-cafe] Monads because of I/O?

[Marcin Szamotulski]

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 <aquagnu at gmail.com> 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.