在Haskell函数中键入量词

Question

假设我有两个以下类型的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演算的规则,类型量词分布在函数目标类型上,而不是函数源类型上吗？

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

Answer 1

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

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