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

Question

我想知道我是否可以写一个函数isPure :: Free f () -> Bool ，它告诉你给定的自由单子(monad)是否等于 Pure ()或不。对于简单的情况，这很容易做到，但对于仿函数 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)的粗粒度结构(即它是 Pure 还是不是 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 强制 Foo 和 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' 不需要实例化。 .忽略bottoms1，你可以实例化的仿函数之一ComplexFree是 Const Void ，这意味着 Free 的递归情况减少到

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

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

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

多么无聊。

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

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

在这种情况下，ComplexFree “携带”仿函数。它只适用于一个仿函数，并且它(并且只有它)知道那是什么仿函数。这个问题的形式更好，并且按照您的预期实现

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

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