SML/NJ error: type definition spec inside of sharing

[Florian Weimer]

The following snippet:

signature FOO =
sig
type foo
end

signature BAR =
sig
structure Foo : FOO
type bar = Foo.foo
end

functor Baz (structure Foo : FOO
structure Bar : BAR
sharing type Foo.foo = Bar.bar)
: sig end =
struct
end

gives this error message with SML/NJ 110.52-1 (the Debian package from
the unstable distribution):

help.sml:12.9-17.7 Error: type definition spec inside of sharing at: Foo.foo

MLton compiles the program just fine. Behavior with earlier SML/NJ
versions was apparently different. Is this a bug in SML/NJ?

(I'm asking because this is one of the things which prevents the ML
Kit from compiling with more recent SML/NJ versions.)

[Matthias Blume]

Post by Florian Weimer
signature FOO =
sig
type foo
end
signature BAR =
sig
structure Foo : FOO
type bar = Foo.foo
end
functor Baz (structure Foo : FOO
structure Bar : BAR
sharing type Foo.foo = Bar.bar)
: sig end =
struct
end
gives this error message with SML/NJ 110.52-1 (the Debian package from
help.sml:12.9-17.7 Error: type definition spec inside of sharing at: Foo.foo
MLton compiles the program just fine. Behavior with earlier SML/NJ
versions was apparently different. Is this a bug in SML/NJ?
(I'm asking because this is one of the things which prevents the ML
Kit from compiling with more recent SML/NJ versions.)

I am not quite sure of the exact reasoning behind it, but apparently
(according to Dave MacQueen) it makes sense to disallow the mention of
types for which there is a definitional spec in sharing specifications
or in "where type" clauses. In this case the offending type is
Bar.bar for which there is a definitional spec.

You can easily transform this code equivalently as follows, and it
will then compile:

functor Baz (structure Foo : FOO
structure Bar : BAR
sharing type Foo.foo = Bar.Foo.foo)
: sig end =
struct
end

Other possible rewrites are:

functor Baz (structure Bar : BAR
structure Foo : FOO where type foo = Bar.bar)
: sig end =
struct
end

and:

functor Baz (structure Foo : FOO
structure Bar : BAR where type Foo.foo = Foo.foo)
: sig end =
struct
end

Notice that the following modification of the last version does
not compile (for the same reason, namely that Bar.bar has a definitonal
spec):

functor Baz (structure Foo : FOO
structure Bar : BAR where type bar = Foo.foo)
: sig end =
struct
end

Cheers,
Matthias

[Florian Weimer]

Post by Matthias Blume
I am not quite sure of the exact reasoning behind it, but apparently
(according to Dave MacQueen) it makes sense to disallow the mention of
types for which there is a definitional spec in sharing specifications
or in "where type" clauses.

Is this a deliberate deviation from the Definition, or the result of
an ambiguity?

Post by Matthias Blume
functor Baz (structure Bar : BAR
structure Foo : FOO where type foo = Bar.bar)
: sig end =
struct
end
functor Baz (structure Foo : FOO
structure Bar : BAR where type Foo.foo = Foo.foo)
: sig end =
struct
end

Thanks, this should be helpful. I only knew about the first
workaround, and it doesn't seem to work in all cases (or I'm missing a
definitional spec somewhere).

By the way, it would be great if SML/NJ could point to exact place of
the violation, and not identify just the functor that is causing it.

[Andreas Rossberg]

Post by Florian Weimer

Post by Matthias Blume
I am not quite sure of the exact reasoning behind it, but apparently
(according to Dave MacQueen) it makes sense to disallow the mention of
types for which there is a definitional spec in sharing specifications
or in "where type" clauses.

Is this a deliberate deviation from the Definition, or the result of
an ambiguity?

It's not a deviation, it's what the Definition demands. In fact, the
Definition is even more restrictive about sharing specifications than
SML/NJ. Unfortunately, weakening these restrictions can quickly lead to
ambiguities or even undecidable type checking when parametric types are
involved. Consider:

type 'a t
type u = int t
type v = int
sharing type u = v

There are two incompatible choices: type 'a t = 'a, or type 'a t = int.
Finding a reliable and simple criterion for what to allow is not easy.
That's why "where" is usually considered the better alternative these
days, because it can be explained in terms of simple substitution
instead of unification.

- Andreas

[Florian Weimer]

Post by Andreas Rossberg

Post by Florian Weimer

Post by Matthias Blume
I am not quite sure of the exact reasoning behind it, but apparently
(according to Dave MacQueen) it makes sense to disallow the mention of
types for which there is a definitional spec in sharing specifications
or in "where type" clauses.

Is this a deliberate deviation from the Definition, or the result of
an ambiguity?

It's not a deviation, it's what the Definition demands. In fact, the
Definition is even more restrictive about sharing specifications than
SML/NJ.

Stephen Weeks disagrees, as you've might read. 8-)

Post by Andreas Rossberg
Unfortunately, weakening these restrictions can quickly lead to
ambiguities or even undecidable type checking when parametric types are
type 'a t
type u = int t
type v = int
sharing type u = v

I fail to see how this is related to my problem. The example I posted
does not use any types in the initial basis. I understand that some
concept of type rigidity is needed, and the the question is what
rigidity actually means, or more precisely: Given a flexible type
Foo.foo, is the type bar in

type bar = Foo.foo

also flexible?

I think the answer is yes. The BAR signature is equivalent to

signature BAR =
sig
structure Foo : FOO
include sig type bar
end where type bar = Foo.foo
end

The declaration of Foo.foo is flexible (according to (80)). (64)
preserves flexibility, so bar is flexible, too.

Comments?

[Andreas Rossberg]

Post by Florian Weimer
I fail to see how this is related to my problem. The example I posted
does not use any types in the initial basis. I understand that some
concept of type rigidity is needed, and the the question is what
rigidity actually means, or more precisely: Given a flexible type
Foo.foo, is the type bar in
type bar = Foo.foo
also flexible?
I think the answer is yes.

You are right. I hadn't studied your example careful enough. This
particular example should be accepted indeed.

On the other hand, I consider this rather an artifact of the way
"flexible" types are implemented in the Definition, and a more
"natural", syntactic way of tracking opaque types in the language
semantics would most likely exclude it (the internal use of which *may*
be the reason for NJ to complain about it). In favour of avoiding
obfuscation I would probably not rely on it anyway.

Cheers,

- Andreas

[Stephen Weeks]

Post by Florian Weimer
MLton compiles the program just fine. Behavior with earlier SML/NJ
versions was apparently different. Is this a bug in SML/NJ?

Yes, it is a bug in SML/NJ. In addition to your program being
accepted by MLton, it is also accepted by Hamlet, the ML Kit, Moscow
ML, and Poly/ML. Also, the Definition of Standard ML requires the
program to be accepted.

The behavior of SML/NJ is all the more bizarre (and incomprehensible)
since you can replace your definition of BAR with the following
equivalent signature (conceptually, as well as according to the
Definition) and SML/NJ will then accept your functor unchanged.

signature BAR =
sig
structure Foo : FOO
type bar
sharing type bar = Foo.foo
end