4 ms·
As far as I'm aware there are a few major problems with static typing in Erlang that can't be solved so far and are not solved here either: 1. If you have a fu
by filmor 6y ago
As far as I'm aware there are a few major problems with static typing in Erlang that can't be solved so far and are not solved here either:
1. If you have a function that calls into other modules like `other_module:some_func(X)`, then the typing of this call can change at runtime. You could first have
some_func(N) when is_number(N) -> N + 1.
and later load a new version with
some_func(N) when is_integer(N) -> N + 1.
The older version accepts all numbers, i.e. floats and integers, while the second only accept integers.
2. Erlang message passing can not be typed statically in a meaningful (i.e. non-trivial) way, as the typing may be state-dependent:
Pid = spawn_link(fun () ->
receive
first -> ok;
_ -> error(bad_message)
end,
receive
second -> ok;
_ -> error(bad_message)
end
end)
Now, the static typing of sending to `Pid` depends on what you've sent before. This could maybe be handled by "enumerating" the receives, but I think that invites the halting problem into your type system.
- mikhailfranco 6y agoThe 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.