<div><div dir="auto">Jesper: many thanks again for taking time explaining the Monad concept in this specific case and in general.</div><div dir="auto"><br></div><div dir="auto">I found this module and I’ll try to play with it:</div><div dir="auto"><a href="https://github.com/rabbitmq/erlando">https://github.com/rabbitmq/erlando</a><br></div><div dir="auto"><br></div><div dir="auto">/Frank</div><br><div class="gmail_quote"><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>In this setting, Monads are used subtly different from the more "normal" setting, but I'll try to draw the connection anyway.<div><br></div><div>When you are trying to formalize a programming language, there is a list of effectful constructions we may want to add to the language:</div><div><br></div><div>* Exceptions or Process Crashes</div><div>* State or the Process Dictionary</div><div>* Communication patterns</div><div>* Hibernation (or more generally: continuation constructs)</div><div>* Non-deterministic computation</div><div>* ...</div><div><br></div><div>The list goes on and also includes more "esoteric" constructions such as variables which has a certain value with a probability, quantum computations, computations where state flows in the reverse order of the program and so on.</div><div><br></div><div>If we add these constructions to a programming language and wish to formalize the language so we can prove theorems about it, then the language can easily become quite large very quickly. This hampers our proof-effort since we need to address the added complexity in all proofs we are doing. Exceptions will mean we have to address the concepts of "throw" and "handle". State will mean we have to address what "put" and "get" does and so on. More importantly, we will have to alter the whole semantics since now there are state and added control flow to keep track of!</div><div><br></div><div>But there is hope. A non-trivial insight is that all the above constructions have something in common. We can, so to speak, extract a more general notion of the above. This is good, because if we can prove something in generality, we can "plug in" the specifics--- exceptions, the state and so on---into our proof. We don't have to handle everything up front if this works out. The price is that the general notion might be harder to work with in the first place.</div><div><br></div><div>You can then ask: what should the rules of such a general notion be? It turns out mathematicians working in the area of Category Theory already had a definition which fit: the Monad. Remarkably, this creates a link, so to speak, between mathematics and programming languages. We can capture the above needed generality by observing that what they have in common are the "Monad Laws".</div><div><br></div><div>Hence our task, as formal semanticists, can now be changed and we can attack the problem in another way:</div><div><br></div><div>1. Show that we can add an abstract Monad to our language. Since the abstraction must hold for every possible monad, we are thus only allowed the use of the Monad Laws when dealing with proofs about the language.</div><div><br></div><div>2. Show that Exceptions, State, ... obeys the Monad laws.</div><div><br></div><div>3. Plug the things together to obtain a language which is extended with the effects of our desire.</div><div><br></div><div>The hope is that dealing with 1 and 2 separately is easier than dealing with both at the same time.</div><div><br></div><div>-------------------------</div><div><br></div><div>The other common use of a "Monad" is to embed effects into a pure language. This idea goes back to Moggi (I believe) and was popularized by Phil Wadler for Haskell[0]. Here the Monad acts like a stratification: computations are put into classes depending on what effects they have. E.g., "exceptions goes here", "io computation goes there" and so on. The key insight is that we can thus keep computations with effects apart from (pure) computations without. Even more interesting, because Haskell is a statically typed language, we can enforce that computations with different effects cannot accidentally be mixed in wrong ways. This helps with correctness.</div><div><br></div><div>What makes the monad construction hard to grasp initially is that it is an abstract notion in line with recursion. One has to work with it for a while to build up a certain amount of familiarity with the concept. This is also why it is so hard to explain: most tutorials are giving you a glimpse of the real deal through metaphor and analogy in the hope that it can make your mind think in the right way. But in reality it is just a definition of a mathematical object with certain laws. Why exactly *those* laws and not something else? Well it turned out that these laws were the useful ones[1]. Why the link to computer science? Because the universe is a remarkable place of systems.</div><div><br></div><div>[0] Phil's original paper is one of the best expositions of the idea and still to this day is one of the most readable.</div><div><br></div><div>[1] Mathematicians some times call such laws the "natural laws" in the sense that they afford you the most power from a perspective of using the definition as a building block for further work.</div><div><br></div></div><br><div class="gmail_quote"><div>On Sat, Oct 7, 2017 at 4:40 AM Frank Muller <<a href="mailto:frank.muller.erl@gmail.com" target="_blank">frank.muller.erl@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div dir="auto">Hi Jesper,</div><div dir="auto"><br></div><div dir="auto">Can you please enlighten me (Erlang newbie here) about this “Monad” things. I’ve heard this word multiple times and still can’t get it.</div><div dir="auto"><br></div><div dir="auto">To me, It’s kind of magic word you say to impress people, and let them think you know functional programming very well 😉</div><div dir="auto"><br></div><div dir="auto">A simple, concrete example will be more than welcome. </div><div dir="auto"><br></div><div dir="auto">Thanks</div></div><div><div dir="auto">/Frank</div></div><div><br><div class="gmail_quote"><div>Oct 6. 2017 at 20:08, Jesper Louis Andersen <<a href="mailto:jesper.louis.andersen@gmail.com" target="_blank">jesper.louis.andersen@gmail.com</a>> wrote :<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><div><div><div><div>General rule when trying to build language cores formally:<br><br></div>Every construction which can be written in terms of another construction should be.<br><br></div>* ETS tables are really just processes<br></div>* The Process dictionary is just a state monad in the language<br></div>* You need monads for message passing side effects anyway, so you can probably reuse the work on top<br></div>* The whole exception system can be cast inside the monad as well<br><div>* Ports can be reimagined as special processes and you can use messaging in order to handle them<br></div><div><br></div><div>The reason is that any construction is a formal liability: it needs special handling. It is often more beneficial to generalize the system a little bit in order to vastly simplify the number of cases you have to handle in proofs.</div><div><br></div></div><br><div class="gmail_quote"><div>On Wed, Sep 27, 2017 at 7:20 AM Karlo Kuna <<a href="mailto:kuna.prime@gmail.com" target="_blank">kuna.prime@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><span style="font-size:12.8px">> No - write a new runtime but inspired by and stealing good bits from the old<br><br></span></div><div><span style="font-size:12.8px">what would you consider good bits here? </span><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">i also suspect that mini erlang  would be better off without process dictionaries? <br><br> </span></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Sep 26, 2017 at 10:59 PM, Joe Armstrong <span><<a href="mailto:erlang@gmail.com" target="_blank">erlang@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Tue, Sep 26, 2017 at 8:22 PM, Brady Powers <<a href="mailto:powers_brady@yahoo.com" target="_blank">powers_brady@yahoo.com</a>> wrote:<br>
> If we're talking about a new instruction set,<br>
<br>
Yes<br>
<br>
> and removing pieces from the<br>
> runtime,<br>
<br>
No - write a new runtime but inspired by and stealing good bits from the old<br>
<br>
then are we still talking about a minimal Erlang,<br>
or are we talking<br>
<br>
It would be a subset of Erlang - so strictly not Erlang<br>
<br>
> about something new?<br>
<br>
Yes<br>
<br>
<br>
> Because I'm sure we could all think of thing's we'd change given the<br>
> opportunity. Joe's already written Erl2.<br>
<br>
No - erl2 just compiles to erl<br>
<br>
/Joe<br>
<br>
> -Brady<br>
> On Tuesday, September 26, 2017, 12:36:04 PM EDT, Joe Armstrong<br>
<div class="m_-2541772837381787424m_5834030080978501905m_-6030591991380073923m_-8569760955391645807HOEnZb"><div class="m_-2541772837381787424m_5834030080978501905m_-6030591991380073923m_-8569760955391645807h5">> <<a href="mailto:erlang@gmail.com" target="_blank">erlang@gmail.com</a>> wrote:<br>
><br>
><br>
> On Tue, Sep 26, 2017 at 5:47 PM, Todd Greenwood-Geer<br>
> <<a href="mailto:t.greenwoodgeer@gmail.com" target="_blank">t.greenwoodgeer@gmail.com</a>> wrote:<br>
>> Hi,<br>
>><br>
>> 1. Are there existing TLA+ specifications [1] for Erlang?<br>
><br>
> Not that I know of.<br>
><br>
>><br>
>> Recent discussions regarding the behavior of messages for local and remote<br>
>> processes, the behavior of data in ETS, and the discussion about a new<br>
>> mini-erlang all make me think there would be great benefit in formal<br>
>> specifications of Erlang behaviors.<br>
>><br>
>> For instance, I've been thinking about writing various widgets for<br>
>> distributed applications, each with a well defined TLA+ specification, and<br>
>> then starting to compose larger and more interesting applications from<br>
>> them.<br>
>><br>
>> My workflow would look like this:<br>
>> Write widget spec -> impl widget -> Write application spec (composed of<br>
>> previously spec'd widgets) -> impl application -> profit!<br>
><br>
> Now sure about the profit bit at the end.<br>
><br>
> (write crap, sell it, sell thousands of consulting hours to fix it = profit<br>
> :-)<br>
><br>
>><br>
>> The runtime behaviors such as message passing, process linking, etc. would<br>
>> be the first level that would need specifications... so has this ever been<br>
>> tackled?<br>
><br>
> Years ago - but not in phase with the distribution.<br>
><br>
> There has always been a bit of gap between reality (C code, and what<br>
> it does) and specifications (math, and what it should do). The two are<br>
> not the same.<br>
><br>
>><br>
>> 2. Regarding the mini-erlang, I'd really like to get involved in this<br>
>> project. Perhaps I should be replying to a separate thread, but my<br>
>> questions<br>
>> are:<br>
><br>
> There is no project - just a few people discussion what they would like to<br>
> see<br>
> in a new system.<br>
><br>
><br>
>><br>
>> * What are the goals of mini-erlang?<br>
><br>
> My goal would be a tiny kernel - performance is<br>
> of secondary importance. Tiny run-time footprint.<br>
><br>
>> * How are these goals different from Erlang?<br>
><br>
> The current Erlang is not designed for a small memory footprint.<br>
><br>
>> * What needs to be removed/added from Erlang to make mini-erlang?<br>
><br>
> Remove NIFS binarys ets tables (possibly)<br>
><br>
>> * What is the current VM instruction set, and what would be the Mini<br>
>> instruction set?<br>
><br>
> Current is BEAM - Mini instruction set unknown.<br>
><br>
>> (my reason for posing these questions in this thread)<br>
>> *** Is there any interest in modeling/specifying the behaviors prior to<br>
>> implementing?<br>
><br>
> I dont' think so - the main problem is figuring out how to make something<br>
> with tiny footprint - so for example GC strategy and memory layout is<br>
> very important - I don't think modelling helps. Counting bytes on squared<br>
> paper<br>
> seems the best method (really)<br>
><br>
>><br>
>> Regarding implementation, I'm fairly agnostic. One thought is that a<br>
>> prototype could be written in anything (python, bash, java, go, c, etc.),<br>
><br>
> I disagree - I'd like the final memory footprint to be small.<br>
> c (and friends) are OK but I don't want to have to include an entire JVM<br>
> (or whatever).<br>
><br>
> Could implement it in Forth though ...<br>
><br>
>> and once the design has settled down, then anyone should be able to go<br>
>> back<br>
>> and re-write in their language of choice. Should be fairly simple since<br>
>> there would be design docs, formal specifications, test suites, etc. Then<br>
>> we<br>
>> could have mini-erlang runtime competitions/shootouts ;-).<br>
><br>
> That would be fun.<br>
><br>
> Cheers<br>
><br>
> /Joe<br>
><br>
><br>
>><br>
>> [1] <a href="http://lamport.azurewebsites.net/tla/tla.html" rel="noreferrer" target="_blank">http://lamport.azurewebsites.net/tla/tla.html</a><br>
>> _______________________________________________<br>
>> erlang-questions mailing list<br>
>> <a href="mailto:erlang-questions@erlang.org" target="_blank">erlang-questions@erlang.org</a><br>
>> <a href="http://erlang.org/mailman/listinfo/erlang-questions" rel="noreferrer" target="_blank">http://erlang.org/mailman/listinfo/erlang-questions</a><br>
><br>
> _______________________________________________<br>
> erlang-questions mailing list<br>
> <a href="mailto:erlang-questions@erlang.org" target="_blank">erlang-questions@erlang.org</a><br>
> <a href="http://erlang.org/mailman/listinfo/erlang-questions" rel="noreferrer" target="_blank">http://erlang.org/mailman/listinfo/erlang-questions</a><br>
_______________________________________________<br>
erlang-questions mailing list<br>
<a href="mailto:erlang-questions@erlang.org" target="_blank">erlang-questions@erlang.org</a><br>
<a href="http://erlang.org/mailman/listinfo/erlang-questions" rel="noreferrer" target="_blank">http://erlang.org/mailman/listinfo/erlang-questions</a><br>
</div></div></blockquote></div><br></div>
_______________________________________________<br>
erlang-questions mailing list<br>
<a href="mailto:erlang-questions@erlang.org" target="_blank">erlang-questions@erlang.org</a><br>
<a href="http://erlang.org/mailman/listinfo/erlang-questions" rel="noreferrer" target="_blank">http://erlang.org/mailman/listinfo/erlang-questions</a><br>
</blockquote></div>
_______________________________________________<br>
erlang-questions mailing list<br>
<a href="mailto:erlang-questions@erlang.org" target="_blank">erlang-questions@erlang.org</a><br>
<a href="http://erlang.org/mailman/listinfo/erlang-questions" rel="noreferrer" target="_blank">http://erlang.org/mailman/listinfo/erlang-questions</a><br>
</blockquote></div></div></blockquote></div>
</blockquote></div></div>