问题

I understand your code-related query. Here's the translated code portion:

我正在尝试引入一个参数化的子类型(`Bar<T(0)>` 如下)，需要我提供类型 `T` 的证明：
```dafny
datatype Foo<T> = Foo(x: T)
type Bar<T(0)> = x: Foo<T> | true witness ???

由于 T 是非空的，我不明白为什么这不可能。

我的尝试：

type Bar<T(0)> = x: Foo<T> | true witness Foo(*) // 错误：需要关闭括号
type Bar<T(0)> = x: Foo<T> | true witness Foo(var x: T := *; x) // 错误：无效的 UnaryExpression
type Bar<T(0)> = x: Foo<T> | true witness Foo(var x: T :| true; x) // 错误：为了可编译，let-such-that 表达式的值必须唯一确定

我猜想我可能可以编写一个函数、函数方法或方法来帮助，但在这里也失败了。一个方法可以用来获得任意的 T：

method Pick<T(0)>() returns (x: T)
{
}

但是 witness 子句需要一个函数方法，而 ghost witness 需要一个函数。在尝试在这两者中获取任意的 T 时，我得到了与我上面指出的错误相同的错误。在方法或函数方法中调用 Pick 也是不可能的。

我明白我可以指定 witness *，但这似乎更像是一个权宜之计而不是一个合适的解决方案。或者我不应该为此烦恼吗？

Please note that the "???" in the code represents the part where you were encountering difficulties, and it hasn't been resolved in the translation.

<details>
<summary>英文:</summary>

I am trying to introduce a parameterized subset type (`Bar&lt;T(0)&gt;` below) requiring me to provide a witness of type `T`:
```dafny
datatype Foo&lt;T&gt; = Foo(x: T)
type Bar&lt;T(0)&gt; = x: Foo&lt;T&gt; | true witness ???

Since T is non-empty, I don't see a reason why this should not be possible.

My attempts:

type Bar<T(0)> = x: Foo<T> | true witness Foo(*) // Error: closeparen expected
type Bar<T(0)> = x: Foo<T> | true witness Foo(var x: T := *; x) // Error: invalid UnaryExpression
type Bar<T(0)> = x: Foo<T> | true witness Foo(var x: T :| true; x) // Error: to be compilable, the value of a let-such-that expression must be uniquely determined

I speculated that I may be able to write a function, function method or method to help out, but failed here as well. A method can be used to obtain an arbitrary T:

method Pick<T(0)>() returns (x: T)
{
}

But a witness clause would require a function method while a ghost witness would require a function. When trying to obtain an arbitrary T in either of those, I get the same errors as the ones I pointed out above. Calling Pick in methods or function methods isn't possible either.

I understand that I can specify witness *, but this seems more of a hack than a proper solution. Or should I not be bothered by it?

答案1

得分: 2

@DivyanshuRanjan 在一个评论中回答了这个问题，我将尝试在这里进行总结。

以下内容有效：

type Bar<T(0)> = x: Foo<T> | true ghost witness Foo(var x: T :| true; x)

它有效是因为ghost见证不需要可编译，并且var x: T :| true; x是一个在函数中有效的表达式，即非编译的上下文。在非ghost见证子句中，验证器将拒绝此表达式并显示上述错误（"错误：为了可编译，let-such-that表达式的值必须唯一确定"）。

根据参考手册，ghost witness的缺点是"[Dafny验证器]将无法在编译的代码中自动初始化该类型的变量"。

以下内容无效：

type Bar<T(0)> = x: Foo<T> | true ghost witness Foo(var x: T := *; x)

根据参考手册，*是"右侧表达式"：
>右侧表达式是一种类似表达式的构造，可能具有副作用。因此，这种表达式只能在方法的某些语句中使用，而不能作为一般表达式或在函数或规范中使用。RHS要么是数组分配，要么是对象分配，要么是破坏右侧，要么是方法调用，要么是简单表达式，可选地后跟一个或多个属性。

我看不出var x: T := *; x与var x: T :| true; x有何不同（除了一个可在函数中使用，另一个不行）。希望将来可以改进这部分答案。

type Bar<T(0)> = x: Foo<T> | true ghost witness Foo(var x: T :| true; x)

type Bar<T(0)> = x: Foo<T> | true ghost witness Foo(var x: T := *; x)