[MLton] where and nj-deviations
Matthew Fluet
fluet@cs.cornell.edu
Thu, 1 Jan 2004 19:59:12 -0500 (EST)
I'm adding another nj-deviation, which is essentially a variation on the
where structure specification. To review, the MLton User Guide currently
says the following: (for convenience, I'm labeling the examples in
comments)
****
SML/NJ allows a where structure specification that is similar to a where
type specification. For example:
(* A *)
structure S = struct type t = int end
signature SIG =
sig
structure T : sig type t end
end where T = S
This is equivalent to:
(* B *)
structure S = struct type t = int end
signature SIG =
sig
structure T : sig type t end
end where type T.t = S.t
****
I want to add the following:
****
SML/NJ also allows a definitional structure specification that is similar
to a definitional type specification. For example:
(* C *)
structure S = struct type t = int end
signature SIG =
sig
structure T : sig type t end = S
end
This is equivalent to the previous examples and to:
(* D *)
structure S = struct type t = int end
signature SIG =
sig
structure T : sig type t end where type t = S.t
end
****
Now, the issue is that all of these examples may not be equivalent.
For example, SML/NJ rejects
(* E *)
structure S = struct type t = int end
signature SIG =
sig
structure T : sig type t end = S
end
where type T.t = S.t
with: "where type defn applied to definitional spec"
SML/NJ also rejects
(* F *)
structure S = struct type t = int end
signature SIG =
sig
structure T : sig type t end where type t = S.t
end
where type T.t = S.t
with: "where type defn applied to definitional spec"
On the other hand, MLton accepts (* F *). But, I'm fairly certain that
that is a bug, because MLton also accepts:
(* G *)
structure S = struct type t = int end
signature SIG =
sig
structure T : sig type t end where type t = S.t
end
where type T.t = bool
which clearly sends conflicting messages about the type of T.t.
However, SML/NJ accepts
(* H *)
structure S = struct type t = int end
signature SIG =
sig
structure T : sig type t end where type t = S.t
end
where T = S
which is arguably equivalent to (* F *) when one expands "where T = S"
by the equivalence of (* A *). But, SML/NJ rejects (* F *) and accepts
(* H *). There may also be a bug in SML/NJ, because it accepts
(* I *)
structure R = struct type t = bool end
structure S = struct type t = int end
signature SIG =
sig
structure T : sig type t end where type t = S.t
end
where T = R
which, like (* G *) seems to be claiming conflicting things about the type
of T.t.
In any case, I'm not sure whether SML/NJ's definitional structure
specifications can really be replicated with where and/or where type
constraints. (The analogy would seem to be that one cannot always replace
a definitional type specification with a where type constraint.) The
problem would seem that the "real" equivalent of (* C *) is
(* J *)
structure S = struct type t = int end
signature SIG =
sig
structure T : sig type t = S.t end
end
The "problem" with that is that if instead of (* C *) we started with:
(* K *)
signature T = sig type t end
structure S = struct type t = int end
signature SIG =
sig
structure T : T = S
end
then we still need to expand to (* J *), which requires replicating the T
signature in order to push the definitional specification to the type.