如何在种类签名中要求功能依赖？

Question

考虑以下代码：

type CFunctor f = forall x y. (x -> y -> Constraint) -> f x -> f y -> Constraint

type MapList :: CFunctor []
class MapList c xs ys
instance MapList c '[] '[]
instance (c x y, MapList c xs ys) => MapList c (x ': xs) (y ': ys)

这很好用，但在某些情况下需要通过引入以下形式的函数依赖来“计算”：

class MapList c xs ys | c xs -> ys

有了函数依赖，我们有以下代码：

type CFunctor f = forall x y. (x -> y -> Constraint) -> f x -> f y -> Constraint

type MapList :: CFunctor []
class MapList c xs ys | c xs -> ys
instance MapList c '[] '[]
instance (c x y, MapList c xs ys) => MapList c (x ': xs) (y ': ys)

但这不会编译，并在最后一个实例中产生以下错误：

[typecheck] [E] • Illegal instance declaration for ‘MapList c (x : xs) (y : ys)’
    The liberal coverage condition fails in class ‘MapList’
      for functional dependency: ‘c xs -> ys’
    Reason: lhs types ‘c’, ‘x : xs’
      do not jointly determine rhs type ‘y : ys’
    Un-determined variable: y
• In the instance declaration for ‘MapList c (x : xs) (y : ys)’

这是有道理的：c + xs 由于 MapList c xs ys 的递归使用（具有函数依赖性）而确定 ys。但是 c + x ': xs 仅当 x 确定 y 时才确定 c + y ': ys，这是属性我们必须要求 class 被传递给 c.

但是我们如何调整 CFunctor 种类来满足这个要求呢？据我所知，没有种类签名中的词汇来讨论功能依赖性。我还有什么方法可以让这项工作成功吗？

Answer 1

一种解决方法是创建一个包装器 class，它只需要您的原始约束以及功能依赖性。在包装器中满足功能依赖的唯一方法是在原始 class.

中具有功能依赖

也就是说：

type FDep :: (a -> b -> Constraint) -> a -> b -> Constraint
class c x y => FDep c x y | c x -> y

现在我们可以写：

type MapList :: CFunctor []
class MapList c xs ys | c xs -> ys
instance MapList (FDep c) '[] '[]
instance (FDep c x y, MapList (FDep c) xs ys) => MapList (FDep c) (x ': xs) (y ': ys)

并对其进行类型检查。

当传入某个箭头时，例如：

class Fst ab a | ab -> a
instance Fst '(a, b) a

我们也简单地为它实例化FDep，以证明它具有相关的功能依赖：

instance Fst ab a => FDep Fst ab a

有点奇怪的是，我们的函子映射相对于 FDep-ness 是封闭的，如下图所示：

type MapList :: CFunctor []
class MapList c xs ys | c xs -> ys
instance MapList c xs ys => FDep (MapList c) xs ys

instance MapList (FDep c) '[] '[]
instance (FDep c x y, MapList (FDep c) xs ys) => MapList (FDep c) (x ': xs) (y ': ys)

这很好，因为它允许函子任意组合。它表明我们正在做某种奇怪的 Constraint 丰富的范畴论，其对象是种类，并且其态射在函数上依赖 classes.

这是一个使用我们的类型级别计算机的示例：

(^$) :: FDep c x y => Proxy c -> Proxy x -> Proxy y
(^$) _ _ = Proxy

class Fst ab a | ab -> a
instance Fst ab a => FDep Fst ab a

instance Fst '(a, b) a

test :: _
test = Proxy @(MapList (FDep Fst)) ^$ Proxy @'[ '(0, 1)]

导致的类型孔错误是：

[typecheck] [E] • Found type wildcard ‘_’ standing for ‘Proxy '[0]’
  To use the inferred type, enable PartialTypeSignatures
• In the type signature: test :: _

如何在种类签名中要求功能依赖？

How to require functional dependencies in kind signature?

haskell

typeclass