SML: Qual è la differenza tra l'uso dell'abstype e l'utilizzo di una firma per nascondere l'implementazione di una struttura?

Question

Ho fatto un po 'di lavoro in SML in passato, ma ora sto iniziando a raggiungere le parti più interessanti.

Utilizzando il costrutto abstype...with...end, posso fare le cose ma mantenere nascosti i loro dettagli di implementazione. Posso anche creare una firma della cosa che voglio creare e usare l'operatore :> per fare in modo che una struttura aderisca a quella firma che mantenga nascosti i dettagli di implementazione.

Non sono le firme/strutture solo una versione più generale di abstypes? Cosa posso fare con gli abstypes che non posso fare con firme/strutture? Perché dovrei voler usare l'abstype?

Grazie in anticipo per l'aiuto!

Per fare un esempio:

signature SET = sig 
    type set 
    val empty: set 
    val insert: int * set -> set 
    val member: int * set -> bool 
end 

structure Set :> SET = struct 
    type set = int list 
    val empty = [] 
    fun insert(x, s) = x::s 
    fun member(x, []) = false 
     | member(x, h::t) = (x = h) orelse member(x, t) 
end 

sembra almeno altrettanto potente come

abstype AbsSet = absset of int list with 
    val empty = absset([]) 
    fun insert(x, absset(s)) = absset(x::s) 
    fun member(x, absset([])) = false 
     | member(x, absset(h::t)) = (x = h) orelse member(x, absset(t)) 
end 

Answer 1

Perché mai dovrei voler utilizzare abstype?

A partire dal più semplice, non lo sarà. Almeno non riesco a trovare una buona ragione.

---

Sono senza le firme/strutture solo una versione più generale di abstypes?

Bene, suppongo che dobbiamo dare un'occhiata alla storia di SML. L'opaco (...:> ...) firma corrispondente non faceva parte del SML '90 come spiegato in questo documento smlnj sui moduli 1.3.9. opaque signature matching :>

... il cui scopo era quello di creare un'istanza "astratto" di la firma SIG. Questa funzione è stata lasciata fuori da SML '90 per vari motivi, ma la necessità era reale.

mi hanno alcuna idea circa la motivazione per non aver compreso, ma per quanto ne so McQueen è stato il "più" del abstype che faceva parte della SML '90 e per qualche motivo non è stato rimosso in SML '97 (forse retrocompatibile?)

Esiste tuttavia una differenza fondamentale tra loro, abstype è parte del linguaggio principale in cui i moduli/firme/funtori fanno parte del sistema del modulo.

---

Cosa posso fare con abstypes che non posso fare con le firme/strutture?

Non riesco a trovare nulla. Tuttavia sono abbastanza sicuro che sarebbe facile costruire qualche esempio che si possa usare la corrispondenza delle firme opache e non si possa fare con gli abstypes.

---

UPDATE

La pagina Degrade abstype to derived form dal wiki-successore ml contiene in realtà una piccola descrizione informale su abstype essere un residuo.

Come molti altri, fanno riferimento anche alle sezioni della carta Defects in the Revised Definition of Standard ML che contiene dettagli su alcuni errori/difetti "minori" nella definizione di abstype, sebbene il loro collegamento sia morto. La "Revised Definition of Standard ML" è la definizione di SML '97.

Answer 2

L'unico grande motivo per cui lo abstype è ancora necessario è che per le applicazioni realistiche è sufficiente la stampa. Questo si riferisce all'intersezione tra SML/NJ e Poly/ML - Non so come funziona Mlton in questo senso (non ha un buon livello).

Il compito è semplice: definire un tipo di dati astratto (uno che non perde l'uguaglianza) e fornire una stampante abbastanza carina per questo. L'unica (quasi-portatile) risposta che so che usa plain-old abstype con stile SML'90 non opachi firma abbinamento:

structure A1: 
sig 
    type t val a: t val b: t -> t val print: t -> string 
end = 
struct 

abstype t = A of int 
with 
    val a = A 42 
    fun b (A i) = A (i + 1) 
    fun print (A i) = "{"^Int.toString i^"}[1]" 
end 

end; 

(* works for Poly/ML 5.3, 5.4, 5.5: 
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => PolyML.PrettyString (A1.print x)); 
*) 

(* works for SML/NJ 110.xx: 
CompilerPPTable.install_pp ["A1", "t"] (fn pps => fn x => PrettyPrint.string pps (A1.print x)); 
*) 

A1.a dovrebbe stampare {42}[1] in questo esempio divertente - le linee specifiche compilatore bisogno essere non commentato Questo è decisamente al di fuori dello standard SML'97, o tentativi successivi a ML'2000 e oltre, ma funziona sia per SML/NJ che per Poly/ML, poiché sono ancora disponibili oggi. In un certo senso, si vedono alcune vecchie SML'90 e una cultura pre-SML che sfolgorano, persino un po 'di hacking toplevel di LISP. (I precedenti post-ludi alla definizione della struttura possono essere trasformati in buffi wrapper che invocano la SML in fase di compilazione in un modo che funziona per entrambi, rendendo così le sorgenti comparse.)

Nota che per applicazioni come Isabelle , HOL4, ProofPower, toplevel ML la stampa carina è indispensabile, qualunque cosa possano dire gli scrittori SML standard.

Qui ci sono altre due versioni che sono più in linea con SML'97 e firma opaco corrispondenza :> ma non riescono a lavorare in modo uniforme:

structure A2 :> 
sig 
    type t val a: t val b: t -> t val print: t -> string 
end = 
struct 

datatype t = A of int 

val a = A 42 
fun b (A i) = A (i + 1) 
fun print (A i) = "{"^Int.toString i^"}[2]" 

(* works, but non-portable: 
val _ = 
    PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => PolyML.PrettyString (print x)) 
*) 

(* does not work (scope problem -- no pp): 
val _ = 
    CompilerPPTable.install_pp ["A2", "t"] (fn pps => fn x => PrettyPrint.string pps (A2.print x)); 
*) 

end; 

(* does not work (no pp): 
    PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => PolyML.PrettyString (A2.print x)); 
*) 

(* does not work (no pp): 
CompilerPPTable.install_pp ["A2", "t"] (fn pps => fn x => PrettyPrint.string pps (A2.print x)); 
*) 


structure A3 :> 
sig 
    type t val a: t val b: t -> t val print: t -> string 
end = 
struct 

type t = int 

val a = 42 
fun b i = i + 1 
fun print i = "{"^Int.toString i^"}[3]" 

(* does not work (overrides pp for int): 
val _ = 
    PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => PolyML.PrettyString (print x)) 
*) 

(* does not work (scope problem -- no pp) 
val _ = CompilerPPTable.install_pp ["A2", "t"] (fn pps => fn x => PrettyPrint.string pps (A2.print x)); 
*) 

end; 

(* works: 
    PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => PolyML.PrettyString (A3.print x)); 
*) 

(* does not work (no pp): 
CompilerPPTable.install_pp ["A3", "t"] (fn pps => fn x => PrettyPrint.string pps (A3.print x)); 
*) 

Spero che ho tutti i casi strani destra. La "no pp" è diversa per le diverse SML: Poly/ML stampa la rappresentazione originale, mentre SML/NJ non stampa nulla (solo un trattino come segnaposto). Il tipo opaco "non contrassegnato" è particolarmente sgradevole: in Poly/ML sovrascrive la pretty-printer per int, ma per SML/NJ non fa nulla, il che è anche negativo.