Dafny模块系统与精化：跨抽象模块共享底层类型问询

我想实现（或近似实现）以下功能：让模块C复用模块A和B的逻辑，针对同一类型T进行操作。

初始尝试及类型不匹配错误 #

abstract module A {
  type T  
  function f(x:T) : nat   // A's operations on T
}

abstract module B {
  type T
  function f(x:T) : nat  // B's operations on T
}
 
// Reuse A and B for the same type T
abstract module C {
  import A : A
  import B : B
  type T
  function f(x:T) : nat { A.f(x) + B.f(x) }  // error: expected C.A.Abs.T, found C.T
}

在模块C中，Dafny将T、A.T与B.T视为完全不同的类型。虽然可以把C.T别名成其中某一个类型，但无法同时关联A.T和B.T。

尝试基模块继承方案 #

为了统一类型，尝试让A、B继承自同一个基模块：

abstract module BaseType {
    type T
}

abstract module A {
  import Base : BaseType
  function f(x:Base.T) : nat
}

abstract module B {
  import Base : BaseType
  function f(x:Base.T) : nat
}

abstract module C {
  import Base : BaseType
  import A : A
  import B : B
  function f(x:Base.T) : nat { A.f(x) + B.f(x) }
}

这个方案能解决类型统一的问题，但存在命名不友好的问题——所有操作都要通过Base.T来引用，无法直接用简洁的T。

尝试模块+Trait结合方案 #

由于Dafny的模块不可参数化，尝试结合模块与Trait来实现：

abstract module A {
  trait A<T> {
    static function f(x:T) : nat
  }
}

abstract module B {
  trait B<T> {
    static function f(x:T) : nat
  }
}

abstract module C {
  import A : A
  import B : B
  trait C<T> {
    static function f(x:T) : nat { A.A.f(x) + B.B.f(x) }
  }
}

这段代码可以编译，但必须将函数声明为static——否则需要实例化Trait才能调用成员。但Dafny不允许在精化模块中重写继承的静态方法，比如：

abstract module A2 refines A {
  trait A2<T> extends A<T> {
    // static function 'f' is inherited from trait 'A' and is not allowed to be re-declared
    function f(x:T) : nat { 0 } 
  }
}

这导致该方案无法用于实际的精化实现。如果改用非静态成员，又需要在模块C中创建A、B的实例，但Dafny不允许在模块内部用new创建实例，也无法在引理中使用new。

内容的提问来源于stack exchange，提问作者JosEduSol