如何在函数定义中使用forall？能否将全称量词作为函数输出？

• forall关键字的语法存在使用场景限制：在你使用的依赖类型语言（大概率是Idris系列）中，forall x . t的写法仅允许出现在顶层类型声明的签名位置，此时编译器会自动绑定x的作用域，因此你写的apple : forall x . x -> x可以正常运行。
• 当forall出现在普通表达式位置（也就是你给banana赋值的右侧）时，编译器默认不会把它识别为全称量词绑定语法，因此会认为x是需要从当前上下文获取的变量，而上下文没有定义x，就抛出了x is not accessible in this context的错误。
• 你写的{x : Type} -> x -> x是隐式Pi类型的标准表达式写法，本身就可以作为Type类型的值直接使用，和你预期的forall x . x -> x语义完全等价，因此可以正常运行。

如果你需要把带全称量词的多态类型作为值绑定输出，有两种可行方式：

1. 直接使用通用的隐式Pi语法（兼容性最好，所有依赖类型语言都支持）

banana : Type
banana = {x : Type} -> x -> x

这个写法和你预期的forall版本没有任何语义差异，后续使用时完全可以当做forall x. x -> x类型来用，示例：

-- 可以正常把恒等函数赋值给banana类型的变量
test : banana
test val = val

2. 部分语言支持给表达式中的forall加括号识别，如果你一定要用forall关键字，可以尝试：

banana : Type
banana = (forall x : Type . x -> x)

这种写法的兼容性不如隐式Pi语法，更推荐用第一种方案。

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