如何在普遍量化的自由单子上进行模式匹配？

Question

我想知道我是否可以写一个函数isPure :: Free f () -> Bool，它告诉你给定的自由 monad 是否相等Pure ()。对于一个简单的情况，这很容易做到，但对于更复杂的情况，我无法弄清楚 functor 有约束f。

import Control.Monad.Free

-- * This one compiles

isPure :: Free Maybe () -> Bool
isPure (Pure ()) = True
isPure _ = False

-- * This one fails to compile with "Ambiguous type variable ‘context0’ arising from a pattern
-- prevents the constraint ‘(Functor context0)’ from being solved."

{-# LANGUAGE RankNTypes #-}
type ComplexFree = forall context. (Functor context) => Free context ()

isPure' :: ComplexFree -> Bool
isPure' (Pure ()) = True
isPure' _ = False

我可以context0理解为什么通常需要指定确切的类型，但我想要的只是查看自由 monad 的粗粒度结构（即 is it Pureor not Pure）。我不想确定类型，因为我的程序依赖于传递一些受约束的普遍量化的自由 monad，我希望它可以与它们中的任何一个一起使用。有没有办法做到这一点？谢谢！

编辑更改“存在量化”->“普遍量化”

编辑：因为我的ComplexFree类型可能太笼统了，这里的版本更准确地模仿了我想要做的事情。

--* This one actually triggers GHC's warning about impredicative polymorphism...
{-# LANGUAGE GADTs #-}

data MyFunctor context next where
  MyFunctor :: Int -> MyFunctor context next -- arguments not important

type RealisticFree context a = Free (MyFunctor context) a

class HasFoo context where
  getFoo :: context -> Foo

class HasBar context where
  getBar :: context -> Bar

type ConstrainedRealisticFree = forall context. (HasFoo context, HasBar context) => RealisticFree context ()

processRealisticFree :: ConstrainedRealisticFree -> IO ()
processRealisticFree crf = case isPure'' crf of
  True -> putStrLn "It's pure!"
  False -> putStrLn "Not pure!"

isPure'' :: ConstrainedRealisticFree -> Bool
isPure'' = undefined -- ???

（对于更多的上下文，这个免费的 monad 旨在为简单语言的解释器建模，其中存在“上下文”。您可以将上下文视为描述在其中评估语言的阅读器 monad，因此HasFoo context并HasBar context强制执行aFoo和Bar可用。我使用通用量化，以便上下文的确切类型可以变化。我的目标是能够在这个免费的 monad 解释器中识别“空程序”。）

Answer 1

首先，这不是存在量化。那看起来像这样：

data ComplexFree = forall context. (Functor context) => ComplexFree (Free context ())

（我觉得这种语法相当混乱，所以我更喜欢 GADT 形式

data ComplexFree where
    ComplexFree :: (Functor context) => Free context () -> ComplexFree 

，这意味着同样的事情）

你在这里有一个普遍量化的类型，也就是说，如果你有一个类型的值ComplexFree（你写它的方式），它可以在你选择的任何函子上变成一个自由的 monad。所以你可以在 实例化它Identity，例如

isPure' :: ComplexFree -> Bool
isPure' m = case m :: Free Identity () of 
                Pure () -> True
                _       -> False

它必须以某种类型实例化才能检查它，您看到的错误是因为编译器无法自行决定使用哪个函子。

但是，定义 不需要实例化isPure'。忽略底部¹，您可以实例化的函子之一ComplexFree是Const Void，这意味着递归情况Free减少到

f (m a)
  = Const Void (m a)
 ~= Void

也就是说，这是不可能的。通过一些自然性论证，我们可以证明 aComplexFree取哪个分支不依赖于函子的选择，这意味着任何完全定义的都ComplexFree必须是Pure一个。所以我们可以“简化”到

isPure' :: ComplexFree -> Bool
isPure' _ = True

多么无聊。

但是，我怀疑您可能在定义 时犯了一个错误ComplexFree，而您真的想要存在版本吗？

data ComplexFree where
    ComplexFree :: (Functor context) => Free context () -> ComplexFree

在这种情况下，a ComplexFree“携带”了函子。它只对一个函子有效，而且它（并且只有它）知道那是什么函子。这个问题的形式更好，并且正如您所期望的那样实现

isPure' :: ComplexFree -> Bool
isPure' (ComplexFree (Pure _)) = True
isPure' _ = False

¹忽略底部是一种常见的做法，通常不会有问题。这种减少严格地增加了程序的信息内容——也就是说，每当原始版本给出一个明确的答案时，新版本就会给出相同的答案。但是新的可能“无法进入无限循环”而意外地给出了答案。在任何情况下，这种减少都可以修改为完全正确，结果isPure'同样无用。

Answer 2

我将在这里回答您修改后的问题。事实证明，答案仍然与 luqui 的基本相同：您需要先实例化多态参数，然后才能对其进行模式匹配。由于该约束，您需要使用作为相关类的实例的上下文类型。如果使用“真正的”不方便，您可以轻松地扔掉：

data Gump = Gump Foo Bar

instance HasFoo Gump where
  getFoo (Gump f _) = f

instance HasBar Gump where
  getBar (Gump _ b) = b

对于这个特殊情况来说，这应该没问题。然而，在大多数类似的实际情况中，您需要实例化您的真实类型以获得其专门的行为。

现在您可以实例化上下文Gump，然后就可以开始了：

isPure'' :: ConstrainedRealisticFree -> Bool
isPure'' q = case q :: RealisticFree Gump () of
  Pure _ -> True
  Free _ -> False

你得到关于命令类型的错误的原因是你写了

isPure'' = ...

高阶多态参数通常要求是语法参数：

isPure'' q = ...