时间戳

首页 > 解决方案 > 无法从上下文错误中推断出包含的约束

haskell - 无法从上下文错误中推断出包含的约束

问题描述

我正在努力在 Haskell 中重新创建一些基本的类别理论，但我遇到了一个问题。我的代码看起来像这样——非常标准。当然，这是隐藏 id 和 (.)。

class Category c where
    id :: forall a. c a a
    (.) :: c b d -> c a b -> c a d

-- Recover usual behavior of . and id
instance Category (->) where
    id = \x -> x
    (.) = \f g x -> f $ g x

class (Category c, Category d) => Functor c d f where
    fmap :: c a b -> d (f a) (f b)

data Comp f g x = Comp {getComp :: f (g x)}

instance (Category c, Category d, Category e,
      Functor d e f, Functor c d g) => Functor c e (Comp f g) where
    fmap = _

最后一个实例声明抛出了一个非常丑陋的错误，

• Could not deduce (Functor d0 e f)
  from the context: (Category c, Category d, Category e,
                     Functor d e f, Functor c d g)
bound by an instance declaration: ...
type variable d0 is ambiguous.

我已经玩了一段时间了，我不太清楚发生了什么。我对haskell很陌生。

标签： haskellcategory-theory

解决方案

让我们尝试修复您的代码

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
import Prelude hiding (Functor, fmap, id, (.))
import Data.Coerce

class Category c where
    id :: forall a. c a a
    (.) :: c b d -> c a b -> c a d

    coerceC :: Coercible a b => c a b

-- Recover usual behavior of . and id
instance Category (->) where
    id = \x -> x
    (.) = \f g x -> f $ g x

    coerceC = coerce

class (Category c, Category d) => Functor c d f where
    fmap :: c a b -> d (f a) (f b)

到目前为止，一切都很好。我在 中添加了coerceC方法Category，我们很快就会看到原因。（profunctors包定义.#和#.大致相同的目的：http ://hackage.haskell.org/package/profunctors-5.2.2/docs/Data-Profunctor-Unsafe.html#t:Profunctor ）

接下来，我们需要写一些具体的东西来获得洞察力。让我们试试[]函子：

instance Functor (->) (->) [] where
    fmap = map

请注意，这[]是一个 Functor (->) -> (->)。洞察力是函子确定/“知道”源和目标类别。我们可以通过FunctionalDependencies.

class (Category c, Category d) => Functor c d f | f -> c d where
    fmap :: c a b -> d (f a) (f b)

然后我们可以继续Comp举例。注意： - 这是newtype为了coerceC工作 - 我放弃了Category约束，因为它们暗示Functor

newtype Comp f g x = Comp {getComp :: f (g x)}

instance (Functor d e f, Functor c d g) => Functor c e (Comp f g) where
    fmap = _

现在我们得到一个类型孔错误，我们期待：

Found hole: _ :: c a b -> e (Comp f g a) (Comp f g b)

那就是我们可以填写

instance (Functor d e f, Functor c d g) => Functor c e (Comp f g) where
    fmap :: forall a b. c a b -> e (Comp f g a) (Comp f g b)
    fmap ab
        = coerceC
        . (fmap (fmap ab :: d (g a) (g b)) :: e (f (g a)) (f (g b)))
        . coerceC

（编写类型中间签名有助于使事情变得正确，在这种情况下，我们至少需要一个，因为coerceC它是非常多态的）

推荐阅读