Testing Equality of two Datatypes

[Shahab Tasharrofi]

Hello there,

I want to write a code in ATS that uses a lot of object sharing (similar
to ROBDD's) and I need to be able to check if two references point
to the same memory location. For example if both x and y represent
formulas in ROBDD format, I want to check if x and y point to the
same memory location. If that is the case, I would know that:
x V y = x /\ y = x

If I have understood the underlying translations of ATS, the memory for
datatypes is allocated in the heap and what is passed to a function is
indeed a pointer to that memory location. My first question is if I have
understood this right?

So, I wrote a very small program in ATS to check if equality (in the
sense of pointing to the same location in memory) is defined over two
objects of the same datatype. My observation was that this is not the
case. My second question is if there is another function that I haven't
checked and that fulfills my purpose.

Now, assuming that the answer to my second question is negative, I
was thinking that I can use linear types to do what I want to do (because
they explicitly deal with location "l" that contains an object of type "a").
So, my third question is if this can indeed be done using linear types.
If so, my fourth question is if I can do something similar using
dataviewtypes as I prefer to avoid explicit referrals to memory locations.

Best regards,
Shahab

[gmhwxi]

Here is an example:

datatype foo = A of int | B of (string, foo)

extern
fun eqref_foo_foo (x: foo, y: foo); bool
overload == with eqref_foo_foo

staload UN = "prelude/SATS/unsafe.sats"

implement eqref_foo_foo (x, y) = ($UN.cast2ptr(x) = $UN.cast2ptr(y))

Note that '==' is only available in the up-to-date version of ATS2.

[gmhwxi]

Yes, a value of a datatype is a pointer to some heap location.

[Shahab Tasharrofi]

Okay, I see.