这两个实例是如何重叠的(涉及超出范围的类型)

我几天前在关于在free-monads环境中注入仿函数的问题 . 在那里建议的解决方案,基于Data Types à la Carte使用一个类来表示仿函数之间的一种包含关系 .

-- | Class that represents the relationship between a functor 'sup' containing
-- a functor 'sub'.
class (Functor sub, Functor sup) => sub :-<: sup where
    inj :: sub a -> sup a

-- | A functor contains itself.
instance Functor f => f :-<: f where
    inj = id

-- | A functor is contained in the sum of that functor with another.
instance (Functor f, Functor g) => f :-<: (Sum f g) where
    inj = InL

-- | If a functor 'f' is contained in a functor 'g', then f is contained in the
-- sum of a third functor, say 'h', with 'g'.
instance (Functor f, Functor g, Functor h, f :-<: g) => f :-<: (Sum h g) where
    inj = InR . inj

现在考虑以下数据类型:

type WeatherData = String

data WeatherServiceF a = Fetch (WeatherData -> a) deriving (Functor)

data StorageF a = Store WeatherData a deriving (Functor)

并且具有以下类型的功能

fetch :: (WeatherServiceF :-<: g) => Free g WeatherData

Free 来自Control.Monad.Free模块 .

然后,如果我尝试使用此功能如下:

reportWeather :: Free (Sum WeatherServiceF StorageF) ()
reportWeather = do
    _ <- fetch
    return ()

我得到一个重叠实例错误,说:

• Overlapping instances for WeatherServiceF
                            :-<: Sum WeatherServiceF StorageF
    arising from a use of ‘fetch’
  Matching instances:
    two instances involving out-of-scope types
      instance (Functor f, Functor g) => f :-<: Sum f g

      instance (Functor f, Functor g, Functor h, f :-<: g) =>
               f :-<: Sum h g

现在,我明白第一个是有效的实例,但为什么第二个也被认为是一个有效的实例呢?如果我在第二种情况下实例化变量,我会得到

instance ( Functor WeatherServiceF
         , Functor StorageF
         , Functor WeatherServiceF
         , WeatherServiceF :-<: StorageF
         ) => WeatherServiceF :-<: Sum WeatherServiceF g

哪个不应该是一个实例,因为 WeatherServiceF :-<: StorageF 不是真的 . 为什么GHC推断这样的实例?

我启用了以下实例:

{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators         #-}

回答(1)

2 years ago

编译器必须能够通过仅考虑实例的“头部”来选择实例,而无需查看约束 . 只有在选择适用的实例后才会考虑约束 . 如果它不能在仅仅看到头部的两个实例之间做出决定,那么它们会重叠 .

原因是无法保证最终完整程序中使用的所有实例都将导入此模块 . 如果编译器曾承诺基于无法看到实现另一个实例的约束的实例来选择实例,那么不同的模块可以根据不同的类型对相同类型的两个重叠实例中的哪一个做出不同的选择 . 每个中可用的实例集 .

重叠检查旨在阻止这种情况发生 . 因此,唯一可以做到这一点的方法是,如果GHC在看到哪些实例可能适用于特定情况时,将所有约束视为至少可能满足 . 如果只留下一个候选人,那么无论在计划的其他地方添加或删除其他实例,该候选人都将保留 . 然后,它可以检查此模块中是否有必要的实例以满足约束 .