Monads because of I/O?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Monads because of I/O?

Olaf Klinke
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.
Reply | Threaded
Open this post in threaded view
|

Re: Monads because of I/O?

Paul
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.
Reply | Threaded
Open this post in threaded view
|

Re: Monads because of I/O?

Vanessa McHale
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
Reply | Threaded
Open this post in threaded view
|

Re: Monads because of I/O?

Haskell - Haskell-Cafe mailing list
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.