[erlang-questions] Erlang, mini-erlang, and TLA+

Sat Oct 7 17:16:34 CEST 2017

Jesper: many thanks again for taking time explaining the Monad concept in
this specific case and in general.

I found this module and I’ll try to play with it:
https://github.com/rabbitmq/erlando

/Frank

In this setting, Monads are used subtly different from the more "normal"
> setting, but I'll try to draw the connection anyway.
>
> When you are trying to formalize a programming language, there is a list
> of effectful constructions we may want to add to the language:
>
> * Exceptions or Process Crashes
> * State or the Process Dictionary
> * Communication patterns
> * Hibernation (or more generally: continuation constructs)
> * Non-deterministic computation
> * ...
>
> 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.
>
> 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!
>
> 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.
>
> 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".
>
> Hence our task, as formal semanticists, can now be changed and we can
> attack the problem in another way:
>
> 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.
>
> 2. Show that Exceptions, State, ... obeys the Monad laws.
>
> 3. Plug the things together to obtain a language which is extended with
> the effects of our desire.
>
> The hope is that dealing with 1 and 2 separately is easier than dealing
> with both at the same time.
>
> -------------------------
>
> 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.
>
> 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.
>
> [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.
>
> [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.
>
>
> On Sat, Oct 7, 2017 at 4:40 AM Frank Muller <frank.muller.erl@REDACTED>
> wrote:
>
>> Hi Jesper,
>>
>> 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.
>>
>> To me, It’s kind of magic word you say to impress people, and let them
>> think you know functional programming very well ��
>>
>> A simple, concrete example will be more than welcome.
>>
>> Thanks
>> /Frank
>>
>> Oct 6. 2017 at 20:08, Jesper Louis Andersen <
>> jesper.louis.andersen@REDACTED> wrote :
>>
>>> General rule when trying to build language cores formally:
>>>
>>> Every construction which can be written in terms of another construction
>>> should be.
>>>
>>> * ETS tables are really just processes
>>> * The Process dictionary is just a state monad in the language
>>> * You need monads for message passing side effects anyway, so you can
>>> probably reuse the work on top
>>> * The whole exception system can be cast inside the monad as well
>>> * Ports can be reimagined as special processes and you can use messaging
>>> in order to handle them
>>>
>>> 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.
>>>
>>>
>>> On Wed, Sep 27, 2017 at 7:20 AM Karlo Kuna <kuna.prime@REDACTED> wrote:
>>>
>>>> > No - write a new runtime but inspired by and stealing good bits from
>>>> the old
>>>>
>>>> what would you consider good bits here?
>>>>
>>>> i also suspect that mini erlang  would be better off without process
>>>> dictionaries?
>>>>
>>>>
>>>>
>>>> On Tue, Sep 26, 2017 at 10:59 PM, Joe Armstrong <erlang@REDACTED>
>>>> wrote:
>>>>
>>>>> On Tue, Sep 26, 2017 at 8:22 PM, Brady Powers <powers_brady@REDACTED>
>>>>> wrote:
>>>>> > If we're talking about a new instruction set,
>>>>>
>>>>> Yes
>>>>>
>>>>> > and removing pieces from the
>>>>> > runtime,
>>>>>
>>>>> No - write a new runtime but inspired by and stealing good bits from
>>>>> the old
>>>>>
>>>>> then are we still talking about a minimal Erlang,
>>>>> or are we talking
>>>>>
>>>>> It would be a subset of Erlang - so strictly not Erlang
>>>>>
>>>>> > about something new?
>>>>>
>>>>> Yes
>>>>>
>>>>>
>>>>> > Because I'm sure we could all think of thing's we'd change given the
>>>>> > opportunity. Joe's already written Erl2.
>>>>>
>>>>> No - erl2 just compiles to erl
>>>>>
>>>>> /Joe
>>>>>
>>>>> > -Brady
>>>>> > On Tuesday, September 26, 2017, 12:36:04 PM EDT, Joe Armstrong
>>>>> > <erlang@REDACTED> wrote:
>>>>> >
>>>>> >
>>>>> > On Tue, Sep 26, 2017 at 5:47 PM, Todd Greenwood-Geer
>>>>> > <t.greenwoodgeer@REDACTED> wrote:
>>>>> >> Hi,
>>>>> >>
>>>>> >> 1. Are there existing TLA+ specifications [1] for Erlang?
>>>>> >
>>>>> > Not that I know of.
>>>>> >
>>>>> >>
>>>>> >> Recent discussions regarding the behavior of messages for local and
>>>>> remote
>>>>> >> processes, the behavior of data in ETS, and the discussion about a
>>>>> new
>>>>> >> mini-erlang all make me think there would be great benefit in formal
>>>>> >> specifications of Erlang behaviors.
>>>>> >>
>>>>> >> For instance, I've been thinking about writing various widgets for
>>>>> >> distributed applications, each with a well defined TLA+
>>>>> specification, and
>>>>> >> then starting to compose larger and more interesting applications
>>>>> from
>>>>> >> them.
>>>>> >>
>>>>> >> My workflow would look like this:
>>>>> >> Write widget spec -> impl widget -> Write application spec
>>>>> (composed of
>>>>> >> previously spec'd widgets) -> impl application -> profit!
>>>>> >
>>>>> > Now sure about the profit bit at the end.
>>>>> >
>>>>> > (write crap, sell it, sell thousands of consulting hours to fix it =
>>>>> profit
>>>>> > :-)
>>>>> >
>>>>> >>
>>>>> >> The runtime behaviors such as message passing, process linking,
>>>>> etc. would
>>>>> >> be the first level that would need specifications... so has this
>>>>> ever been
>>>>> >> tackled?
>>>>> >
>>>>> > Years ago - but not in phase with the distribution.
>>>>> >
>>>>> > There has always been a bit of gap between reality (C code, and what
>>>>> > it does) and specifications (math, and what it should do). The two
>>>>> are
>>>>> > not the same.
>>>>> >
>>>>> >>
>>>>> >> 2. Regarding the mini-erlang, I'd really like to get involved in
>>>>> this
>>>>> >> project. Perhaps I should be replying to a separate thread, but my
>>>>> >> questions
>>>>> >> are:
>>>>> >
>>>>> > There is no project - just a few people discussion what they would
>>>>> like to
>>>>> > see
>>>>> > in a new system.
>>>>> >
>>>>> >
>>>>> >>
>>>>> >> * What are the goals of mini-erlang?
>>>>> >
>>>>> > My goal would be a tiny kernel - performance is
>>>>> > of secondary importance. Tiny run-time footprint.
>>>>> >
>>>>> >> * How are these goals different from Erlang?
>>>>> >
>>>>> > The current Erlang is not designed for a small memory footprint.
>>>>> >
>>>>> >> * What needs to be removed/added from Erlang to make mini-erlang?
>>>>> >
>>>>> > Remove NIFS binarys ets tables (possibly)
>>>>> >
>>>>> >> * What is the current VM instruction set, and what would be the Mini
>>>>> >> instruction set?
>>>>> >
>>>>> > Current is BEAM - Mini instruction set unknown.
>>>>> >
>>>>> >> (my reason for posing these questions in this thread)
>>>>> >> *** Is there any interest in modeling/specifying the behaviors
>>>>> prior to
>>>>> >> implementing?
>>>>> >
>>>>> > I dont' think so - the main problem is figuring out how to make
>>>>> something
>>>>> > with tiny footprint - so for example GC strategy and memory layout is
>>>>> > very important - I don't think modelling helps. Counting bytes on
>>>>> squared
>>>>> > paper
>>>>> > seems the best method (really)
>>>>> >
>>>>> >>
>>>>> >> Regarding implementation, I'm fairly agnostic. One thought is that a
>>>>> >> prototype could be written in anything (python, bash, java, go, c,
>>>>> etc.),
>>>>> >
>>>>> > I disagree - I'd like the final memory footprint to be small.
>>>>> > c (and friends) are OK but I don't want to have to include an entire
>>>>> JVM
>>>>> > (or whatever).
>>>>> >
>>>>> > Could implement it in Forth though ...
>>>>> >
>>>>> >> and once the design has settled down, then anyone should be able to
>>>>> go
>>>>> >> back
>>>>> >> and re-write in their language of choice. Should be fairly simple
>>>>> since
>>>>> >> there would be design docs, formal specifications, test suites,
>>>>> etc. Then
>>>>> >> we
>>>>> >> could have mini-erlang runtime competitions/shootouts ;-).
>>>>> >
>>>>> > That would be fun.
>>>>> >
>>>>> > Cheers
>>>>> >
>>>>> > /Joe
>>>>> >
>>>>> >
>>>>> >>
>>>>> >> [1] http://lamport.azurewebsites.net/tla/tla.html
>>>>> >> _______________________________________________
>>>>> >> erlang-questions mailing list
>>>>> >> erlang-questions@REDACTED
>>>>> >> http://erlang.org/mailman/listinfo/erlang-questions
>>>>> >
>>>>> > _______________________________________________
>>>>> > erlang-questions mailing list
>>>>> > erlang-questions@REDACTED
>>>>> > http://erlang.org/mailman/listinfo/erlang-questions
>>>>> _______________________________________________
>>>>> erlang-questions mailing list
>>>>> erlang-questions@REDACTED
>>>>> http://erlang.org/mailman/listinfo/erlang-questions
>>>>>
>>>>
>>>> _______________________________________________
>>>> erlang-questions mailing list
>>>> erlang-questions@REDACTED
>>>> http://erlang.org/mailman/listinfo/erlang-questions
>>>>
>>> _______________________________________________
>>> erlang-questions mailing list
>>> erlang-questions@REDACTED
>>> http://erlang.org/mailman/listinfo/erlang-questions
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20171007/013934e5/attachment.htm>