技术问询：Dafny内置Boolean operators为何无法作为first-class functions使用？

你踩中了Dafny一个常见的小坑——它确实不把内置布尔运算符（比如&&、||）当作一等函数。这些运算符是语法层面的特殊构造，不能直接作为值返回、赋值给变量或者当作函数参数传递。你遇到的编译错误，主要有两个核心原因：

1. 类型完全不匹配：你的evalOp函数声明的返回类型是bool -> bool（接受一个bool、返回bool的一元函数），但&&是二元运算符（需要两个bool参数），这种类型不匹配直接触发了"Invalid UnaryExpression"错误。
2. 语法不支持直接引用运算符：哪怕类型匹配，Dafny也不允许直接写&&作为函数值返回，必须显式把运算符包装成合法的函数形式。

修正后的代码示例 #

要解决这个问题，你需要用lambda表达式把内置运算符包裹起来，明确它的参数和返回值，同时修正返回类型为二元函数：

datatype binOp = X

// 返回类型改为 (bool, bool) -> bool，对应二元布尔函数
function evalOp(o: binOp): (bool, bool) -> bool {
    match o {
        case X => (a: bool, b: bool) => a && b
    }
}

扩展用法示例 #

如果需要支持更多二元布尔运算符，只需要扩展binOp枚举并添加对应的lambda包装即可：

datatype binOp = And | Or | Xor

function evalOp(o: binOp): (bool, bool) -> bool {
    match o {
        case And => (a, b) => a && b
        case Or => (a, b) => a || b
        case Xor => (a, b) => a != b
    }
}

这样修改后代码就能正常编译，你还可以像调用普通函数一样使用evalOp返回的函数值，比如：

method Main() {
    let andFunc := evalOp(And);
    assert andFunc(true, false) == false;
    
    let xorFunc := evalOp(Xor);
    assert xorFunc(true, true) == false;
}

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