Impedisci al tipo SML di diventare eqtype senza nascondere i costruttori

Question

Nelle dichiarazioni datatype, ML standard produrrà un tipo di uguaglianza se tutti gli argomenti tipo di tutte le varianti sono essi stessi eqtype s.

ho visto commenti in alcuni posti lamentando l'incapacità degli utenti per fornire la propria definizione di uguaglianza e di costruire i propri eqtypes e conseguenze inattese delle regole SML (per esempio a nudo ref s e array s sono eqtypes, ma datatype Foo = Foo of (real ref) non è un eqtype).

Fonte: http://mlton.org/PolymorphicEquality

ci si potrebbe aspettare di essere in grado di confrontare due valori di tipo reale t, perché il confronto puntatore su una cella Rif sarebbe sufficiente. Sfortunatamente, il sistema di tipi può solo esprimere che un tipo di dati definito dall'utente ammette o meno l'uguaglianza.

Mi chiedo se sia possibile per blocco eqtyping. Per esempio, sto implementando un set come un albero binario (con una variante non necessaria) e voglio sfruttare la capacità di confrontare strutturalmente i set l'uno con l'altro.

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

dire che non voglio che la gente per essere in grado di distinguere SetLeaf(5) e SetNode(5, EmptySet, EmptySet) con = dal momento che è un'operazione di astrazione di rottura.

Ho provato un semplice esempio con datatype on = On | Off solo per vedere se potevo abbassare il tipo a un non-eqtype utilizzando le firme.

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

Sembra che ascription trasparente non riesce a impedire X.on divenga un eqtype, ma ascription opaca impedisce ad esso. Tuttavia, queste soluzioni non sono l'ideale perché introducono un nuovo modulo e nascondono i costruttori di dati. C'è un modo per evitare che un costruttore o tipo di costruttore personalizzato diventi un eqtype o ammetta l'uguaglianza senza nascondere i suoi costruttori di dati o l'introduzione di nuovi moduli?

Answer 1

Risposta breve no. Quando la definizione di un tipo è visibile, è eq-ness è qualsiasi cosa implichi la definizione. L'unico modo per evitare che sia l'eq è modificare la definizione in modo tale che non lo sia, ad esempio, aggiungendo un costruttore fittizio con un parametro real.

Btw, piccola correzione: il tipo foo deve essere un tipo di uguaglianza. Se la tua implementazione SML non è d'accordo, allora ha un bug. Un caso diverso è real bar quando datatype 'a bar = Bar of 'a ref (che è ciò che il manuale di MLton discute). Il motivo per cui il primo funziona ma il secondo no è che ref è magico in SML: ha una forma di eqnità polimorfa che i tipi di utenti non possono avere.