A trick to define abstract types without writing down module types

Learning
,
1

I was amused, perhaps surprised to see that you can define a module with an abstract type without writing down any module types using the following trick where you open an anonymous module (this is copy-pasted from the 5.3.0 toplevel except I prettified the code):

# module M = struct
    open (struct type aux = Newtype of int end)
    type t = aux
    let make n : t = Newtype n
  end;;
module M : sig type t val make : int -> t end

The annotation on make is essential:

# module M = struct
    open (struct type aux = Newtype of int end)
    type t = aux
    let make n = Newtype n
  end;;
Error: The type aux introduced by this open appears in the signature.
Line 1, characters 79-83:
  The value make has no valid type if aux is hidden.

So I’m guess I’m just putting this up for discussion. Useful trick? Horrible sorcery? Is this known (I couldn’t find a reference to it)? Is it even intended? Fwiw the fact the annotation changes the inferred signature feels intuitively “wrong” to me, at the point where you write : t the types t and aux ought to be fully interchangeable, and here they are not.

2

I never read someone write this kind of usage. They usually does:

module M : sig
  type t

  val make : int -> t
= struct
  type t = Newtype of int

  let make n = Newtype n
end

More clearer and concise to me.

Is it intended? I guess so, since the aux type and constructor only accessible inside module M. I see similar style generated by ppx, where they use

include struct ...
1 Like
3

Is this the kind of code that is cute while writing it but also the one that will you make scratch your head when code no longer compiles? I’d avoid it. Signatures are the language feature to model abstraction and navigating around them “looked like a good idea at the time” - but no longer.

1 Like
4

The core issue here is signature avoidance: there are some signatures that can be constructed in the module language but which cannot be written in the surface language. A more flagrant case would be

module N = struct
  include struct type t = A end
  type alias = t
  let x : alias = A
  type t = B
end

here if we try to write down the signature of N, we end up with the invalid signature

type t = A
type alias = t
val x: t
type t = B

because the type t can only be defined once in a given module.

For easy cases, the typechecker tries to rewrite such signature to avoid the issue by considering that:

  • type introduced by includes can be shadowed by local definitions
  • type definitions using the shadowed types can be made abstracts
  • type aliases can be used as alternatives names for shadowed types.

For instance, the signature of N can be rewritten to eliminate the shadowed type t

type alias
val x: alias
type t = B

However, this is quite brittle and dependent on user annotations. This is even more true if there are more than one types which are shadowed. Moreover, outside of the simplest cases, this is subject to changes in new version of language. There is some ongoing work to specify a more robust solution for signature avoidance, but this is not a high priority.

3 Likes
5

Interesting thanks. So this is neither a bug nor really specified to behave like this, it’s a known weird corner case. To be clear, I wasn’t really suggesting for people to use this in their code (as I said, the fact it depends on annotations gives me the ick, plus it’s not really practical to annotate every single use of the type in value definitions in the module).

I think I was inspired to try this by this comment and others where people use open struct and include struct tricks to avoid writing interfaces, it got me wondering if you can actually do this for the most obvious use case of interfaces, that is, abstract types. I was expecting it to be outright impossible to be honest.

6

I wouldn’t say that exactly.

There was at some point a proposal to add private items to ocaml’s structure and signature. This turned out to have a rather large amount of overlap with open struct ... end and in the end that last construction was added to the language (and the private items proposal was left behind).

You can find the discussion here but the tl;dr is: it is well known that open struct … end can be used to “hide” parts of a module implementation … and your example just builds upon that: you’re “exporting” an alias to a private/hidden item, so your alias is made abstract by the compiler (for the reasons laid out by @octachron).

2 Likes