存在类型的类型变量介绍

Question

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

我可以添加一个额外的参数，但它违背了目的。

{-# 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相同)之外几乎毫无用处。这是因为无论谁消耗这样的值，都必须能够使用任何monadm，并且你可以用monad做任何事情，除非你知道它是什么。你不能把它绑定在IO里面，因为它不一定是IO的，你不能用Just或Nothing来匹配它，因为它不一定是Maybe的，等等。你唯一能做的就是用>>=绑定它，但随后你会得到它的另一个实例，然后你又回到了原点。