时间戳

首页 > 解决方案 > 如何在普遍量化的自由单子上进行模式匹配？

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

问题描述

我想知道我是否可以编写一个函数isPure :: Free f () -> Bool，它告诉你给定的自由单子是否等于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 的粗粒度结构（即 is it Pureor not Pure）。我不想确定类型，因为我的程序依赖于传递一些受约束的普遍量化的自由单子，我希望它可以与它们中的任何一个一起使用。有没有办法做到这一点？谢谢！

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

编辑：因为我的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 -- ???

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

标签： haskell

解决方案

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

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

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

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

, 意思是一样的)

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

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

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

但是，实例化对于定义isPure'. 忽略底部1，您可以实例化的函子之一ComplexFree是Const Void，这意味着递归情况Free减少为

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

也就是说，这是不可能的。通过一些自然性论证，我们可以证明一个分支ComplexFree不能依赖于函子的选择，这意味着任何完全定义的都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'同样无用。

推荐阅读