"forall a -> b"语法是什么意思？

Question

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

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

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

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

但事实证明，TemplateHaskell有一个单独的构造函数用于这种形式：ForallVisT。我找不到任何关于它的文档，我甚至不知道如何开始以一种有意义的方式进行实验。

这个语法是什么意思？CCD_ 3与"；正常的"；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基元的怪异之处。