Haskell 中的模糊实例解析

Question

简介和示例用例

你好！我在 Haskell 中遇到了问题。让我们考虑以下代码

class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
    polyBind :: m1 a -> (a -> m2 b) -> m3 b

它只是声明了一个 poly monad 绑定。一个很好的示例用例场景是：

newtype Pure a = Pure { fromPure :: a } deriving (Show)

instance PolyMonad Pure Pure Pure where
    polyBind a f = f (fromPure a)

instance PolyMonad Pure IO IO where
    polyBind a f = f (fromPure a)

instance PolyMonad IO Pure IO where
    polyBind a f = (fromPure . f) <$> a

instance PolyMonad IO IO IO where
    polyBind a f = a >>= f

并将其与-XRebindableSyntax 一起使用，如下所示：

test = do
    Pure 5
    print "hello"
    Pure ()

但我们可以用它做更多的事情 - 这只是一个向您展示示例案例的测试。

问题

让我们考虑一些更复杂的用法。我想写一个类似polymonad的类，它不会总是输出m3 b，但在某些特定情况下，它会为特定的X输出m3 (X b)。为简单起见，假设我们只想在m1 或m2 为IO 时输出m3 (X b)。

似乎我们现在不能在 Haskell 中做到这一点而不会失去灵活性。 我需要在不添加任何类型信息的情况下编译以下函数（Haskell 代码是生成的）：

tst1 x = x `polyBind` (\_ -> Pure 0)
tst2 = (Pure 1) `polyBind` (\_ -> Pure 0)
tst3 x y = x `polyBind` (\_ -> y `polyBind` (\_ -> Pure 0))

无论如何，这些函数使用 PolyMonad 类编译得很好。

Fundep 尝试解决问题

其中一种尝试可能是：

class PolyMonad2 m1 m2 m3 b | m1 m2 b -> out where
    polyBind2 :: m1 a -> (a -> m2 b) -> out

当然，我们可以轻松编写所有必要的实例，例如：

instance PolyMonad2 Pure Pure b (Pure b) where
    polyBind2 a f = f (fromPure a)

instance PolyMonad2 Pure IO b (IO (X b)) where
    polyBind2 a f = fmap X $ f (fromPure a)

-- ...

但是当使用polyBind2 而不是polyBind 时，我们的测试函数将无法编译。第一个函数（tst1 x = xpolyBind2(\_ -> Pure 0)）输出编译错误：

Could not deduce (PolyMonad2 m1 Pure b0 out)
  arising from the ambiguity check for ‘tst1’
from the context (PolyMonad2 m1 Pure b out, Num b)
  bound by the inferred type for ‘tst1’:
             (PolyMonad2 m1 Pure b out, Num b) => m1 a -> out
  at /tmp/Problem.hs:51:1-37
The type variable ‘b0’ is ambiguous
When checking that ‘tst1’
  has the inferred type ‘forall (m1 :: * -> *) b out a.
                         (PolyMonad2 m1 Pure b out, Num b) =>
                         m1 a -> out’
Probable cause: the inferred type is ambiguous

封闭类型族试图解决问题

更好的方法是在这里使用closed type families，例如：

class PolyMonad3 m1 m2 where
    polyBind3 :: m1 a -> (a -> m2 b) -> OutputOf m1 m2 b

type family OutputOf m1 m2 a where
    OutputOf Pure Pure a = Pure a
    OutputOf x    y    a = Pure (X a)

但是当尝试编译 tst1 函数 (tst1 x = xpolyBind3(\_ -> Pure 0)) 时，我们得到另一个编译时错误：

Could not deduce (OutputOf m1 Pure b0 ~ OutputOf m1 Pure b)
from the context (PolyMonad3 m1 Pure, Num b)
  bound by the inferred type for ‘tst1’:
             (PolyMonad3 m1 Pure, Num b) => m1 a -> OutputOf m1 Pure b
  at /tmp/Problem.hs:59:1-37
NB: ‘OutputOf’ is a type function, and may not be injective
The type variable ‘b0’ is ambiguous
Expected type: m1 a -> OutputOf m1 Pure b
  Actual type: m1 a -> OutputOf m1 Pure b0
