存在类型的类型变量介绍

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[=46 时选择 m =].所以调用 Exists 构造函数的人必须知道 m 是什么。

如果您希望它是相反的方式 - 即 unwraps 一个 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 相同）。这是因为任何消费这种价值的人都必须能够使用 any monad m，并且你可以用 monad 做任何事情，除非你知道它是什么。你不能把它绑定在IO里面，因为它不一定是IO，你不能把它和Just或者Nothing进行模式匹配，因为它不一定是Maybe ]，等等。你唯一能用它做的就是用 >>= 绑定它，但是你只会得到它的另一个实例，然后你又回到了原点。

存在类型的类型变量介绍

Type variable introduction for existential types

haskell

existential-type

quantifiers

rank-n-types