Verhindern, dass SML-Typ zu eqtype wird, ohne Konstruktoren auszublenden

Question

In datatype Deklarationen wird Standard ML einen Gleichheitstyp erzeugen, wenn alle Typargumente für alle Varianten selbst eqtype s sind.

Ich habe in einigen Orten gesehen Kommentare die Unfähigkeit der Nutzer klagend ihre eigene Definition von Gleichheit zu schaffen und bauen ihre eigenen eqtypes und unerwartete Folgen der SML Regeln (zB blanke ref s und array s sind eqtypes, aber datatype Foo = Foo of (real ref) ist kein eqtype).

Quelle: http://mlton.org/PolymorphicEquality

man erwarten könnte der Lage sein, wirklich t vergleichen zwei Werte vom Typ, weil Zeiger Vergleich auf ref Zelle ausreichen würde. Leider kann das Typsystem nur ausdrücken, dass ein benutzerdefinierter Datentyp Gleichheit zulässt oder nicht.

Ich frage mich, ob es sich um Block eqtyping möglich ist. Sagen wir zum Beispiel, ich implementiere eine Menge als binären Baum (mit einer unnötigen Variante) und ich möchte die Fähigkeit verpatzen, Sätze strukturell miteinander zu vergleichen.

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

Sagen wir, ich will nicht Menschen in der Lage sein SetLeaf(5) und SetNode(5, EmptySet, EmptySet) mit = zu unterscheiden, da es eine Abstraktion brechender Betrieb ist.

Ich versuchte ein einfaches Beispiel mit datatype on = On | Off nur um zu sehen, ob ich den Typ zu einem Nicht-eqtype mit Signaturen degradieren könnte.

(* 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 

Es scheint, dass transparente Zuschreibung X.on davor ein eqType verhindern ausfällt, aber undurchsichtig Zuschreibung tut es zu verhindern. Diese Lösungen sind jedoch nicht ideal, da sie ein neues Modul einführen und die Datenkonstruktoren ausblenden. Gibt es eine Möglichkeit zu verhindern, dass ein benutzerdefinierter Typ oder Typkonstruktor zu einem eqtype wird oder Gleichheit zulässt, ohne seine Datenkonstruktoren zu verbergen oder neue Module einzuführen?

Answer 1

Kurze Antwort ist nein. Wenn die Definition eines Typs sichtbar ist, ist die Gleichung die Definition. Die einzige Möglichkeit, dies zu verhindern, besteht darin, die Definition so zu optimieren, dass beispielsweise kein Dummy-Konstruktor mit einem real-Parameter hinzugefügt wird.

Btw, kleine Korrektur: Ihr Typ foo sollte ein Gleichheits-Typ sein. Wenn Ihre SML-Implementierung dem nicht zustimmt, liegt ein Fehler vor. Ein anderer Fall ist real bar, wenn datatype 'a bar = Bar of 'a ref (was das MLton Handbuch diskutiert). Der Grund, dass der erste funktioniert, aber der zweite nicht, ist, dass ref in SML magisch ist: Es hat eine Form von polymorpher Gleichheit, die Benutzertypen nicht haben können.