GHC 类型错误对我来说没有意义

Question

，所以我正在播放可扩展的效果，试图重新进化一些基本类型和功能时，当我得到这种类型的错误时：

home/kadhem/projects/Haskell/stackWorkingAgain/app/Implementation_error.hs:24:96: error:
    * Couldn't match type `x1' with `x'
      `x1' is a rigid type variable bound by
        a pattern with constructor:
          Impure :: forall (r :: [* -> *]) a x.
                    Union r x -> (x -> Eff r a) -> Eff r a,
        in an equation for `createInterpreter'
        at /home/kadhem/projects/Haskell/stackWorkingAgain/app/Implementation_error.hs:22:59-68
      `x' is a rigid type variable bound by
        the type signature for:
          createInterpreter :: forall a (r :: [* -> *]) b (f :: * -> *) x.
                               (a -> Eff r b)
                               -> (f x -> (x -> Eff (f : r) a) -> Eff (f : r) a)
                               -> (Eff r b -> Eff r b)
                               -> Eff (f : r) a
                               -> Eff r b
        at /home/kadhem/projects/Haskell/stackWorkingAgain/app/Implementation_error.hs:(15,1)-(18,47)
      Expected type: f x
        Actual type: f x1
    * In the first argument of `runContinuation', namely
        `f_is_theTarget'

我不明白x1如何被构造函数不纯净。

这是完整的代码：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE  DataKinds #-}
{-# LANGUAGE  FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}

module Implemntation where
import Data.OpenUnion (Union , decomp)

data Eff r a where 
   Pure :: a -> Eff r a
   Impure ::  Union r x -> (x -> Eff r a) -> Eff r a
createInterpreter :: (a -> Eff r b)
                  -> (f x -> (x -> Eff (f ': r) a) -> Eff (f ': r) a)
                  -> (Eff r b -> Eff r b) 
                  -> Eff (f ': r) a -> Eff r b

createInterpreter handlePure runContinuation applyEffect (Pure a) = 
      handlePure a
createInterpreter handlePure runContinuation applyEffect (Impure f k) 
      = case decomp f of
Right f_is_theTarget
     -> applyEffect $ createInterpreter handlePure runContinuation 
           applyEffect (runContinuation f_is_theTarget k)
Left f_is_notTheTarget
     -> Impure f_is_notTheTarget $ createInterpreter handlePure 
           runContinuation applyEffect  . k 

Answer 1

考虑这两个事实：

事实1：谁称为Impure的人都可以选择其类型中的x的类型：

Impure ::  Union r x -> (x -> Eff r a) -> Eff r a

请注意，这种x最终不会在Eff r a中，使该类型为"存在"。

事实2：谁称为createInterpreter的人可以在其类型中选择x的值

createInterpreter :: (a -> Eff r b)
                  -> (f x -> (x -> Eff (f ': r) a) -> Eff (f ': r) a)
                  -> (Eff r b -> Eff r b) 
                  -> Eff (f ': r) a -> Eff r b

请注意，此选择是独立的。

所以，这两个事实都意味着当我们调用

时

createInterpreter handlePure runContinuation applyEffect (Impure f k)

我们可以通过x类型传递runContinuation函数，并使用不同类型的x(例如x1(传递Impure。由于您试图混合这些类型，因此编译器抱怨它们不必相同。

您可能想要以下类型

createInterpreter :: (a -> Eff r b)
                  -> (forall x. f x -> (x -> Eff (f ': r) a) -> Eff (f ': r) a)
                  -> (Eff r b -> Eff r b) 
                  -> Eff (f ': r) a -> Eff r b

这将迫使您稍后通过A polymorphic runContinuation函数，该功能可用于任何选择的x，这些功能可能会发现" Impure"。

---

您的示例非常复杂，但是要了解问题，您也可以考虑这种类似的情况：

data SomeList where
   SL :: [x] -> SomeList
sumIntList :: [Int] -> Int
sumIntList = sum
workWithSL :: ([x] -> Int) -> SomeList -> Int
workWithSL f (SL list) = f list
test :: Int
test = workWithSL sumIntList (SL [True, False])

在这里，我们在调用SL时选择x = Bool，但是我们在调用workWithSL时选择x = Int(因为我们通过sumIntList(。这样的呼叫没有错，因为类型完美地检查了。真正的问题是在workWithSL内部，无法将f应用于list，因为list可能是类型[x1]而不是[x]。