casting in implementing gflist_vt_mergesort$cmp

Question

In gflist_vt.sats, the signature of gflist_vt_mergesort$cmp implies that the order used for sorting must be the same as that of stamp. I understand that if such comparing function is given, the soundness of the function is ensured.

In this example, gflist_vt_mergesort$cmp seems to be implemented using unsafe casting.

• Is it safe to do that? (i.e. Doesn't that cause any problem? e.g. What if the list is sorted multiple times with different ordering?)
• Is there any other (safer) way?

Answer 1

Unsafe casting is inherently unsafe.

Unsafe casting can be removed. In order to do so, you need to implement the abstract type stamped_vt0ype (which is given the alias stamped_vt). For instance, to sort an integer list in descending order, you could do something as follows:

local

assume stamped_vt0ype(_, i) = int(~i)

in (* in-of-local *)

implement
{a}
gflist_vt_mergesort$cmp(x, y) = g1int_sgn(y - x)

end // end of [local]

However, doing something like this does not seem to offer much in terms of practical programming.