haskell - Haskell 中的模糊实例解析

Question

简介和示例用例

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

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

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

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 ，但在某些特定情况下，它会输出 m3 (X b)对于特定的 X .为简单起见，假设我们要输出 m3 (X b)仅当 m1或 m2是 IO .

看来我们现在不能在 Haskell 中做到这一点而不会失去灵 active 。
我需要以下函数来编译而不添加任何类型信息(Haskell 代码是生成的):

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

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

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 = x polyBind2 (\_ -> 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 = x polyBind3 (\_ -> 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

在 周围进行的一次骇人听闻的尝试

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

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 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 (见最后的代码 list )，但到目前为止我没有得到任何好的结果。

最后一个问题

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

完整代码 list

这是一个完整的代码 list ，可以在 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是单态的，从而固定数字类型并避免麻烦。