haskell - 我可以限制类型族吗？

Question

在 this recent answer of mine ，我碰巧 pry 开这个老栗子(这么老的程序，有一半是十七世纪莱布尼茨写的，七十年代我爸在电脑上写的)。为了节省空间，我将省略现代部分。

class Differentiable f where
  type D f :: * -> *

newtype K a     x  = K a
newtype I       x  = I x
data (f :+: g)  x  = L (f x)
                   | R (g x)
data (f :*: g)  x  = f x :&: g x

instance Differentiable (K a) where
  type D (K a) = K Void
instance Differentiable I where
  type D I = K ()
instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g
instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
  type D (f :*: g) = (D f :*: g) :+: (f :*: D g)

现在，令人沮丧的事情来了。我不知道如何规定 D f 必须本身是可微分的。当然，这些实例尊重该属性，并且您很可能可以编写有趣的程序，这些程序利用不断微分仿函数的能力，在越来越多的地方射击漏洞:泰勒展开式，诸如此类。

我希望能够说这样的话

class Differentiable f where
  type D f
  instance Differentiable (D f)

并要求检查实例声明是否具有存在必要实例的类型定义。

也许更平凡的东西，比如

class SortContainer c where
  type WhatsIn c
  instance Ord (WhatsIn c)
  ...

也不错。当然，这有fundep解决方法

class Ord w => SortContainer c w | c -> w where ...

但是尝试对Differentiable使用同样的技巧似乎……嗯……很复杂。

那么，有没有一种巧妙的解决方法可以让我获得可重复的可微性？ (我想我可以构建一个表示 GADT 和并且......但是有没有一种方法可以与类一起使用？)

当我们声明类型(以及我想的数据)族时，我们应该能够要求对它们进行约束，然后检查实例是否满足它们，这个建议是否存在任何明显的障碍？

Answer 1

当然，显而易见的是直接编写所需的约束:

class (Differentiable (D f)) => Differentiable (f :: * -> *) where

唉，GHC 对此很生气并且拒绝配合:

ConstrainTF.hs:17:1:
    Cycle in class declaration (via superclasses):
      Differentiable -> Differentiable
    In the class declaration for `Differentiable'

因此，正如通常的情况一样，当试图描述足够奇特的类型约束而使 GHC 难以抗拒时，我们必须诉诸某种不正当手段。

回顾一下涉及类型黑客的 GHC 的一些相关功能:

• 它对类型级不终止的偏执远远超出了它给用户带来的实际不便。
• 在考虑所有可用信息之前，它会愉快地做出有关类和实例的决策。
• 它会尽职尽责地尝试检查您欺骗它 promise 的任何内容。

这些是熟悉的旧仿通用实例背后的狡猾原理，其中类型与 (~) 事后统一，以改进某些类型黑客构造的类型推断行为。

然而，在这种情况下，我们需要以某种方式阻止 GHC 注意到类约束，而不是偷偷地通过 GHC 类型信息，这是一个完全不同的类型...heeeey, waaaitamin...

import GHC.Prim

type family DiffConstraint (f :: * -> *) :: Constraint
type instance DiffConstraint f = Differentiable f

class (DiffConstraint (D f)) => Differentiable (f :: * -> *) where
  type D f :: * -> *

自取其辱!

这也是真正的交易。正如您所希望的那样，这些被接受:

instance Differentiable (K a) where
  type D (K a) = K Void
instance Differentiable I where
  type D I = K ()

但是如果我们提供一些废话来代替:

instance Differentiable I where
  type D I = []

GHC 向我们提供了我们希望看到的错误消息:

ConstrainTF.hs:29:10:
    No instance for (Differentiable [])
      arising from the superclasses of an instance declaration
    Possible fix: add an instance declaration for (Differentiable [])
    In the instance declaration for `Differentiable I'

当然，有一个小障碍，即:

instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g

...结果证明没有充分的依据，因为我们已经告诉 GHC 进行检查，只要 (f :+: g) 是 Differentiable ，(D f :+: D g) 也是如此，但结局并不好(或根本没有)。

避免这种情况的最简单方法通常是在一堆显式基本案例上编写样板，但这里 GHC 似乎有意在实例上下文中出现 Differentiable 约束时出现分歧。我认为它以某种方式不必要地急于检查实例约束，并且可能会因另一层欺骗而分散足够长的时间，但我不确定从哪里开始，并且今晚已经耗尽了我的午夜后类型黑客攻击的能力。

<小时/>

#haskell 上的一些 IRC 讨论成功地唤起了我对 GHC 如何处理类上下文约束的内存，看来我们可以通过更挑剔的约束系列来修补一些事情。使用这个:

type family DiffConstraint (f :: * -> *) :: Constraint
type instance DiffConstraint (K a) = Differentiable (K a)
type instance DiffConstraint I = Differentiable I
type instance DiffConstraint (f :+: g) = (Differentiable f, Differentiable g)

我们现在有一个表现更好的求和递归:

instance (Differentiable (D f), Differentiable (D g)) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g

然而，对于产品来说，递归情况不能那么容易地一分为二，并且仅当我收到上下文缩减堆栈溢出而不是简单地卡在无限循环中时，应用相同的更改才可以改善问题。