dafny - Dafny 中的类型约束：为二元关系类型实现“显示”

Question

我在 Dafny 中定义了一个多态二元关系类型（一个类）：

class binRel<S,T>

实际的声明是：

class binRel<S(!new,==),T(!new,==)>. 

我想添加一个新的类型约束：类型 S 和 T 应该实现“显示”操作（返回字符串）。

我对 Dafny 参考手册的阅读表明，Dafny 仅支持一些内置类型约束：==，并且显然是 !new，并且没有办法要求该类型支持，例如某些特定的 trait。

也许我错了，比参考手册更新的更新提供了这样的功能。我走运了吗？如果没有，是否有解决方法？

Answer 1

正确，Dafny 中只有几个内置类型约束。没有要求类型扩展特征的机制。

对于 Dafny 的面向对象/命令式片段，我不知道有什么好的解决方法。在纯片段中，您可以使用一流的函数来解决这个问题。

datatype MyPair<A,B> = MakePair(a: A, b: B)

type Show<!A> = A -> string

function ShowMyPair<A,B>(sa: Show<A>, sb: Show<B>): Show<MyPair<A,B>>
{
  (p: MyPair<A,B>) => "(" + sa(p.a) + "," + sb(p.b) + ")"
}