Version française
Home     About     Download     Resources     Contact us    
Browse thread
Exceptions considered as values in recursive module typechecking?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Jérémie_Lumbroso <jeremie.lumbroso@e...>
Subject: Exceptions considered as values in recursive module typechecking?
Hello,

I am currently working on a project which I strive to make as modular,
flexible and abstract as I possibly can (the previous codebase was not
sufficiently abstracted, making some of the dependent components *too*
dependent insofar as they would often break with implementational
changes).

To this end, the recursive module typing system has been both a terrific
blessing and something of a bane: while it mostly allows me the freedom to
organize my modules in a clean, satisfying way, the "double vision"
problem (in particular, but not only) might have given me gray hair! But
the "double vision" problem is not what this message is about ...

While I think I have a good understanding of the "safe/unsafe" typing rule
for recursive modules (which is described in Xavier Leroy's introductory
paper), I am still specifically befuddled and frustrated by the
restriction on exceptions:

  <code>
  module type CLIENT =
  sig
    exception Error
  end

  module type HOST =
  sig
    module Client : CLIENT
  end


  module Client(Host : HOST) : CLIENT =
  struct
    exception Error
  end

  module rec Host : HOST =
  struct
    module Client = Client(Host)
  end
  </code>

OCaml's typechecker lets me know it cannot type my code because "Cannot
safely evaluate the definition of the recursively-defined module Host".  I
have a hunch (which I might as well call a certainty) that this is because
OCaml considers exceptions to be values ...


I would be interested to know why this is the case; and furthermore why
this was maintained in the context of recursive modules: it would seem to
me (but please correct me if I'm wrong) that the typing of exceptions in
recursive modules can never go jawry---or rather can never be "worse" than
those inconsistencies that can be written with types:

  <code>
  module rec A : sig type t end =
  struct
    type t = B of B.t
  end
  and B : sig type t end =
  struct
    type t = A of A.t
  end
  </code>

(Certainly, if the types were transparent, it would be possible to create
an infinite value with a "let rec".) I know that typing recursive modules
is a difficult problem, and I understand why it should be considered a
work in progress.

That said--is there a (clean, practical) way to circumvent this particular
problem? I like using exceptions a great deal, and the solutions I've come
up with (when a functor is not involved) are troublesome and ugly: I
create a separate, recursive module, with the exceptions; something like
this:

  <code>
  module rec MainModule1 : sig .. end =
  struct

    type t = ..
    ..

  end
  and MainModule2 : sig .. end =
  struct

    ..
    try
      ..
    with MM_Exceptions.Error a -> ...

  end
  and MM_Exceptions : sig exception Error of MainModule.t end =
  struct
    exception Error of MainModule.t
  end
  </code>

Finally, is there a hack I can apply to OCaml's code to get peace of mind?
I've awkwardly stumbled accross "translmod.ml" (in which I've located the
infamous Circular_dependency exception), but my attempts have not been
very successful, to the extent that I was only able to produce a version
of the typechecker that segfaults spectacularly ...

Best regards,

Jérémie