haskell - 存在类型的类型变量引入

Question

haskell中是否有任何绑定(bind)器来引入在类型中量化的类型变量(和约束)？

我可以添加一个额外的参数，但它达不到目的。

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}


data Exists x = forall m. Monad m => Exists (m x)

convBad ::  x -> Exists x  
convBad  x = Exists @m (return @m x, undefined) --Not in scope: type variable ‘m’typecheck


data Proxy (m:: * -> *) where Proxy :: Proxy m

convOk ::  Monad m => x -> Proxy m -> Exists x 
convOk  x (_ :: Proxy m) = Exists (return @m x)

Answer 1

要将类型变量引入作用域，请使用 forall (由 ExplicitForall 启用，由 ScopedTypeVariables 隐含):

convWorksNow :: forall m x. Monad m => x -> Exists x  
convWorksNow x = Exists (return @m x)

-- Usage:
ex :: Exists Int
ex = convWorksNow @Maybe 42

但是无论您是这样做还是通过 Proxy 执行此操作，请记住，在创建 Exists 时必须选择 m。因此，无论谁调用 Exists 构造函数，都必须知道 m 是什么。

如果您希望相反 - 即无论谁解开 Exists 值都选择 m， - 那么您的 forall 应该在里面:

newtype Exists x = Exists (forall m. Monad m => m x)

convInside :: x -> Exists x
convInside x = Exists (return x)

-- Usage:
ex :: Exists Int
ex = convInside 42

main = do
  case ex of
    Exists mx -> mx >>= print  -- Here I choose m ~ IO

  case ex of
    Exists mx -> print (fromMaybe 0 mx)  -- Here I choose m ~ Maybe

---

此外，正如 @dfeuer 在评论中指出的那样，请注意，您的原始类型定义(外部带有 forall 的类型)除了表示 x 的类型之外几乎没有任何用处。 (与Proxy 相同)。这是因为无论是谁消耗了这样的值(value)，都必须能够使用任何 monad m，并且你可以使用 monad 做任何事情，除非你知道它是什么。您无法将其绑定(bind)在 IO 内部，因为它不一定是 IO，您无法将其与 Just 或 Nothing 进行模式匹配 因为它不一定是也许，等等。你唯一能用它做的就是用 >>= 绑定(bind)它，但随后你只会得到它的另一个实例，然后你又回到了原点。