[MLton] signature language lacking

[Vesa Karvonen]

On Feb 13, 2008 6:47 AM, Henry Cejtin <henry.cejtin at sbcglobal.net> wrote:
> Consider the following piece of SML code:
[...]
>         structure S: sig
>            structure A: sig
>               type t = S.at
>               val f: S.at -> S.bt
>            end
>            structure B: sig
>               type t = S.bt
>               val f: S.bt -> S.at
>            end
>         end = S
>
> Unless I am confused, the result is a structure S which has nothing in it but
> two sub-structures.  Each of these two sub-structures has only a single  type
> and a single function in it.  The two types are completely opaque except that
> the two functions map between them.
>
> My question is: is there any way to specify  a  signature  such  that  opaque
> matching  to that signature would express exactly this? [...]

I think you are quite right and the signature language is too weak to
express the desired signature.  Specifically, there is no way to refer
to (i.e. write the path to) the type defined in the second
substructure from the first substructure signature.  A "recursively
dependent signature", as described in

  A Type System for Recursive Modules.
  Derek Dreyer.
  http://ttic.uchicago.edu/~dreyer/papers/recmod/main-short.pdf

could express the desired signature.  It would look something like this:

  signature S = rec (X) sig
     structure A : sig
        type t
        val f : t -> X.B.t
     end
     structure B : sig
        type t
        val f : t -> X.A.t
     end
  end

Something like parameterized signatures with mutually recursive
substructure specifications could be another solution.  It could look
something like this:

  signature S' (type u) = sig
     type t
     val f : t -> u
  end

  signature S = sig
     structure A : S' (type u = B.t)
           and B : S' (type u = A.t)
  end

As your original post already showed, one can work around the problem
within SML'97 by introducing additional types in the signatures.  I
think that an idiomatic solution within SML'97 would be to specify all
the referred to types in the substructure signatures (making them self
contained) and tie the types together later using sharing constraints:

  signature S = sig
     structure A : sig
        type t
        type u
        val f : t -> u
     end
     structure B : sig
        type t
        type u
        val f : t -> u
     end
     sharing type A.t = B.u
     sharing type B.t = A.u
  end

Note that this can be further factored (by noting that A's and B's
signatures are self contained and the same) into:

  signature S' = sig
     type t
     type u
     val f : t -> u
  end

  signature S = sig
     structure A : S'
     structure B : S'
     sharing type A.t = B.u
     sharing type B.t = A.u
  end

-Vesa Karvonen