Mutually recursive modules

[gfngfn]

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.
• Martin Elsman, Troels Henriksen, Danil Annenkov, and Cosmin E. Oancea. Static interpretation of higher-order modules in Futhark: functional GPU programming in the large. In Proceedings of the ACM on Programming Languages 2, ICFP, Article 97, 2018.
• Andreas Rossberg and Derek Dreyer. Mixin’ up the ML module system. TOPLAS 35(1), 2013.

[michallepicki]

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.

[michallepicki]

This may or may not be of use to you (I stumbled upon it when looking for something else): Pauli Jaakkola A type system for first-class recursive ML modules and https://github.com/nilern/r1ml