You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Since it is often required in Erlang that two kinds of processes have the ability to actively start to send data to each other, it is desirable that modules can be mutually dependent.
In order to formalize a type system for recursive modules, it is not sufficient to introduce the mechanism of the forward declaration of signatures that will be assigned to recursive modules, because of the so-called double vision problem [Dreyer 2007]. Since the RMC type system [Dreyer 2007], MixML [Rossberg & Dreyer 2013], etc. remedy the problem, we can possibly utilize them as a basis of the type system for Sesterl.
However, it is never trivial how to extend RMC or MixML for handling the static interpretation [Elsman, Henriksen, Annenkov & Oancea 2018], which is a method for statically generating modules from functor applications; the mechanism of the static interpretation is crucial for Sesterl so that the resulting programs can be represented by Erlang modules.
(More explanation should be added here)
import rec BarServer
module FooServer :> sig
type proc
val notify<$a> : proc -> [$a]unit
...
end = struct
module Callback = struct
...
val handle_info(...) = act
... BarServer.notify(...) ...
/* sends data to a process that is working based on the `BarServer` module */
...
end
module Impl = GenServer.Make(Callback)
type proc = Impl.proc
val notify(p) = act
Impl.cast(p, ...)
...
end
import rec FooServer
module BarServer :> sig
type proc
val notify<$a> : proc -> [$a]unit
...
end = struct
module Callback = struct
...
val handle_info(...) = act
... FooServer.notify(...) ...
/* sends data to a process that is working based on the `FooServer` module */
...
end
module Impl = GenServer.Make(Callback)
type proc = Impl.proc
val notify(p) = act
Impl.cast(p, ...)
...
end
A minimal example case of double vision problem:
/* A.sest */
import rec B
module A :> sig
type u = B.u
type t :: o
val f : fun(t) -> {u, t}
end = struct
type u = B.u
type t = int
val f(x : t) : {u, t} =
let {y, z} = B.g (x + 3) in
/* Assume that the type system does not handle the double vision problem:
The type environment here tracks the fact `B.g : fun(A.t) -> {B.u, A.t}`
but cannot recognize that `A.t` equals `int`.
Therefore, a type error will occur here. */
{y, z + 5}
end
/* B.sest */
import rec A
module B :> sig
type t = A.t
type u :: o
val g : fun(t) -> {u, t}
end = struct
type t = A.t
type u = bool
val f(x : t) : {u, t} =
...
end
Bibliography
Derek Dreyer. A type system for recursive modules. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP’07), pp. 289–302, 2007.
Is this only a code organization limitation? Meaning, can't this run-time behavior be curently achieved when carefully splitting the message types (contract) and two GenServer implementations in additional modules?
edit: I've been staring at the example and indeed I don't have an immediate idea of how it could be split, so it could be an expresiveness limitation.
Since it is often required in Erlang that two kinds of processes have the ability to actively start to send data to each other, it is desirable that modules can be mutually dependent.
In order to formalize a type system for recursive modules, it is not sufficient to introduce the mechanism of the forward declaration of signatures that will be assigned to recursive modules, because of the so-called double vision problem [Dreyer 2007]. Since the RMC type system [Dreyer 2007], MixML [Rossberg & Dreyer 2013], etc. remedy the problem, we can possibly utilize them as a basis of the type system for Sesterl.
However, it is never trivial how to extend RMC or MixML for handling the static interpretation [Elsman, Henriksen, Annenkov & Oancea 2018], which is a method for statically generating modules from functor applications; the mechanism of the static interpretation is crucial for Sesterl so that the resulting programs can be represented by Erlang modules.
(More explanation should be added here)
A minimal example case of double vision problem:
Bibliography
The text was updated successfully, but these errors were encountered: