On Thu, Mar 4, 2010 at 9:46 AM, David Matthews <[email protected]> wrote: > In Poly/ML a single constructor is the identity function
Thanks, that's exactly what I needed to know. > There's no difference in implementation between an abstype and a datatype. > "abstype" is a very old construction in Standard ML and predates the > modules system let alone the opaque signature matching of ML 97. It's > probably better on stylistic grounds to use signature matching to hide the > constructors but I don't think there's any difference in the underlying > implementation. Here's some more background to my question: I'm a regular contributor to Isabelle, and I've written some code that uses type-synonyms together with opaque ascription to make abstract types, like this: signature Foo = sig type T ... end; structure Bar :> Foo = struct type T = int * bool; ... end; For reasons related to pretty-printing (which, to be honest, I don't completely understand), other developers have determined that opaque ascription should be avoided in the Isabelle sources. So most uses of opaque ascription have now been replaced with "abstype", like this: structure Bar : Foo = struct abstype T = MkT of int * bool with ... end; end; But according to what you've said, the following code with "datatype" instead of "abstype" works in exactly the same way: structure Bar : Foo = struct datatype T = MkT of int * bool ... end; (and if I understand correctly, the "datatype" and "abstype" versions both work exactly like the original version with "type" and opaque ascription.) It seems that there is no advantage to using "abstype" over "datatype" in this situation: The only difference of "abstype" is the "with...end" block, which is redundant since "struct...end" already delimits the scope of the declaration. - Brian _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
