Haskell中的恶意实例解析
介绍和示例用例
你好！ 我在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 = 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
更新奇的尝试使用newtype包装
我告诉它更加黑客，因为它导致我们使用-XIncoherentInstances ，它们是Just (Pure evil) 。 其中一个想法当然可以写出新类型的包装：
newtype XWrapper m a = XWrapper (m (X (a)))
和一些utils解压缩它：
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
但是，再次，我们不能运行我们的测试时，结合绑定和解包功能：
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
我不认为这个问题取决于内射型家庭。
在封闭类型系列OutputOf周围的错误消息中提到了注入类型族位。 但是，这个函数实际上不是内射的 - 第二个方程允许任何x和y 。 GHC喜欢提醒用户不要对类型系列进行注入分析，但有时（比如这里），这个警告是没有用的。
相反，你遇到的问题似乎都源于超载的数字。 当你说Pure 0 ，GHC正确地推断出类型Num a => Pure a 。 问题是，该型级别功能你所访问（类型类的分辨率，函数依赖，类型家庭）很在乎什么具体的选择是由a在这里。 例如，很可能您的任何一种方法对Int来说都表现出不同于Integer 。 （例如，你可以在OutputOf有不同的PolyMonad2实例或额外的方程。）
所有这些的解决方案可能是使用RebindableSyntax并将fromInteger定义为单形，从而修复数字类型并避免麻烦。
我相信这里的根本区别在于：
class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
polyBind :: m1 a -> (a -> m2 b) -> m3 b
b是完全多态的; 它不是类型参数，因此可以选择实例，并应用函数依赖关系来独立于b从m1和m2确定m3 。 它也出现在两个地方; 如果类型推断器知道传递给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 => mc （对于某种类型的构造函数m ），那么没有理由说c和b必须是相同的Num实例。 因此，在一个链一系列polyBind2呼吁数字操作，每一个中间结果，可以使用不同的Num实例，并且不知道任何人没有办法来选择正确的PolyMonad2那些统一的情况下， b与东西out 。 只有当变量的所有约束都是数字前奏类时，类型默认才适用，但这里的b涉及约束PolyMonad2 m1 m2 m3 b ，所以它不能被默认（这可能是一件好事，因为究竟是什么类型你选择的可能会影响使用哪个实例并显着改变程序的行为;它只是已知为相互“近似”的数字类，所以如果程序对使用哪个实例不明确，那么对于使用哪个实例来说这是半合理的只是随意挑选一个而不是抱怨含糊不清）。
就我所知，无论是函数依赖关系，类型家族还是其他类型，从m1 ， m2和b确定的任何方法out一样的。 我不确定如何真正解决这个问题，但没有提供更多的类型注释。