[Haskell-cafe] Monads because of I/O?
Marcin Szamotulski
profunctor at pm.me
Thu Jul 19 18:16:24 UTC 2018
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.
More information about the Haskell-Cafe
mailing list