Zapobiegaj, by typ SML nie stawał się typem eqtype bez ukrywania konstruktorów.

Question

W deklaracjach datatype, Standard ML będzie generował typ równości, jeśli wszystkie argumenty typu dla wszystkich wariantów są same w sobie eqtype s.

Widziałem komentarze w kilku miejscach lamentować niezdolność użytkowników do własnej definicji równości i konstruować własne eqtypes i nieoczekiwane konsekwencje zasad SML (np nagie ref s i array s są eqtypes, ale datatype Foo = Foo of (real ref) nie jest typem eqty).

Źródło: http://mlton.org/PolymorphicEquality

można by oczekiwać, aby móc porównać dwie wartości typu rzeczywistym t, ponieważ porównanie wskaźnik na komórce ref wystarczy. Niestety, system typów może jedynie wyrazić, że typ danych zdefiniowany przez użytkownika dopuszcza równość lub nie.

Zastanawiam się, czy jest możliwe blok eqtyping. Załóżmy na przykład, że implementuję zestaw jako drzewo binarne (z niepotrzebnym wariantem) i chcę oddać możliwość strukturalnego porównywania zestawów ze sobą.

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

powiedzieć, że nie chcemy, aby ludzie mogli odróżnić SetLeaf(5) i SetNode(5, EmptySet, EmptySet) z = ponieważ jest to operacja abstrakcji łamanie.

Próbowałem prosty przykład z datatype on = On | Off tylko po to, aby zobaczyć, czy mogę zdegradować typ do nie-eqtype za pomocą podpisów.

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

Wydaje się, że przejrzyste przypisywanie nie zapobiega X.on od zostania eqtype, ale nieprzezroczyste przypisanie ma zapobiec. Jednak rozwiązania te nie są idealne, ponieważ wprowadzają nowy moduł i ukrywają konstruktory danych. Czy istnieje sposób, aby uniemożliwić konstruktorowi typu niestandardowego lub typu, aby stał się eqtype lub przyznać równości bez ukrywania swoich konstruktorów danych lub wprowadzania nowych modułów?

Answer 1

Krótka odpowiedź brzmi: nie. Gdy definicja typu jest widoczna, jego eq-ność jest zgodna z definicją. Jedynym sposobem, aby nie dopuścić do tego, że jest to eq, jest zmodyfikowanie definicji tak, aby nie było na przykład przez dodanie konstruktora fikcyjnego z parametrem real.

Btw, mała korekta: Twój typ foo powinien być typem równości. Jeśli twoja implementacja SML nie zgadza się, to ma błąd. Innym przypadkiem jest real bar, gdy datatype 'a bar = Bar of 'a ref (co omawia podręcznik MLton). Powód, dla którego pierwszy działa, ale drugi nie jest taki, że ref jest magiczne w SML: ma formę polimorphic eq-ness, której typy użytkowników nie mogą mieć.