Tony's Wiki

ocaml abstract signature

2 min read

OCaml’ abstract signatures, an incidental feature ? The challenge for understanding (and implementing) abstract signatures lies more in the meaning of the module-level polymorphism that they offer than the module level sealing,

More specifically, the crux lies in the meaning of the instantiation of an abstract signature variable A by some other signature S, that happens when a polymorphic functor is applied. OCaml follows an unrestricted syntactical approach: A can be instantiated by any (well-formed) signature S. During instantiation, all occurrences of A are just replaced by S ; finally, the resulting signature is re-interpreted—as if it were written as is by the user.

  • Syntactical rewriting in instantiation
    • creates different views for positive/negative positions ←> universal/existential implicit quantifiers

We should write:

module type UDPLib_expose' = sig
  module type CORE_UNSAFE
  include UDPLib with module type UNSAFE = sig
    module type CORE_UNSAFE = CORE_UNSAFE
    module Unsafe : CORE_UNSAFE
    module Safe : sig ... end
  end
end

instead of

module type UDPLib_expose = sig
  include UDPLib with module type UNSAFE =
    sig
      module type CORE_UNSAFE
      module Unsafe : CORE_UNSAFE (* this part remains abstract *)
      module Safe : sig ... end (* this part is exposed *)
    end
end

because unfolding UDPLib_expose, Reliable in UDPLib will be sig ... module type CORE_UNSAFE ... end

This means that the functor actually has to be polymorphic in the underlying implementation of CORE_UNSAFE, rather than using the internal details, which has the opposite meaning as before. If the user wants to hide a shared unsafe core, accessible to the functor when they were defined

  • Type in type issue

Abstract module types are impredicative: a signature containing an abstract signature can be instantiated by itself.

3 Solution: simple abstract signature

we propose to restrict the instantiation of abstract signatures by simple signatures: signatures that may contain abstract type fields but no abstract module-type fields.

Graph View