Prevent SML from becoming an eqtype without hiding constructors

Question

In declarations, datatype Standard ML will return an equality type if all type arguments for all variants are themselves eqtype s.

I saw comments in several places that regretted the inability of users to provide their own definition of equality and build their own excips and unexpected consequences of SML rules (for example, bare ref and array are eqtypes, but datatype Foo = Foo of (real ref) not equivalent).

Source: http://mlton.org/PolymorphicEquality

one would expect a comparison of two values ​​of type real t, since comparing the pointers on the ref cell would be sufficient. Unfortunately, a type system can only express that a user-defined data type allows equality or not.

I am wondering if eqtyping can be blocked. Say, for example, I implement a set as a binary tree (with an unnecessary option), and I want to defer the ability to structurally compare sets with each other.

 datatype 'a set = EmptySet | SetLeaf of 'a | SetNode of 'a * 'a set * 'a set; 

Say I don’t want people to be able to distinguish SetLeaf(5) and SetNode(5, EmptySet, EmptySet) with = , since this is an abstraction operation.

I tried a simple example with datatype on = On | Off datatype on = On | Off to see if I can change the type to non-eqtype using signatures.

 (* attempt to hide the "eq"-ness of eqtype *) signature S = sig type on val foo : on end (* opaque transcription to kill eqtypeness *) structure X :> S = struct datatype on = On | Off let foo = On end 

It seems that transparent assignment does not allow X.on to become an eqtype, but an opaque record forbids it. However, these solutions are not ideal because they introduce a new module and hide data constructors. Is there a way to prevent the creation of a type or type constructor from eqtype or allowing equality without hiding its data constructors or introducing new modules?

Answer 1

The short answer is no. When a type definition is visible, its value has the meaning that the definition implies. The only way to prevent its equality is to configure the definition so that it does not exist, for example, by adding a stub constructor with the real parameter.

Btw, a little correction: your foo type should be an equality type. If your SML implementation is not consistent with this, it has an error. Another case of real bar is when datatype 'a bar = Bar of 'a ref (this is what is discussed in the MLton manual). The reason the first and the second works is not because ref is magic in SML: it takes the form of a polymorphic equation that types of users cannot have.