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

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 ': ysifx确定y，这是我们必须要求传入的类的属性c。

但是我们如何调整CFunctor种类来满足这个需求呢？据我所知，没有种类签名的词汇来讨论功能依赖。我还有办法让这个工作吗？

Answer 1

一种解决方法是创建一个包装类，它只需要您的原始约束是什么，再加上函数依赖性。满足包装器中的函数依赖关系的唯一方法是在原始类中具有函数依赖关系。

\n

以机智：

\n

type FDep :: (a -> b -> Constraint) -> a -> b -> Constraint\nclass c x y => FDep c x y | c x -> y\n

\n

现在我们可以写：

\n

type MapList :: CFunctor []\nclass MapList c xs ys | c xs -> ys\ninstance MapList (FDep c) '[] '[]\ninstance (FDep c x y, MapList (FDep c) xs ys) => MapList (FDep c) (x ': xs) (y ': ys)\n

\n

并进行类型检查。

\n

当传递一些箭头时，例如：

\n

class Fst ab a | ab -> a\ninstance Fst '(a, b) a\n

\n

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

\n

instance Fst ab a => FDep Fst ab a\n

\n

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

\n

type MapList :: CFunctor []\nclass MapList c xs ys | c xs -> ys\ninstance MapList c xs ys => FDep (MapList c) xs ys\n\ninstance MapList (FDep c) '[] '[]\ninstance (FDep c x y, MapList (FDep c) xs ys) => MapList (FDep c) (x ': xs) (y ': ys)\n

\n

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

\n

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

\n

(^$) :: FDep c x y => Proxy c -> Proxy x -> Proxy y\n(^$) _ _ = Proxy\n\nclass Fst ab a | ab -> a\ninstance Fst ab a => FDep Fst ab a\n\ninstance Fst '(a, b) a\n\ntest :: _\ntest = Proxy @(MapList (FDep Fst)) ^$ Proxy @'[ '(0, 1)]\n

\n

导致的类型孔错误为：

\n

[typecheck] [E] \xe2\x80\xa2 Found type wildcard \xe2\x80\x98_\xe2\x80\x99 standing for \xe2\x80\x98Proxy '[0]\xe2\x80\x99\n  To use the inferred type, enable PartialTypeSignatures\n\xe2\x80\xa2 In the type signature: test :: _\n

\n