存在类型和monad变换器

Question

上下文:我正在尝试生成一个错误monad,它也会跟踪警告列表,如下所示:

data Dangerous a = forall e w. (Error e, Show e, Show w) =>
    Dangerous (ErrorT e (State [w]) a)

即Dangerous a是一个操作导致(Either e a, [w])哪里e是可显示的错误并且w是可显示的.

问题是,我似乎无法真正运行这件事,主要是因为我不太了解存在类型.注意:

runDangerous :: forall a e w. (Error e, Show e, Show w) =>
    Dangerous a -> (Either e a, [w])
runDangerous (Dangerous f) = runState (runErrorT f) []

这不会编译,因为:

Could not deduce (w1 ~ w)
from the context (Error e, Show e, Show w)
...
`w1' is a rigidtype variable bound by
    a pattern with constructor
    Dangerous :: forall a e w.
                 (Error e, Show e, Show w) =>
                 ErrorT e (State [w]) a -> Dangerous a
...
`w' is a rigid type variable bound by
    the type signature for
    runDangerous :: (Error e, Show e, Show w) =>
                    Dangerous a -> (Either e a, [w])

我迷路了.什么是w1？为什么我们不能推断它是~ w什么？

Answer 1

存在主义可能不是你想要的; 有没有办法来"观察"绑定到实际的类型e或w一个Dangerous a值,所以你完全仅限于提供给你的操作Error和Show.

换句话说,你唯一知道的w就是你可以把它变成一个String,所以它也可能只是一个String(忽略简化事物的优先权),你唯一知道的e就是你可以把它变成一个String,你可以把String它变成它,你有一个显着的值(noMsg).没有办法断言或检查这些类型是否与其他类型相同,因此一旦将它们放入a中Dangerous,就无法恢复这些类型可能具有的任何特殊结构.

什么错误消息说的是,从本质上讲,你的类型runDangerous索赔,你可以把Dangerous成(Either e a, [w])用于任何 e与w该有相关的实例.这显然不是这样的:你只能将a Dangerous转换成一种选择:e和w它创建的那种.的w1,因为你仅仅是Dangerous类型与类型的变量定义的w,所以是runDangerous,这样GHC重命名其中一个来避免名称冲突.

您需要提供的类型runDangerous如下所示:

runDangerous
  :: (forall e w. (Error e, Show e, Show w) => (Either e a, [w]) -> r)
  -> Dangerous a -> r

其中,由于将接受一个类型的值的函数(Either e a, [w])进行任何的选择e,并w为他们提供的情况下,和这么久Dangerous a,产生作用的结果.这很难让你满意!

实现非常简单

runDangerous f (Dangerous m) = f $ runState (runErrorT m) []

这对您的版本来说是一个微不足道的变化.如果这适合你,那很好; 但我怀疑存在主义是实现你想要做的任何事情的正确方法.

请注意,您需要{-# LANGUAGE RankNTypes #-}表达的类型runDangerous.或者,您可以为结果类型定义另一个存在方:

data DangerousResult a = forall e w. (Error e, Show e, Show w) =>
   DangerousResult (Either e a, [w])

runDangerous :: Dangerous a -> DangerousResult a
runDangerous (Dangerous m) = DangerousResult $ runState (runErrorT m) []

并提取结果case,但你必须要小心,否则GHC会开始抱怨你已经放弃e或w逃避 - 这相当于试图将一个不充分的多态函数传递给另一种形式runDangerous; 即需要对什么类型e以及w超出runDangerous保证类型的更多限制.