在Haskell函数中输入量词
假设我有两个以下类型的Haskell函数，ExplicitForAll被激活，
f :: forall a. (a -> Int)
g :: forall a. (Int -> a)
在我看来， g的类型同构于Int -> (forall a. a) ，因为例如g(2)的类型是全部forall a. a forall a. a 。
然而， f的类型看起来不同构于(forall a. a) -> Int 。 f是一个多态函数，它知道在每个输入类型a上计算什么，在数学上我猜它应该是一个函数族; 但我不认为它可以处理所有类型的单一参数。
它是一种类型化的lambda演算规则，类型量词分布在函数目标类型上，而不是函数源类型上？
在Haskell中是否存在类型(forall a. a) -> Int ，可能受限于类型类(forall a. SomeClass a => a) -> Int ？ 它有用吗？
weird :: (forall a. a) -> Int不必要的具体。
undefined是唯一值类型为forall a. a forall a. a ，所以定义必须是weird _ = someInteger ，这只是const一个更严格的版本。
∀ 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函数准备处理的类型相匹配。
这是Chi上面评论的一个副本，它通过将函数解释为逻辑含义（Curry-Howard函数）来解释理论部分：
类型量子可以用逻辑交换箭头：命题p -> forall a. q(a) p -> forall a. q(a)相当于forall a. p -> q(a) forall a. p -> q(a)提供p不依赖于a 。 如果Haskell具有存在类型，我们可以有同构(forall a. p(a) -> q) ~ ((exists a. p(a)) -> q) 。 它也会与产品通勤(forall a. pa, forall a. qa) ~ forall a. (pa, qa) (forall a. pa, forall a. qa) ~ forall a. (pa, qa) 。 总和它更棘手。
我也链接了RankNTypes的规格。 它确实执行了“浮出”类型量词的规则并定义了类型(forall a. SomeClass a => a) -> Int 。