Brian Huffman wrote:
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.
From the point of view of run-time representation of the values of the
datatype there is no difference between an abstype and a datatype and
across opaque or transparent signatures. There are differences in the
way pretty printing is handled; in particular there were changes between
different versions of Poly/ML. Also abstype removes the equality
attribute from the datatype. I would imagine that the Isabelle
maintainers are attempting to minimise the changes in the code between
the different versions of Poly/ML.
Regards,
David
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
