Absolutely, this behavior is fully compliant with the Standard ML definition. The difference between your Option and List examples comes down to two key factors: how the standard OPTION and LIST signatures define their core types, and how opaque ascription (:>) processes those definitions.

Let’s break this down step by step:

1. Opaque Ascription 101 #

Opaque ascription (structure S :> Sig = Impl) acts like a "type firewall": it hides any details of Impl's types that aren’t explicitly declared in Sig. The critical rule here is:

• If Sig declares a type as generative (like type t or a plain datatype t = ... without a transparent binding), the resulting type in S becomes a brand-new abstract type—completely distinct from the original type in Impl.
• If Sig declares a type as transparent (like type t = s or datatype t = datatype s), the type in S stays exactly the same as Impl's type—no abstraction happens.

2. Why the Option Example Throws a Type Error #

The standard OPTION signature defines option as a generative datatype:

signature OPTION =
sig
  datatype 'a option = NONE | SOME of 'a
  (* ... helper functions like isSome, valOf ... *)
end

When you run structure O :> OPTION = Option;, the opaque ascription treats O.option as a new abstract type. Even though Option.option is the familiar built-in 'a option type, O.option is a separate, unrelated type in the type checker’s eyes.

That’s why O.NONE = Option.NONE fails: O.NONE has type ''a O.option, while Option.NONE has type 'a option—these are incompatible types, so the type checker rightfully rejects the comparison.

3. Why the List Example Returns true #

The standard LIST signature’s list type is tightly coupled to the built-in list type. The signature’s declaration datatype 'a list = nil | :: of 'a * 'a list exactly matches the definition of the global, built-in list datatype. The SML specification recognizes this as an implicit transparent binding—meaning the signature isn’t asking for a new generative type, just the existing built-in one.

So when you run structure L :> LIST = List;, L.list isn’t abstracted at all—it’s just a synonym for the standard 'a list type. Since L.nil and List.nil are both the same singleton value of 'a list, comparing them with = returns true.

Wrap-Up #

The key takeaway is that opaque ascription’s behavior depends entirely on the signature’s type declarations. OPTION uses a generative type that gets abstracted, while LIST uses a type tied directly to the built-in list that stays transparent. Poly/ML’s implementation here strictly follows the Standard ML rules.

内容的提问来源于stack exchange，提问作者isekaijin