铸造实施 gflist_vt_mergesort$cmp

Question

在gflist_vt.sats中，gflist_vt_mergesort$cmp的签名意味着排序使用的顺序必须与stamp相同。我理解如果给出这样的比较函数，就保证了函数的健全性。

在 this example 中，gflist_vt_mergesort$cmp 似乎是使用不安全转换实现的。

• 这样做安全吗？ （也就是说，这不会造成任何问题吗？例如，如果列表以不同的顺序多次排序怎么办？）
• 还有其他（更安全）的方法吗？

Answer 1

不安全转换本质上是不安全。

可以删除不安全的转换。为此，您需要实现抽象类型 stamped_vt0ype（别名 stamped_vt）。例如，要按降序对整数列表进行排序，您可以执行以下操作：

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]

但是，做这样的事情在实际编程方面似乎并没有提供太多。