Hello all,
In Haskell, when I declare the following type:
data Foo = MkFoo (Int, Bool)
the constructor "MkFoo" has a run-time cost: A pointer must be dereferenced whenever I pattern-match on MkFoo, and memory is allocated when I apply the MkFoo constructor.
On the other hand, if I declare this type:
newtype Foo = MkFoo (Int, Bool)
then the MkFoo constructor has no existence at run-time: Types Foo and (Int, Bool) have the same representation on the heap, and the MkFoo constructor function is a no-op.
Here's my question: When I declare a single-constructor datatype in Poly/ML, is it more like Haskell's "data" or "newtype"?
Here's the reason I'm asking: I'm thinking of using single-constructor datatypes to implement abstract types, by defining the datatype within the module, but not including the constructor function in the module signature. (This is exactly how people usually do abstract types in Haskell - just don't export the constructors.) I'd like to know if there are any pros or cons of this method compared to using abstype.
- Brian
Brian Huffman wrote:
Hello all,
In Haskell, when I declare the following type:
data Foo = MkFoo (Int, Bool)
the constructor "MkFoo" has a run-time cost: A pointer must be dereferenced whenever I pattern-match on MkFoo, and memory is allocated when I apply the MkFoo constructor.
On the other hand, if I declare this type:
newtype Foo = MkFoo (Int, Bool)
then the MkFoo constructor has no existence at run-time: Types Foo and (Int, Bool) have the same representation on the heap, and the MkFoo constructor function is a no-op.
Here's my question: When I declare a single-constructor datatype in Poly/ML, is it more like Haskell's "data" or "newtype"?
In Poly/ML a single constructor is the identity function so the answer is presumably that it's like "newtype" (I don't know Haskell).
Here's the reason I'm asking: I'm thinking of using single-constructor datatypes to implement abstract types, by defining the datatype within the module, but not including the constructor function in the module signature. (This is exactly how people usually do abstract types in Haskell - just don't export the constructors.) I'd like to know if there are any pros or cons of this method compared to using abstype.
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.
David
On Thu, Mar 4, 2010 at 9:46 AM, David Matthews David.Matthews@prolingua.co.uk 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
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
-
brianh＠cs.pdx.edu -
David.Matthews＠prolingua.co.uk