为什么使用QuantifiedConstraints指定类型类的子类也需要该子类的实例? [英] Why is using QuantifiedConstraints to specify a subclass of a typeclass also demanding an instance of the subclass?

问题描述

我正在使用Free

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
module Free where
import GHC.Types

type (a :: k) ~> (b :: k) = Morphism k a b

newtype Natural (f :: j -> k) (g :: j -> k) = 
  Natural { getNatural :: forall (x :: j). f x ~> g x }

type family Morphism k :: k -> k -> Type where
  Morphism Type = (->)
  Morphism (j -> k) = Natural

class DataKind k where
  data Free :: (k -> Constraint) -> k -> k
  interpret :: forall (cls :: k -> Constraint) (u :: k) (v :: k). 
               cls v => (u ~> v) -> (Free cls u ~> v)
  call :: forall (cls :: k -> Constraint) (u :: k). 
          u ~> Free cls u

instance DataKind Type where
  newtype Free cls u = Free0
    { runFree0 :: forall v. cls v => (u ~> v) -> v }
  interpret f = \(Free0 g) -> g f
  call = \u -> Free0 $ \f -> f u

我可以毫无问题地为Free Semigroup和Free Monoid编写Semigroup实例:

I can write Semigroup instances for Free Semigroup and Free Monoid without a problem:

