Minimal gen_server
When we started EXE we didn't know the landscape of ways we could implement interoperability with Erlang runtime. From the first, it seems reasonable to break all the compatibility and build the new world. But what about thinking of building reasonable type checked code that produces OTP compatible gen_server?
To show you that way we understand gen_server first we need to reimplement poor man's OTP-compatible gen_server in Erlang, by the way showing the session types and typed handler of gen_server.
We at Synrc are not using much OTP. First, we found that OTP principles, in general, are OK, but for simple services all those handle_call, handle_info necessary declarations seems a bit extra. We have irreplaceable application_controller, complicated user_drv layer, and more legacy stuff that prevent us from building modern and flexible functional codebase. E.g. we have the use case in mad for loading the application from escript bundle and ETS filesystem and even made a custom static handler for that purposes.
The reason to rethink OTP ideas is not only NIH syndrome. We also want to see minimal primitives to specify gen_server more formally in its distilled form. Others may take into account that this is toy sample.
Overview
The basic idea of gen_server is to be run and to be reacted during life-time to a series of ordered events. You may think of gen_server as simple stream data type of a given state and also typed with an effectfull process.
Boot Code
The very first gen_server in ERTS and LING is application_controller, that starts from init module. It starts even without proc_lib and enters gen_server loop manually.
NOTE: init message is our public version of ack. We use init for reinitialization even without stopping the process. But instead of gen_server for N2O protocols we use n2o_async interfaced with proc/2 message and state parameters.
-module(boot).
-compile(export_all).
start(App) ->
spawn_link(?MODULE, init, [self(), App]).
init(Parent, App) ->
process_flag(trap_exit, true),
self() ! {init,self(),{}},
loop(Parent, {local, ?MODULE}, {}, ?MODULE, infinity).
We can make it gen_server-compatible by placing two lines in init
put('$ancestors', [Parent]),
put('$initial_call', {application_controller, start, 1}),
Loop
Here is the hardest part for reasoning. We give computing control to Erlang VM which calls hibernate function in the gen_server module.
Hibernate, Infinity or Timeout:
loop(Parent, Name, State, Mod, hibernate) ->
erlang:hibernate(?MODULE,hibernate,[Parent, Name, State, Mod]);
loop(Parent, Name, State, Mod, Time) ->
server(drain(Time), Parent, Name, State, Mod).
Here is happened computational emptiness and all sources of effects.
You may think of receive as effectful suspended case.
drain() -> receive Input -> Input end.
drain(Timeout) -> receive Input -> Input
after Timeout -> {timeout,[],[]} end.
Wake up from Hibernate state here:
hibernate(P, N, S, M) -> server(drain(), P, N, S, M).
Session Types in EXE
Note that init is added by me, because it always needed a place for reinit without stopping the process.
data input (Any: Type): Type :=
(EXIT: Any -> Pid -> Record -> input Any)
(init: Any -> Pid -> Record -> input Any)
($gen_call: Any -> Pid -> Record -> input Any)
($gen_cast: Any -> Pid -> Record -> input Any)
(system: Any -> Pid -> Record -> input Any)
(timeout: Any -> Pid -> Record -> input Any)
(info: Any -> input Any)
data output (Any: Type): Type :=
(ok: Record -> output Any)
(ok: Any -> Record -> output Any)
(error: Atom -> output Any)
(stop: Atom -> Pid -> Record -> output Any)
Effects could be stored as persisted trace of ok and/or error events in KVS. We could allow process to continue on errors, etc.
Server
Loop is waiting for data in drain and pass it to Server which can handle only tuple/3 with following first elements: EXIT, timeout, system, $gen_call, $gen_cast, init. After receiving message the server will call appropriate function in a given sen_server module.
OTP reply is a tuple/2:
reply({To,Tag},Reply) -> To ! {Tag,Reply}.
server({Fun, Sender, Msg}, P, N, S, M) ->
try case M:Fun(Msg, Sender, S) of
{stop, Status, Tag, NS} -> reply(Tag,Status), Status;
{ok, Reply, NS} -> reply(Sender,Reply),
loop(P, N, NS, M, infinity);
{ok, NS} -> loop(P, N, NS, M, infinity) end
catch _:_ -> reply(Sender, {error,erlang:get_stacktrace() }) end;
There is a trick in OTP to handle Any messages built into protocol which is not good for reasoning. We will convert them to cast messages (or better deny totally).
server(Message,P,N,S,M) -> server({'$gen_cast',[],Message},P,N,S,M).
Callback Module
Here is new callback module, that eliminates gen_server behaviour callbacks, but allows raw protocol messages naming.
init(M,R,S) ->
{ok, State}.
timeout(M,R,S) ->
io:format("timeout: ~p~n",[{M,R,S}]),
{stop, timeout, {R,[]}, S}.
system(M,R,S) ->
io:format("system: ~p~n",[{M,R,S}]),
{stop, M, {R,[]}, S}.
'$gen_call'(M,R,S) ->
io:format("$gen_call: ~p~n",[{M,R,S}]),
{ok,R,S}.
'$gen_cast'(M,R,S) ->
io:format("$gen_cast: ~p~n",[{M,R,S}]),
{ok, S}.
'EXIT'(M,R,S) ->
io:format("EXIT: ~p~n",[{M,R,S}]),
{stop, M, {R,[]}, S}.
Callback Module in EXE
In general it is possible to compile such EXE record in OTP-compatible Erlang code.
record handler (M: Sigma) (P: Pid) (S: State) (A: Type): Type :=
(init := output.ok A S)
(timeout := output.stop A :timeout (prod P []) S)
(system := output.stop A M (prod P []) S)
($gen_call := output.ok A M S)
($gen_cast := output.ok A S)
Typed Free Structure can handle the stream.
data IOI.F (A,State: Type): Type :=
(receive: (input A → State) → IO.F)
(server: input A → State → IO.F)
(pure: A → IO.F)
data IOI (A,State: Type): Type :=
(intro: State → (State → IOI.F A State) → IOI)
Let's try!
1> boot:start(1).
<0.1564.0>
2> gen_server:call(pid(0,1564,0),hello).
$gen_call: {hello,{<0.1562.0>,#Ref<0.0.3.2620>},{}}
{<0.1562.0>,#Ref<0.0.3.2620>}
3> pid(0,1564,0) ! helo.
$gen_cast: {helo,[],{}}
helo
4> exit(pid(0,1564,0),normal).
EXIT: {normal,<0.1562.0>,{}}
true