When checking that ‘tst1’
  has the inferred type ‘forall (m1 :: * -> *) a b.
                         (PolyMonad3 m1 Pure, Num b) =>
                         m1 a -> OutputOf m1 Pure b’
Probable cause: the inferred type is ambiguous

一个 hacky 的尝试

我找到了另一种解决方案，但很老套，最终无法正常工作。但这是非常有趣的一个。让我们考虑以下类型类：

class PolyMonad4 m1 m2 b out | m1 m2 b -> out, out -> b where
    polyBind4 :: m1 a -> (a -> m2 b) -> out

当然函数依赖out -> b是错误的，因为我们不能定义这样的实例：

instance PolyMonad4 Pure IO b (IO (X b)) where
    polyBind4 a f = fmap X $ f (fromPure a)

instance PolyMonad4 IO IO b (IO b) where
    polyBind4 = undefined

但让我们玩它并声明它们（使用-XUndecidableInstances）：

instance out~(Pure b) => PolyMonad4 Pure Pure b out where
    polyBind4 a f = f (fromPure a)

instance out~(IO(X b)) => PolyMonad4 Pure IO b out where
    polyBind4 a f = fmap X $ f (fromPure a)

instance out~(IO b) => PolyMonad4 IO IO b out where
    polyBind4 = undefined

instance out~(IO(X b)) => PolyMonad4 IO Pure b out where
    polyBind4 = undefined

有趣的是，我们的一些测试函数确实可以编译和工作，即：

tst1' x = x `polyBind4` (\_ -> Pure 0)
tst2' = (Pure 1) `polyBind4` (\_ -> Pure 0)

但这个不是：

tst3' x y = x `polyBind4` (\_ -> y `polyBind4` (\_ -> Pure 0))

导致编译时错误：

Could not deduce (PolyMonad4 m3 Pure b0 (m20 b))
  arising from the ambiguity check for ‘tst3'’
from the context (PolyMonad4 m3 Pure b1 (m2 b),
                  PolyMonad4 m1 m2 b out,
                  Num b1)
  bound by the inferred type for ‘tst3'’:
             (PolyMonad4 m3 Pure b1 (m2 b), PolyMonad4 m1 m2 b out, Num b1) =>
             m1 a -> m3 a1 -> out
  at /tmp/Problem.hs:104:1-62
The type variables ‘m20’, ‘b0’ are ambiguous
When checking that ‘tst3'’
  has the inferred type ‘forall (m1 :: * -> *)
                                (m2 :: * -> *)
                                b
                                out
                                a
                                (m3 :: * -> *)
                                b1
                                a1.
                         (PolyMonad4 m3 Pure b1 (m2 b), PolyMonad4 m1 m2 b out, Num b1) =>
                         m1 a -> m3 a1 -> out’
Probable cause: the inferred type is ambiguous

使用新类型包装的更骇人听闻的尝试

我告诉过它更hacky，因为它导致我们使用-XIncoherentInstances，即Just (Pure evil)。其中一个想法当然是编写 newtype 包装器：

newtype XWrapper m a = XWrapper (m (X (a)))

还有一些解压它的工具：

class UnpackWrapper a b | a -> b where
    unpackWrapper :: a -> b

instance UnpackWrapper (XWrapper m a) (m (X a)) where
    unpackWrapper (XWrapper a) = a

instance UnpackWrapper (Pure a) (Pure a) where
    unpackWrapper = id

instance UnpackWrapper (IO a) (IO a) where
    unpackWrapper = id

现在我们可以轻松声明以下实例：

instance PolyMonad Pure Pure Pure 
instance PolyMonad Pure IO (XWrapper IO) 
instance PolyMonad IO Pure (XWrapper IO) 
instance PolyMonad IO IO IO 

但同样，当结合 bind 和 unwrap 函数时，我们无法运行我们的测试：

polyBindUnwrap a f = unpackWrapper $ polyBind a f

测试函数再次编译失败。我们可以在这里乱用一些-XIncoherentInstances（见最后的代码清单），但到目前为止我没有得到任何好的结果。