instance Semigroup (Free Semigroup u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

instance Semigroup (Free Monoid u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

这些实例是相同的，并且将用于Semigroup的任何其他子类.

These instances are the same, and will be for any other subclass of Semigroup.

我想使用QuantifiedConstraints，所以我可以为Semigroup的所有子类编写一个实例:

I want to use QuantifiedConstraints so I can just write one instance for all subclasses of Semigroup:

instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

但是编译器(GHC-8.6.3)抱怨无法推断cls (Free cls u):

But the compiler (GHC-8.6.3) complains that it's unable to deduce cls (Free cls u):

Free.hs:57:10: error:
    • Could not deduce: cls (Free cls u)
        arising from a use of ‘GHC.Base.$dmsconcat’
      from the context: forall v. cls v => Semigroup v
        bound by the instance declaration at Free.hs:57:10-67
    • In the expression: GHC.Base.$dmsconcat @(Free cls u)
      In an equation for ‘GHC.Base.sconcat’:
          GHC.Base.sconcat = GHC.Base.$dmsconcat @(Free cls u)
      In the instance declaration for ‘Semigroup (Free cls u)’
    • Relevant bindings include
        sconcat :: GHC.Base.NonEmpty (Free cls u) -> Free cls u
          (bound at Free.hs:57:10)
   |
57 | instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Free.hs:57:10: error:
    • Could not deduce: cls (Free cls u)
        arising from a use of ‘GHC.Base.$dmstimes’
      from the context: forall v. cls v => Semigroup v
        bound by the instance declaration at Free.hs:57:10-67
      or from: Integral b
        bound by the type signature for:
                   GHC.Base.stimes :: forall b.
                                      Integral b =>
                                      b -> Free cls u -> Free cls u
        at Free.hs:57:10-67
    • In the expression: GHC.Base.$dmstimes @(Free cls u)
      In an equation for ‘GHC.Base.stimes’:
          GHC.Base.stimes = GHC.Base.$dmstimes @(Free cls u)
      In the instance declaration for ‘Semigroup (Free cls u)’
    • Relevant bindings include
        stimes :: b -> Free cls u -> Free cls u (bound at Free.hs:57:10)
   |
57 | instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

当我将其添加为实例的上下文时，它可以正常编译:

When I add this as context for the instance, it compiles fine:

instance (cls (Free cls u), forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

添加的上下文有些冗长，但是由于Free的全部要点是cls (Free cls u)始终是真实的，因此不会繁琐.

The added context is a little verbose, but since the whole point of Free is that cls (Free cls u) is always true, not onerous.

我不明白的是为什么 GHC需要能够为Semigroup的子类得出cls (Free cls u)的结论，以便编译Semigroup实例.我尝试用undefined替换(<>)的定义，并得到相同的错误，因此我认为问题不在于实现本身，而在于实例的声明.可能是由于QuantifiedConstraints的某些方面我不了解.

What I don't understand is why GHC needs to be able to conclude cls (Free cls u) for the subclass of Semigroup for the Semigroup instance to compile. I tried replacing the definition of (<>) with undefined and got the same error, so I think the issue is not in the implementation itself but in the declaration of the instance; probably due to some aspect of QuantifiedConstraints I don't understand.

推荐答案

错误消息指出这些错误来自sconcat和stimes的默认定义.量化的上下文就像instance一样:在您的instance Semigroup (Free cls v)中，就好像作用域中有一个instance cls v => Semigroup v一样.通过匹配选择instance. sconcat和stimes想要Semigroup (Free cls v)，因此它们与上下文instance forall z. cls z => Semigroup z相匹配，并在z ~ Free cls v之后成功，并进一步想要cls (Free cls v).即使我们也有递归instance _etc => Semigroup (Free cls v)，也会发生这种情况.记住，我们假设类型类实例是连贯的.使用量化上下文还是使用当前定义的实例应该没有什么区别，因此GHC只会选择感觉上要使用的任何实例.

The error messages state these errors come from the default definitions of sconcat and stimes. Quantified contexts act like instances: within your instance Semigroup (Free cls v), it's as if there is an instance cls v => Semigroup v in scope. instances are chosen by matching. sconcat and stimes want Semigroup (Free cls v), so they match that want against the context instance forall z. cls z => Semigroup z, succeed with z ~ Free cls v, and get a further wanted of cls (Free cls v). This happens even though we also have a recursive instance _etc => Semigroup (Free cls v) around. Remember, we assume that typeclass instances are coherent; there should be no difference whether the quantified context is used or the currently defined instance is used, so GHC just picks whichever instance it feels like using.

但是，这不是一个好情况.量化上下文与我们的实例重叠(实际上，它与每个 Semigroup实例重叠)，这令人震惊.如果尝试使用(<>) = const (Free0 _etc) ([1, 2] <> [3, 4])之类的方法，则会收到类似的错误，因为量化的上下文会使库中的实际instance Semigroup [a]蒙上阴影.我认为，包括来自 issue 14877 的一些想法，可以减轻这种不舒服的感觉:

However, this is not a good situation. The quantified context overlaps with our instance (actually, it overlaps with every Semigroup instance), which is alarming. If you try something like (<>) = const (Free0 _etc) ([1, 2] <> [3, 4]), you get a similar error, because the quantified context overshadows the real instance Semigroup [a] in the library. I think including some ideas from issue 14877 can make this less uncomfortable:

class (a => b) => Implies a b
instance (a => b) => Implies a b
instance (forall v. cls v `Implies` Semigroup v) => Semigroup (Free cls u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

在这里使用Implies意味着量化上下文不再与Semigroup (Free cls v)的需求匹配，而是通过递归释放.但是，约束背后的要求没有改变.本质上，我们保留了量化约束的需求片段，对于用户来说，Semigroup v应该由cls v隐含，同时为排放片段打上安全性，以便实施，因此它不会破坏我们的约束解析度.仍然可以并且必须使用Implies约束来证明(<>)中的Semigroup v约束，但是在用尽了明确的Semigroup实例之后，它被认为是最后的选择.

Using Implies here means that the quantified context no longer matches the want for Semigroup (Free cls v) which is instead discharged by recursion. However, the requirement behind the constraint doesn't change. Essentially, we keep the requirement fragment of the quantified constraint, for the user, that Semigroup v should be implied by cls v, while slapping a safety on the discharge fragment, for the implementation, so it doesn't muck up our constraint resolution. The Implies constraint still can and has to be used to prove the Semigroup v constraint in (<>), but it's considered as a last resort after the explicit Semigroup instances are exhausted.

这篇关于为什么使用QuantifiedConstraints指定类型类的子类也需要该子类的实例?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！