sharing and where clauses

[RobertHarper]

I'm not sure of the current state of play, but the last I knew the syntax and semantics of structure sharing and structure realization was in a state of flux.

It seems to me, working from memory, that sharing and where should be about types. Sharing is a form of spec, and where is a form of sigexp. So, SIG where t = int would be a signature, for example, and type t type u sharing t=u is a form of spec.

Whether to allow "bulk" realization and sharing is questionable. I'm pretty sure the official definition is badly broken, and that compilers differ on what to do with them. Are these really all that important?

[YawarRaza7349]

I mean, yes, sharing is a spec and where is a sigexp modifier, but that's not the fundamental difference between them. Indeed, you can convert between specs and sigexps with sig (* spec *) end and include (* sigexp *) (which are inverses of each other), so this difference is rather inconsequential. The important difference, in what they are actually used for, is that where equates a type inside the signature to one outside the signature, whereas sharing equates multiple types inside a signature to each other.

Mechanically, this difference is actually solely about name lookup: whether the RHS(s) are looked up in the signature or in the surrounding scope. Interestingly, writing type specs in a signature itself follow normal shadowing rules instead:

signature FIN = sig
  type t = int (* from outside signature *)
  type u = t (* from inside signature *)
end

Now consider:

signature INIT = sig
  type t
  type u
end

Suppose you wanted to get from INIT to FIN using where and sharing. You can get type t = int using where, but you can't technically get type u = t because where can't reference the signature's t, and sharing gets the same effect, but is technically different. And of course, to even get this latter effect, you'd need to do the clunky sigexp to spec conversion I mentioned above:

signature ALMOST_FIN = sig
  include INIT
  sharing type t = u
end where type t = int

It could be convenient to add a (* sigexp *) with (* spec *) syntax meaning the same as sig include (* sigexp *); (* spec *) end. So the above could be written as:

signature ALMOST_FIN =
  INIT with sharing type t = u
  where type t = int