2

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)
4

1 回答 1

4

要将类型变量带入范围，请使用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，请记住，m必须在创建时Exists选择它。所以调用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的类型之外几乎没有用。这是因为任何消耗这种价值的人都必须能够使用任何monad ，并且您可以使用 monad 做任何事情，除非您知道它是什么。你不能在里面绑定它，因为它不是必须的，你不能与它进行模式匹配，或者因为它不是必须的，等等。你唯一能用它做的就是用 绑定它，但是你只会得到它的另一个实例，然后你又回到了原点。xProxymIOIOJustNothingMaybe>>=

于 2021-03-25T15:15:17.577 回答