Problem with recursive modules?

[jonsterling]

@freebroccolo I don't really know how recursive modules work, but I think there is some problem; here is what happens in the toplevel (./script/top):

open TT.Tm.Chk;;
show (Pair (Dim0, Dim1));;

throws:

Exception: Undefined_recursive_module ("src/lib/Tm.ml", 32, 6).

Any ideas?

[jonsterling]

See https://github.com/ocaml-ppx/ppx_deriving/issues/142 and #5

[jonsterling]

I think one approach that might be more lightweight is to not put these big datatypes in their own modules, if they are mutually recursive. I'm not sure what the tradeoffs there are, but it might simplify things. Looks like in this case, ppx_deriving just generates functions like show_name instead of show.

[ghost]

Sorry about that undefined issue. I should have remembered that that shorthand only works when the modules consist purely of data declarations. Otherwise as you have discovered you must write out the structure as well.

[jonsterling]

No worries! Gave me a chance to learn more OCaml :)

On Feb 7, 2018, at 11:38 AM, Darin Morrison notifications@github.com wrote:

Sorry about that undefined issue. I should have remembered that that shorthand only works when the modules consist purely of data declarations. Otherwise as you have discovered you must write out the structure as well.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub, or mute the thread.

[ghost]

I think one approach that might be more lightweight is to not put these big datatypes in their own modules, if they are mutually recursive. I'm not sure what the tradeoffs there are, but it might simplify things. Looks like in this case, ppx_deriving just generates functions like show_name instead of show.

Yeah, this is really the only downside: the naming of the generated code just isn't as convenient.

[ghost]

Some additional thoughts on this now that I've had some coffee:

We could keep the recursive type definitions outside of a module, like how you have changed it to now, but then create essentially what are utility modules and then derive the instances within them instead of at the type declaration site. I think this would let us keep the nice module hierarchy and naming scheme but avoid most of the bureaucracy.

type chk =
  | Up of inf
  | Bool
  | Pi of chk * chk Bind.t
  | Sg of chk * chk Bind.t
  | Eq of chk Bind.t * chk * chk
  | Lam of chk Bind.t
  | Pair of chk * chk
  | Tt
  | Ff
  | Dim0
  | Dim1
  | U
and inf = 
  | V of Idx.t
  | App of inf * chk
  | Proj1 of inf
  | Proj2 of inf
  | If of chk Bind.t * inf * chk * chk
  | Down of chk * chk

module Chk = struct
  type t = chk = [%import: chk] [@@deriving (eq, ord, show)]
end

module Inf = struct
  type t = inf = [%import: inf] [@@deriving (eq, ord, show)]
end

[jonsterling]

this seems reasonable to me!

On Feb 7, 2018, at 1:04 PM, Darin Morrison notifications@github.com wrote:

Some additional thoughts on this now that I've had some coffee:

We could keep the recursive type definitions outside of a module, like how you have changed it to now, but then create essentially what are utility modules and then derive the instances within them instead of at the type declaration site. I think this would let us keep the nice module hierarchy and naming scheme but avoid most of the bureaucracy.

type chk = | Up of inf | Bool | Pi of chk chk Bind.t | Sg of chk chk Bind.t | Eq of chk Bind.t chk chk | Lam of chk Bind.t | Pair of chk chk | Tt | Ff | Dim0 | Dim1 | U and inf = | V of Idx.t | App of inf chk | Proj1 of inf | Proj2 of inf | If of chk Bind.t inf chk chk | Down of chk chk

module Chk = struct type t = chk = [%import: chk] [@@deriving (eq, ord, show)] end

module Inf = struct type t = inf = [%import: inf] [@@deriving (eq, ord, show)] end — You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub, or mute the thread.

[ghost]

So after digging around a bit I don't think the solution I proposed above is going to work:

1. [%import: …] requires that the types you are importing are from a different module, maybe even a different compilation unit. It might have worked close to how I have it above (within the same file) if I would have wrapped chk and inf in their own module but I didn't try. Needing to have separate Chk.ml and Inf.ml files starts to feel like too much bureaucracy though.

2. ppx_import doesn't currently work with jbuilder anyway.

I briefly tried switching the project back to ocamlbuild (which does work with ppx_import) and it worked (with the separate Chk.ml and Inf.ml) but ocamlbuild is somewhat difficult to use and prone to weird breakage issues that are hard to debug. Not worth it in my opinion.

I think the cppo (simple C-style preprocessor) approach mentioned in the issue you linked would be okay and this is supported with jbuilder:

#define MODULE(types) sig types end = struct types end

module rec TestMethod : MODULE(
  type t = A of int
  [@@deriving show]
)

So I think these are the realistic options for using recursive modules without the boilerplate. I don't think it's a big deal or anything if they aren't used, I just find the namespacing kind of nice. I'll go ahead and close this for now though.

[jonsterling]

@freebroccolo OK! Let's revisit it after I get the evaluator working in the way I want it to :) The style I've done right now isn't exactly what I want, but I need to try out several different ideas.