Referring to mutually recursive modules

Learning
1

I’ve been trying to write an OCaml version the free selective functors examples from @snowleopard’s Selective Applicative Functors paper and ran into problems when trying to write the ISA example.

Briefly, I have implemented Free as a functor, taking a module of effects Eff:

module Selective = struct
  module type S = sig
    include Applicative.S
    val select: ('a,'b) Either.t t -> ('a -> 'b) t -> 'b t
  end

  module Free = struct
    module type S = sig
       module Eff : sig
         type 'a t
         val map: 'a t -> f:('a -> 'b) -> 'b t
       end
 
       type _ t = 
         | Pure : 'a -> 'a t 
         | Select: ('a,'b) Either.t t * ('a -> 'b) Eff.t -> 'b t 
       
       include S with type 'a t := 'a t
     
       val lift: 'a Eff.t -> 'a t
    end

    module Make(Eff: sig type 'a t ... end) : S with module Eff := Eff = struct 
       ...
    end
  end
end

The example I am having problems with looks like this in Haskell:

type Program a = Select RW a
data RW a = 
  | Read Key (Value -> a)
  | Write Key (Program Value) (Value -> a) deriving Functor

The key point here is that our effects RW makes reference to Program and vice versa.

I tried to use recursive modules to do this in OCaml:

module rec Program : Selective.Free.S with module Eff := Eff = 
  Selective.Free.Make(Eff)

and Eff : sig
    type key = string
    type value = string
    type 'a t = 
      | Read of key * (value -> 'a)
      | Write of key * (value Program.t) * (value -> 'a)
    val map: 'a t -> f:('a -> 'b) -> 'b t
end = struct
    ...
end

But I get an error, Illegal recursive module reference from the the mention of Eff in the signature for Program.

Is there any way to write this program in OCaml?

1 Like
2

Can you upload your code somewhere for experimenting?

3

Of course: Sketch.sh - Interactive ReasonML/OCaml sketchbook

The example is at the very end of the sketch

4

The problem is with

module rec Eff : sig
  type 'a t = ...
  val map : ('a -> 'b) -> 'a t -> 'b t
end = struct .. end
and module Program : (S with Eff = Eff) = Make(Eff)

The module-checker considers that mentioning the recursively-defined Eff directly in the signature of Program is unsafe. I’m not sure why, but I think that it may come from the fact that Eff also has value components. In contrast, mentioning type components of Eff is safe, so the following works:

module rec Eff : sig
  type 'a t = ...
  val map : ('a -> 'b) -> 'a t -> 'b t
end = struct .. end
and module Program : (S with 'a Eff.t = 'a Eff.t) = Make(Eff)
3 Likes
5

Interesting; this seems to be the opposite of the ‘no safe modules’ problem I usually run into when tinkering with recursive modules i.e. a set of mutually recursive modules must go through at least one “safe” module in which all values have function types.

I’d wondered if this was coming from use of destructive substitution. Clearly I need to go and read the recursive module spec a bit more!

Thank you for taking a look at this and finding a working solution! I’ve updated the sketch with a working version using this approach if anyone wants to take a look.

1 Like