Re: Relation between Effects, Indexed monads, Free monads (PY)

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

Re: Relation between Effects, Indexed monads, Free monads (PY)

鲍凯文
Hi,

Disclaimer: I am not a lawyer. Nor do I claim to understand all this stuff.

The enforcement of sequential ordering is sort of baked into monads; the haskell (read: do-notation) way of combining monadic computations is using bind (i.e. in the "fancy list of instructions with a way to bind results"). This is only for the structure of the computation, though. Every monadic computation is still a pure function, so in the end the RTS, well, executes parts of those at a time, just as pure functions.

The ordering guarantee that more corresponds to imperative programming is most obvious (to me) with ST, IO, and State; data dependencies ensure that things "later" in the monadic chain cannot be executed until everything "before". But those effects all involve (mutable) state. Monadic chaining, i.e. combining effectful computations, is separate from the concept of mutable state, etc. It seems more like just an algebra for effects.

If you're talking about marked monads as in those with extra type information or phantom params, like when used in tandem with the rank-2 type trick (used in ST, region-based IO, etc.), I think that's a little different, or at least beyond what monads are. Those were created to handle things like guaranteeing that state is only modified single-threadedly (ST), or to ensure that you can't do things like forget to close a handle or leak a ref to a closed one (regions).

I think Free monads and (Kiselyov's) Eff monad are still different. They still appeal to the "monads as sequence of instructions" view, but uh, especially with the Eff monad, they're pretty fancy. As in at least personally, for "normal" programming, I haven't felt the need to delve into them.

I think the important upshot is: what are you working on? Do monadic computations model what you want to do naturally? If they do, do you need something stronger than what they provide? It's hard to answer the latter questions without answering the first.

Sorry for rambling,

toz

On Wed, Nov 15, 2017 at 4:00 AM, <[hidden email]> wrote:
Send Beginners mailing list submissions to
        [hidden email]

To subscribe or unsubscribe via the World Wide Web, visit
        http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
        [hidden email]

You can reach the person managing the list at
        [hidden email]

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."


Today's Topics:

   1.  Relation between Effects, Indexed monads,        Free monads (PY)


----------------------------------------------------------------------

Message: 1
Date: Wed, 15 Nov 2017 14:15:13 +0200
From: PY <[hidden email]>
To: [hidden email]
Subject: [Haskell-beginners] Relation between Effects, Indexed monads,
        Free monads
Message-ID: <[hidden email]>
Content-Type: text/plain; charset=utf-8; format=flowed

Hello, All!

I'm not sure is it question for Cafe or Beginners List, so first I'll
try here.

There are kind of errors related to wrong execution sequence. They are
good known in OOP: object keeps state internally and check it before to
execute got message - to prevent wrong execution sequence. Best
implementation is: state machine, also can be used Markov's algorithm,
more complex can be done with Petri nets, etc.

Example: if I have complex inserting into DB (consisting of several
inserts), I can check done of previous step before to start next, etc.
After read of different Haskell resources I found solution for it:
Indexed Monads. They (if I got it rightly) are monads with additional
type parameter which "marks" monad, gives it more specific
qualification, for example instead of monad "Opening" (action) we have
monad "Opening-of-closed", exactly what I'm talking: type-level check of
correct actions sequence (allowed transition).

After more research I found Free Monads and Effects and something like 
"free monad can be used to proof your program". How?! Free monads  make
"active" (executable) code into "passive" code (data instead of code),
which can be interpreted separately, so program becomes like Lisp
program: code is a data (so, can be modified, checked, etc, etc) and
what exactly will be executing - decides interpreter of such code. But
do they allow to proof right sequence of actions in such data-like code?

What are the Effects I don't understand yet.

Somewhere I find something like: Eff = Free Monad + indexed monad (may
be I'm not right here). So  my questions are:

- how Effects, Free Monad, Indexed Monads are related?

- can effects replace indexed monads?

- are indexed monad yet usable/modern concept or they are abandoned and
replaced by Effects or something else? Do you use indexed monads in real
projects?

- can I (and how) to use both of them? Or: can I use only FreeMonads /
Effects to solve the same problem (control of correct sequence of
actions) like with indexed monads help?


===

Best regards, Paul



------------------------------

Subject: Digest Footer

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


------------------------------

End of Beginners Digest, Vol 113, Issue 10
******************************************


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Baa
Reply | Threaded
Open this post in threaded view
|

Re: Relation between Effects, Indexed monads, Free monads (PY)

Baa

Hello, Toz,

I apologize for my little bit confused question. The root of my interest to such approaches is the situation when order is not possible to be done in one code fragment (such function under monad) because "ordered" steps should happens not immediately one after one, but with time gap, possible in different location of the program. For example, if you do:

  1. open file
  2. read data
  3. close file

all these actions are ordered and are located on time axis near one to one, happening immediately. But another case can be:

  1. insert info about class rooms
  2. do different things (may be exit application even)
  3. insert info about pupils

It's fictitious example and is targeting by RDBMS but this example is only to illustrate what I'm talking about. I found good example on SO with DVD control: https://stackoverflow.com/questions/28690448/what-is-indexed-monad

Also I found that indexed monads can be used to change type of the state "on the fly". So, for me, it's interesting to control allowed transitions between monad actions:

do
  action1
  action2
  -- action3 is denied because "action2 => action3" is denied transition/sequence
And I'm agree with you that Eff + Free monads looks different from this goal. But I found somewhere that Free monad can be used as proof assistance (there was some lecture on Youtube in Ljubljana university, but I can't find it more) and I'm thinking: may be it's possible to use Free monads for something similar like indexed monads? I found indexed free monads but such abstraction looks very complex and hard to me.

===
Best regards, Paul


16.11.2017 04:29, 鲍凯文 wrote:
Hi,

Disclaimer: I am not a lawyer. Nor do I claim to understand all this stuff.

The enforcement of sequential ordering is sort of baked into monads; the haskell (read: do-notation) way of combining monadic computations is using bind (i.e. in the "fancy list of instructions with a way to bind results"). This is only for the structure of the computation, though. Every monadic computation is still a pure function, so in the end the RTS, well, executes parts of those at a time, just as pure functions.

The ordering guarantee that more corresponds to imperative programming is most obvious (to me) with ST, IO, and State; data dependencies ensure that things "later" in the monadic chain cannot be executed until everything "before". But those effects all involve (mutable) state. Monadic chaining, i.e. combining effectful computations, is separate from the concept of mutable state, etc. It seems more like just an algebra for effects.

If you're talking about marked monads as in those with extra type information or phantom params, like when used in tandem with the rank-2 type trick (used in ST, region-based IO, etc.), I think that's a little different, or at least beyond what monads are. Those were created to handle things like guaranteeing that state is only modified single-threadedly (ST), or to ensure that you can't do things like forget to close a handle or leak a ref to a closed one (regions).

I think Free monads and (Kiselyov's) Eff monad are still different. They still appeal to the "monads as sequence of instructions" view, but uh, especially with the Eff monad, they're pretty fancy. As in at least personally, for "normal" programming, I haven't felt the need to delve into them.

I think the important upshot is: what are you working on? Do monadic computations model what you want to do naturally? If they do, do you need something stronger than what they provide? It's hard to answer the latter questions without answering the first.

Sorry for rambling,

toz

On Wed, Nov 15, 2017 at 4:00 AM, <[hidden email]> wrote:
Send Beginners mailing list submissions to
        [hidden email]

To subscribe or unsubscribe via the World Wide Web, visit
        http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
        [hidden email]

You can reach the person managing the list at
        [hidden email]

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."


Today's Topics:

   1.  Relation between Effects, Indexed monads,        Free monads (PY)


----------------------------------------------------------------------

Message: 1
Date: Wed, 15 Nov 2017 14:15:13 +0200
From: PY <[hidden email]>
To: [hidden email]
Subject: [Haskell-beginners] Relation between Effects, Indexed monads,
        Free monads
Message-ID: <[hidden email]>
Content-Type: text/plain; charset=utf-8; format=flowed

Hello, All!

I'm not sure is it question for Cafe or Beginners List, so first I'll
try here.

There are kind of errors related to wrong execution sequence. They are
good known in OOP: object keeps state internally and check it before to
execute got message - to prevent wrong execution sequence. Best
implementation is: state machine, also can be used Markov's algorithm,
more complex can be done with Petri nets, etc.

Example: if I have complex inserting into DB (consisting of several
inserts), I can check done of previous step before to start next, etc.
After read of different Haskell resources I found solution for it:
Indexed Monads. They (if I got it rightly) are monads with additional
type parameter which "marks" monad, gives it more specific
qualification, for example instead of monad "Opening" (action) we have
monad "Opening-of-closed", exactly what I'm talking: type-level check of
correct actions sequence (allowed transition).

After more research I found Free Monads and Effects and something like 
"free monad can be used to proof your program". How?! Free monads  make
"active" (executable) code into "passive" code (data instead of code),
which can be interpreted separately, so program becomes like Lisp
program: code is a data (so, can be modified, checked, etc, etc) and
what exactly will be executing - decides interpreter of such code. But
do they allow to proof right sequence of actions in such data-like code?

What are the Effects I don't understand yet.

Somewhere I find something like: Eff = Free Monad + indexed monad (may
be I'm not right here). So  my questions are:

- how Effects, Free Monad, Indexed Monads are related?

- can effects replace indexed monads?

- are indexed monad yet usable/modern concept or they are abandoned and
replaced by Effects or something else? Do you use indexed monads in real
projects?

- can I (and how) to use both of them? Or: can I use only FreeMonads /
Effects to solve the same problem (control of correct sequence of
actions) like with indexed monads help?


===

Best regards, Paul



------------------------------

Subject: Digest Footer

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


------------------------------

End of Beginners Digest, Vol 113, Issue 10
******************************************



_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners