3 ms·
The stateful receive (2) just means that an Erlang process should be modelled as a state machine with some variety of automaton. Each receive blocks on a finite
by mikhailfranco 6y ago
The stateful receive (2) just means that an Erlang process should be modelled as a state machine with some variety of automaton. Each receive blocks on a finite ordered sequence of (possibly overlapping) pattern-matching expressions. The priority sequence means it behaves more like a PEG than an NDA or DFA.
Writing down the PEG message grammar for the process becomes quite easy. Pattern matching is well-defined. The number of states may be large, but can often be factored nicely by data types and ranges (e.g. tagged tuples). However, PEG semantics make it difficult to analyze composition of receive statements in the general case.
It's easy to solve the Halting Problem in Erlang - just add a timeout to your receive and accept some false positives :)
- filmor 6y agoThis is about static typing. I expect my static typing to terminate. Getting typing to work with a "screw this" fallback is already possible.
- mikhailfranco 6y agoHave a look at Erlang's success typing https://it.uu.se/research/group/hipe/papers/succ_types.pdf https://it.uu.se/research/group/hipe/papers/succ_types.pdf
- filmor 6y agoYes, that is the "screw-this-fallback" typing I was referring to... If it fails to prove a type for a value, it falls back to "this could be any type" which brings this part of the code back to pure dynamic typing.