[erlang-questions] Erlang, mini-erlang, and TLA+
Jesper Louis Andersen
jesper.louis.andersen@REDACTED
Sat Oct 7 16:54:15 CEST 2017
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/838c53e2/attachment.htm>
More information about the erlang-questions
mailing list