‘`forall a -> b’语法是什么意思？

Question

在GHCi中，FUN的类型显示如下：

λ> :k FUN
FUN :: forall (n :: Multiplicity) -> * -> * -> *

起初，我认为这是一种迂回的说法。

FUN :: Multiplicity -> * -> * -> *

但是事实证明，模板Haskell为这个表单有一个单独的构造函数：ForallVisT。我找不到任何关于它的文档，我也不知道如何开始以一种有意义的方式进行实验。

这个语法是什么意思？forall a -> b与“普通”forall a. a -> b有何不同？

Answer 1

当结果类型依赖于显式参数时，将使用forall a -> _。

-- type NonDep :: Type -> Type; argument is explicit
data NonDep (x :: Type) :: Type
-- type ImpDep :: forall a. Maybe a -> Type; first argument is implicit and dependent
data ImpDep (x :: Maybe a) :: Type
-- so if you want an explicit and dependent argument...
-- type ExpDep :: forall (a :: Type) -> Maybe a -> Type
data ExpDep (a :: Type) (x :: Maybe a) :: Type

奇怪的是，FUN的类型有forall (m :: Multiplicity) ->而不是Multiplicity ->，因为以下参数(两个隐式RuntimeReps和两个TYPEs)不依赖于它，但这就是围绕GHC原语的奇怪之处。