最后一个问题

这是使用当前 GHC Haskell 实现无法解决的问题吗？

完整代码清单

这是一个完整的代码清单，可以在 GHC >= 7.8 中运行：

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import Control.Applicative

class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
    polyBind :: m1 a -> (a -> m2 b) -> m3 b


----------------------------------------------------------------------
-- Some utils
----------------------------------------------------------------------

newtype Pure a = Pure { fromPure :: a } deriving (Show)
newtype X a = X { fromX :: a } deriving (Show)

main = return ()

----------------------------------------------------------------------
-- Example use cases
----------------------------------------------------------------------

instance PolyMonad Pure Pure Pure where
    polyBind a f = f (fromPure a)

instance PolyMonad Pure IO IO where
    polyBind a f = f (fromPure a)

instance PolyMonad IO Pure IO where
    polyBind a f = (fromPure . f) <$> a

instance PolyMonad IO IO IO where
    polyBind a f = a >>= f

-- works when using rebindable syntax
--test = do
--    Pure 5
--    print "hello"
--    Pure ()

tst1 x = x `polyBind` (\_ -> Pure 0)
tst2 = (Pure 1) `polyBind` (\_ -> Pure 0)
tst3 x y = x `polyBind` (\_ -> y `polyBind` (\_ -> Pure 0))

----------------------------------------------------------------------
-- First attempt to solve the problem
----------------------------------------------------------------------


class PolyMonad2 m1 m2 b out | m1 m2 b -> out where
    polyBind2 :: m1 a -> (a -> m2 b) -> out


instance PolyMonad2 Pure Pure b (Pure b) where
    polyBind2 a f = f (fromPure a)

instance PolyMonad2 Pure IO b (IO (X b)) where
    polyBind2 a f = fmap X $ f (fromPure a)

-- ...

-- tst1 x = x `polyBind2` (\_ -> Pure 0) -- does NOT compile


----------------------------------------------------------------------
-- Second attempt to solve the problem
----------------------------------------------------------------------

class PolyMonad3 m1 m2 where
    polyBind3 :: m1 a -> (a -> m2 b) -> OutputOf m1 m2 b

type family OutputOf m1 m2 a where
    OutputOf Pure Pure a = Pure a
    OutputOf x    y    a = Pure (X a)

-- tst1 x = x `polyBind3` (\_ -> Pure 0) -- does NOT compile


----------------------------------------------------------------------
-- Third attempt to solve the problem
----------------------------------------------------------------------

class PolyMonad4 m1 m2 b out | m1 m2 b -> out, out -> b where
    polyBind4 :: m1 a -> (a -> m2 b) -> out


instance out~(Pure b) => PolyMonad4 Pure Pure b out where
    polyBind4 a f = f (fromPure a)

instance out~(IO(X b)) => PolyMonad4 Pure IO b out where
    polyBind4 a f = fmap X $ f (fromPure a)

instance out~(IO b) => PolyMonad4 IO IO b out where
    polyBind4 = undefined

instance out~(IO(X b)) => PolyMonad4 IO Pure b out where
    polyBind4 = undefined


tst1' x = x `polyBind4` (\_ -> Pure 0)
tst2' = (Pure 1) `polyBind4` (\_ -> Pure 0)
--tst3' x y = x `polyBind4` (\_ -> y `polyBind4` (\_ -> Pure 0)) -- does NOT compile


----------------------------------------------------------------------
-- Fourth attempt to solve the problem
----------------------------------------------------------------------

class PolyMonad6 m1 m2 m3 | m1 m2 -> m3 where
    polyBind6 :: m1 a -> (a -> m2 b) -> m3 b

newtype XWrapper m a = XWrapper (m (X (a)))


class UnpackWrapper a b | a -> b where
    unpackWrapper :: a -> b

instance UnpackWrapper (XWrapper m a) (m (X a)) where
    unpackWrapper (XWrapper a) = a

instance UnpackWrapper (Pure a) (Pure a) where
    unpackWrapper = id

instance UnpackWrapper (IO a) (IO a) where
    unpackWrapper = id

