这个 GHC 功能叫什么？类型定义中的“forall”

Question

我了解到，您可以ContT从变压器中重新定义，以使r类型参数隐式化（并且可以使用显式指定TypeApplications），即：

-- | Same as `ContT` but with the `r` made implicit
type ContT ::
  forall (r :: Type).
  (Type -> Type) ->
  Type ->
  Type
data ContT m a where
  ContT ::
    forall r m a.
    {runContT :: (a -> m r) -> m r} ->
    ContT @r m a

type ContVoid :: (Type -> Type) -> Type -> Type
type ContVoid = ContT @()

我没有意识到这在 GHC 中是可能的。更大的功能是什么，用来指代这种使用隐式类型参数定义类型族的方法，该方法是在类型定义中使用指定的forall（在上面的示例中，指的是外部forall- 而不是forall简单地统一了内部r） ？

Answer 1

没有人将其（不可见的相关量化）用于此目的（不使用相关性），但它与隐式给出参数相同Type -> ..。

type EITHER :: forall (a :: Type) (b :: Type). Type
data EITHER where
 LEFT  :: a -> EITHER @a @b
 RIGHT :: b -> EITHER @a @b

eITHER :: (a -> res) -> (b -> res) -> (EITHER @a @b -> res)
eITHER left right = \case
 LEFT  a -> left  a
 RIGHT b -> right b

您还可以使用“可见相关量化”，其中forall->是 的可见对应项forall.，所以就像a不出现在..中forall (a :: Type) -> ..一样：Type -> ..

type EITHER :: forall (a :: Type) -> forall (b :: Type) -> Type
data EITHER a b where
 LEFT  :: a -> EITHER a b
 RIGHT :: b -> EITHER a b

eITHER :: (a -> res) -> (b -> res) -> (EITHER a b -> res)
eITHER left right = \case
 LEFT  a -> left  a
 RIGHT b -> right b