[erlang-questions] Looking for tricky protocol examples for verification research
Fri Oct 31 17:20:04 CET 2014
On 2014年10月31日 金曜日 11:14:15 you wrote:
> On Fri, Oct 31, 2014 at 12:47 AM, zxq9 <zxq9@REDACTED> wrote:
> > In other words, you want to define a contractual way that different
> > processes
> > can verify the external behavior of one another, instead of doing the
> > actor
> > version of duck typing that we tend to use all the time?
> It wouldn't be so much the processes verifying each other, but some
> overarching part of the runtime, or perhaps an analysis tool that verifies
> the "contract" for each process. Think of a type system: the type checker
> verifies that every function has the right type, and then a programmer who
> uses the function can be confident that the result of the function will be
> what they expect. I'm not saying I want to invent a type system, but I want
> to enable a similar style of reasoning for concurrent programs, where a
> programmer can just assume that another process acts in a certain way
> because that behavior is checked by another mechanism. Contracts in Racket (
> http://docs.racket-lang.org/guide/contracts.html) also enable this kind of
> reasoning, although with enforcement happening at run-time.
> I'm not sure what you mean by the "actor version" of duck typing, though.
> Could you expand on that, or point me towards an example?
In a duck typed language like Python we can treat anything as some type if it
implements the basic methods expected of that type. An outside process doesn't
need to care (sure we could introspect, but needing to is usually regarded as
a sign of using the wrong tool).
Erlang processes can be thought of the same way if we accept that in Erlang
"process" means something much closer to what languages like Python mean by
"object" than is commonly imagined. If I have a game character process it
might have an AI controller, or it might have a player controller. The
character process doesn't need to know or care, and we could actively swap out
AI for player control on the fly and the character process wouldn't care, so
long as all controllers, regardless of subtype (if we decide to use this term
"type"), adhere to the "controller" protocol.
Erlang lacks inheritance, so this talk of types is often limited to mean "a
particular sort of Erlang term()", but in some sense protocol definitions are
interface definitions that parallel duck typing very closely. This is true of
any network API as well, actually, hence the loose coupling enjoyed by network
components that communicate via bland protocols (as opposed to overly rich
ones nobody bothers to implement).
I think the main issue here is that most protocols internal to Erlang programs
are informally specified, if at all. The closest thing I see to a contract
system governing message protocols is Erlang behavior definitions. Come to
think of it, Erlang behavior definitions might be a good place look for
inspiration with regard to a message protocol contract system. They mandate
callback function definitions, but those callback functions are required to
adhere to certain protocol expectations which are handled directly
(received/emitted) by functions defined in the governing module of the
These modules could be seen as describing (but not defining on their own) a
message protocol that could be enforced by contract. Properly -spec'd
functions would contain the information needed in most cases, but there are
probably some weird edges there. The only ones necessary to evaluate would be
the ones mandated by the behavior module (in practice that is mostly true, but
this is not explicit -- it is not necessary that everything demanded by a
behavior be ultimately message related).
Blah. I wrote this thinking through it as I typed, so there's almost certainly
something ridiculous up there. But basically it should be possible to extend
behaviors or add something very similar to them that would do what you want.
The problem is that the compiler will care but not the runtime, and this is a
very different problem.
More information about the erlang-questions