--instance (a1~a2, out~(m a2)) => UnpackWrapper (m a1) out where
--    unpackWrapper = id


--{-# LANGUAGE OverlappingInstances #-}
--{-# LANGUAGE IncoherentInstances #-}

instance PolyMonad6 Pure Pure Pure where
    polyBind6 = undefined

instance PolyMonad6 Pure IO (XWrapper IO) where
    polyBind6 = undefined

instance PolyMonad6 IO Pure (XWrapper IO) where
    polyBind6 = undefined

instance PolyMonad6 IO IO IO where
    polyBind6 = undefined

--polyBind6' a f = unpackWrapper $ polyBind6 a f

--tst1'' x = x `polyBind6'` (\_ -> Pure 0)
--tst2'' = (Pure 1) `polyBind4` (\_ -> Pure 0)
--tst3'' x y = x `polyBind4` (\_ -> y `polyBind4` (\_ -> Pure 0)) -- does NOT compile

Answer 1

我不认为这个问题取决于单射类型族。

封闭类型族OutputOf 周围的错误消息中提到了单射类型族位。但是，该函数确实不是单射的——它的第二个等式允许任何x 和y。 GHC 喜欢提醒用户它不会对类型族进行单射性分析，但有时（如此处），此警告没有帮助。

相反，您遇到的所有问题似乎都源于超载的数字。当你说Pure 0 时，GHC 正确地推断出Num a => Pure a 的类型。问题是您正在访问的类型级特性（类型类解析、函数依赖项、类型族）非常关心这里为a 做出的具体选择。例如，很可能您的任何一种方法对Int 的行为与对Integer 的行为不同。 （例如，PolyMonad2 的不同实例或OutputOf 中的额外方程式。）

解决所有这些问题的方法可能是使用RebindableSyntax 并将fromInteger 定义为单态，从而固定数字类型并避免麻烦。

Answer 2

我认为根本区别在于：

class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
    polyBind :: m1 a -> (a -> m2 b) -> m3 b

b 是完全多态的；它不是类型类的参数，因此可以选择实例并应用函数依赖关系来确定m1 和m2 中的m3，独立于b。它也出现在两个地方；如果类型推断器知道结果类型或传递给polyBind的函数类型，那么它就可以充分确定b。并且像Num b => b 这样的类型将愉快地“流过”polyBind 的许多应用程序，直到它被用于修复具体类型的地方。虽然我认为这可能只是单态限制默认类型，在这种情况下可以避免模棱两可的类型变量错误（正是它的设计目的）。

而在这里：

class PolyMonad2 m1 m2 m3 b | m1 m2 b -> out where
    polyBind2 :: m1 a -> (a -> m2 b) -> out

b 显示为类型类参数。如果我们试图推断 out 是什么，我们需要在选择实例之前完全确定 b。并且 b 没有理由与 out 类型的结构有任何特定关系（或者更确切地说，这种关系对于每个单独的实例都可能不同，这毕竟是你想要实现的），所以除非您完全解决了所有个实例，否则不可能“通过”polyBind2 调用链“跟踪 b”。

如果b 是一个多态数Num b => b 并且out 受限于其使用形式为Num c => m c（对于某些类型的构造函数m），则没有理由认为c b 必须是 same Num 实例。因此，在对数字进行的一系列polyBind2 调用链中，每个中间结果可能使用不同的Num 实例，并且在不知道其中任何一个的情况下，无法选择正确的PolyMonad2将b 与out 中的内容统一起来的实例。类型默认仅适用于变量上的所有约束都是数字前奏类，但这里b 涉及约束PolyMonad2 m1 m2 m3 b，因此它不能被默认（这可能是一件好事，因为究竟是什么类型您选择可能会影响使用哪个实例并显着改变程序行为；只有数字类已知是彼此的“近似值”，因此如果程序对使用哪个实例不明确，那么它是半合理的随便挑一个，而不是抱怨模棱两可）。

据我所知，从m1、m2 和b 确定out 的任何方法都是如此，无论是功能依赖、类型系列还是其他。我不确定如何在此处实际解决该问题，但不提供更多类型注释。