这两个实例如何重叠（涉及超范围类型） [英] How are these two instances overlapping (involving out-of-scope types)

问题描述

我几天前我提出了一个关于在自由单体环境中注入仿函数的问题。这里提出的解决方案基于点菜数据类型使用一个代表仿函数之间包含关系的类。

   -  |代表包含
的函子'sup'与函子'sub'之间关系的类。 
 class（Functor sub，Functor sup）=> sub： - <：sup其中
 inj :: sub a  - > sup a 
 
  -  |一个函子包含它自己。 
实例Functor f => f： - <：f其中
 inj = id 
 
  -  |一个仿函数包含在该仿函数与另一个仿函数的总和中。 
实例（Functor f，Functor g）=> f： - <：（Sum f g）其中
 inj = InL 
 
  -  |如果仿函数'f'包含在仿函数'g'中，则f包含在
  - 第三个仿函数的总和中，比如'h'和'g'。 
实例（Functor f，Functor g，Functor h，f： - < ;: g）=> f： - < ;:（Sum h g）其中
 inj = InR。注意
  

现在考虑以下数据类型：

< pre $ type WeatherData = String

WeatherServiceF a = Fetch（WeatherData - > a）派生（Functor）

数据StorageF a =存储WeatherData一个派生函数（Functor）


以下类型的函数

  fetch ::（WeatherServiceF： - <：g）=> Free g WeatherData 
  

其中空闲来自 Control.Monad.Free module。

然后，如果我尝试按如下方式使用此函数：

  reportWeather :: Free（Sum WeatherServiceF StorageF）（）
 reportWeather = do 
 _<  -  fetch 
 return（）
  

我得到重叠实例错误，说：

 •WeatherServiceF的重叠实例
： - <：Sum使用'fetch'产生的WeatherServiceF StorageF 
 
匹配实例：
涉及范围外类型的两个实例
实例（Functor f，Functor g）=> f： - <：Sum f g 
 
 instance（Functor f，Functor g，Functor h，f： - < ;: g）=> 
f： - <：Sum hg 
  

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

 实例（Functor WeatherServiceF 
，Functor StorageF 
，Functor WeatherServiceF 
，WeatherServiceF： - <：StorageF 
）=> WeatherServiceF： - <：Sum WeatherServiceF g 
  

这不应该是一个实例，因为它不是真的 WeatherServiceF： - <：StorageF 。为什么GHC推断这样的实例？

我启用了以下实例：

  { - ＃LANGUAGE FlexibleContexts＃ - } 
 { - ＃LANGUAGE TypeOperators＃ - } 
  

解决方案

编译器必须能够通过仅考虑实例的头部来选择实例，而不必查看约束。只有在选择适用的实例后才考虑约束条件。如果它不能确定两个实例之间只看到头部，那么它们会重叠。

原因是，不能保证最终完成中使用的所有实例程序将被导入这个模块。如果编译器曾经承诺基于不能看到满足另一个实例的约束的实例而选择实例，那么不同的模块可以根据不同的选择关于两个重叠实例中的哪一个用于相同类型每个实例都有一套实例。

重叠检查旨在阻止这种情况的发生。所以它唯一可以做到这一点的方式是，如果GHC在给定情况下查看哪些实例可能适用，至少潜在地可以满足所有约束。如果只剩下一名候选人，那么该候选人将保留，而不管在该计划的其他地方添加或删除了哪些其他实例。然后它可以检查该模块中是否有必要的实例可以满足约束条件。

I couple of days ago I asked a question about injecting functors in the context of free-monads. The solution suggested there, based on Data Types à la Carte uses a class that represents a sort of containment relationship between functors.

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

Now consider the following data types:

type WeatherData = String

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

data StorageF a = Store WeatherData a deriving (Functor)

And a function with the following type

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

Where Free comes from the Control.Monad.Free module.

Then if I try to use this function as follows:

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

I get an overlapping-instances error, saying:

• 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

Now, I understand that the first is a valid instance, but why the second is considered a valid instance as well? If I instantiate the variables in the second case I would get

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

Which should not be an instance since it is not true that WeatherServiceF :-<: StorageF. Why is GHC inferring such an instance?

I have the following instances enabled:

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

解决方案

The compiler has to be able to select instances by considering only the "head" of the instance, without looking at the constraints. The constraints are only considered once the applicable instance has been chosen. If it cannot decide between two instances looking only at the head, then they overlap.

The reason is that there is no guarantee that all of the instances used in the final complete program will be imported into this module. If the compiler ever committed to choosing an instance based on not being able to see an instance fulfilling a constraint of another instance, then different modules could make different choices about which of the two overlapping instances to use for the same type, based on the different set of instances available in each.

The overlap check is intended to stop that happening. So the only way it can do that is if GHC treats all constraints as at least potentially satisfiable when it's seeing which instances might apply in a given situation. When that leaves exactly one candidate, that candidate will remain regardless of what other instances are added or removed elsewhere in the program. It can then check that the necessary instances are available in this module to satisfy the constraints.

这篇关于这两个实例如何重叠（涉及超范围类型）的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！