Haskell 函数中的类型量词答案

【问题标题】：Type quantifiers in Haskell functionsHaskell 函数中的类型量词
【发布时间】：2026-02-14 14:55:02
【问题描述】：

假设我有两个以下类型的 Haskell 函数，并激活了 ExplicitForAll，

f :: forall a. (a -> Int)
g :: forall a. (Int -> a)

在我看来g 的类型与Int -> (forall a. a) 同构，因为例如g(2) 的类型是forall a. a。

但是，f 的类型看起来与 (forall a. a) -> Int 不同。 f 是一个多态函数，它知道在每个输入类型上计算什么 a，在数学上我猜它宁愿是一个函数族；但我认为它不能处理具有所有类型的单个参数。

类型量词分布在函数目标类型而不是函数源类型上是类型化 lambda 演算的规则吗？

Haskell 中是否存在 (forall a. a) -> Int 类型，可能被限制为类型类 (forall a. SomeClass a => a) -> Int ？有用吗？

【问题讨论】：

不，它们不是同构的。是什么让你这么认为？
如果你碰巧熟悉范畴论，f :: forall a. F a -> G a 可以看成是在a 上自然的函数族：这是自然变换@ 987654334@（假设F,G 是函子，如本例所示）。
@n.m. g(2) :: forall a. a 不是一个充分的理由吗？
@chi 的确，我的问题源于自然变换，这就是我谈到函数族的原因。你知道当F 或G 是一个常量函子时，类型化的 lambda 演算是否有分配类型量词的规则？
类型量词可以与逻辑中的箭头交换：命题p -> forall a. q(a) 等价于forall a. p -> q(a)，前提是p 不依赖于a。如果 Haskell 有存在类型，我们就会有同构(forall a. p(a) -> q) ~ ((exists a. p(a)) -> q)。它也与产品通勤(forall a. p a, forall a. q a) ~ forall a. (p a, q a)。总和比较棘手。

标签： haskell lambda-calculus

【解决方案1】：

weird :: (forall a. a) -> Int 不必要地具体。

undefined 是唯一具有forall a. a 类型的值，因此定义必须是weird _ = someInteger，这只是const 的一个更严格的版本。

【讨论】：

使用类型类约束(forall a. SomeClass a => a) -> Int 怎么样？
@V.Semeria 在这种情况下，可能会找到已定义的参数。例如。如果SomeClass = Num，则42 :: Num a => a 是一个有效参数。

【解决方案2】：

∀ a . 基本上只是一个额外的隐式参数，或者更确切地说，是关于如何处理与该参数相关的类型约束的规范。例如，

f :: ∀ a . Show a => (a -> Int)
g :: ∀ a . Show a => (Int -> a)

本质上是两个参数的函数，

f' :: ShowDictionary a -> a -> Int
g' :: ShowDictionary a -> Int -> a

甚至更笨，

type GenericReference = Ptr Foreign.C.Types.Void -- this doesn't actually exist

f'' :: (GenericReference -> String) -> GenericReference -> Int
g'' :: (GenericReference -> String) -> Int -> GenericReference

现在，这些只是单态（或弱动态类型）函数。我们可以清楚地在他们身上使用flip来获取

f''' :: GenericReference -> (GenericReference -> String) -> Int
g''' :: Int -> (GenericReference -> String) -> GenericReference

后者可以简单地使用任何Int 参数进行部分评估，因此g 确实等同于γ :: Int -> (∀ a . Show a => Int -> a)。

对于f'''，将其应用于一些空指针参数将是灾难的根源，因为类型系统无法确保实际传递的类型与Show 函数准备处理的类型相匹配.

【讨论】：

感谢您解释 GHC 如何在幕后实现它。你知道这是否也是类型化 lambda 演算的理论规则吗？
是的，我认为在 System F 中你会有类似 Λ a . (λ (n:a) . X) 这样的表达方式，表达相同的东西，但我从未真正读过。
约束和类型量化的问题是不相交的 - 约束可以出现在不紧邻量词右侧的位置，例如forall a . (C a => a) -> X 与 forall a . C a => a -> X;甚至 (D => X) -> Z 也是有效类型。两者都在核心表示中作为函数参数实现，但是对于类型系统（System F omega 的形式语义）的一个非常原始的原因，量化类型变量就是这种情况，而对于约束，它只是一个实现细节。
@user2407038：听起来不错。我很想看到它的详细解释，添加一个答案怎么样？

【解决方案3】：

这是 Chi 上面评论的副本，它通过将函数解释为逻辑含义（Curry-Howard 对应）来解释理论部分：

类型量词可以与逻辑中的箭头交换：命题p -> forall a. q(a) 等价于forall a. p -> q(a) 提供p 不依赖于a。如果 Haskell 有存在类型，我们将具有同构(forall a. p(a) -> q) ~ ((exists a. p(a)) -> q)。它也与产品通勤(forall a. p a, forall a. q a) ~ forall a. (p a, q a)。总和比较棘手。

我还链接了RankNTypes 的规格。它确实强制执行“浮动”类型量词的规则并定义类型(forall a. SomeClass a => a) -> Int。

【讨论】：