SML: What's the difference between using abstype and using a signature to hide the implementation of a structure?

I've done a little work in SML in the past, but I'm now starting to get to the more interesting parts.

Using the abstype...with...end construct, I can make things but keep their implementation details hidden. I can also create a signature of the thing I want to make, and use the :> operator to make a structure adhering to that signature that keeps the implementation details hidden.

Aren't signatures/structures just a more general version of abstypes? What can I do with abstypes that I can't do with signatures/structures? Why would I ever want to use abstype?

Thanks in advance for the help!

As an example:

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

seems at least as powerful as

abstype AbsSet = absset of int list开发者_Python百科 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

Why would I ever want to use abstype?

Starting with the easiest, you won't. Atleast I can't come up with one good reason.

Aren't signatures/structures just a more general version of abstypes?

Well, I guess we have to take a look at the history of SML. The opaque (... :> ...) signature matching was not part of SML '90 as explained on this smlnj document about modules 1.3.9. opaque signature matching :>

... whose purpose was to create an "abstract" instance of the signature SIG. This feature was left out of SML '90 for various reasons, but the need for it was real.

I have no idea about the reasoning for not including it, but as far as I know McQueen was the "farther" of the abstype which was part of SML '90 and for some reason wasn't removed in SML '97 (maybe backwards compatibility?)

There is however a fundamentally difference between them, abstype is part of the core language where modules/signatures/functors are part of the module system.

What can I do with abstypes that I can't do with signatures/structures?

I can't come up with anything. However I'm pretty sure it would be easy to construct some example that you can using opaque signature matching and can't do with abstypes.

UPDATE

The page Degrade abstype to derived form from the successor-ml wiki actually contains a tiny informal description about abstype being a leftover.

As with many other, they also refer to the sections of the Defects in the Revised Definition of Standard ML paper which contains details about some "minor" errors/defects in the definition of abstype, although their link being dead. The "Revised Definition of Standard ML" is the definition of SML '97.

The one big reason why abstype is still required is for realistic applications is toplevel pretty printing. This refers to the intersection of SML/NJ and Poly/ML -- I don't know how Mlton works in this respect (it does not have a proper toplevel).

The task is simple: define an abstract datatype (one that does not leak equality) and provide a toplevel pretty printer for it. The only (quasi-portable) answer that I know uses plain-old abstype with SML'90-style non-opaque signature matching:

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 should print {42}[1] in this funny example -- the compiler specific lines need to be un-commented. This is definitely outside the SML'97 standard, or later attempts at ML'2000 and beyond, but it works both for SML/NJ and Poly/ML, as they are still available today. In some sense you see some older SML'90 and pre-SML culture shining through, even a bit of LISP toplevel hacking. (The above post-ludes to the structure definition can be turned into funny wrappers that invoke the SML toplevel at compile time in a way that works for both, thus making the sources appear portable.)

Note that for applications like Isabelle, HOL4, ProofPower, toplevel ML pretty printing is indispensible, whatever SML standard writers might say.

Here are two more versions that are more in line with SML'97 and opaque signature matching :> but fail to work uniformly:

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));
*)

I hope that I've got all the odd cases right. The "no pp" sitation is different for different SMLs: Poly/ML prints the original representation, while SML/NJ prints nothing (just a dash as place holder). The "untagged" opaque type is particularly nasty: in Poly/ML it will override the pretty-printer for int, but for SML/NJ it does just nothing, which is also bad.