haskell - 如何在实物签名中要求功能依赖？

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确定 ys由于 MapList c xs ys 的递归使用(具有功能依赖性)。但是 c + x ': xs确定 c + y ': ys仅当 x确定 y ，这是我们必须要求为 c 传入的类的属性.
但是我们如何调整 CFunctor好心要求这个？据我所知，没有实物签名中的词汇来讨论功能依赖关系。还有办法让我完成这项工作吗？

Answer 1

一种解决方法是创建一个包装类，该类只需要您的原始约束以及功能依赖项。满足包装器中的功能依赖的唯一方法是在原始类中具有功能依赖。
以机智:

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丰富的范畴论，其对象是种类，而态射是函数依赖的类。
这是使用我们的类型级计算机的一个工作示例:

(^$) :: 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 :: _