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 是如何被构造函数 Impure 绑定的。

这里是完整的代码：

{-# 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 结尾，使类型成为 "existential"。

事实 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

这将迫使您稍后传递多态 runContinuation 函数，该函数适用于 x 的任何选择，可能会发现 "inside" 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] 类型。

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

GHC type error doesn't make sense to me

haskell

ghc