我可以限制类型家庭吗?

在我最近的这个回答中,我碰巧揭开了这个老栗子(一个很古老的程序,其中一半是由莱布尼茨在十七世纪写成的,七十年代由我父亲写在计算机上)。 为了节省空间,我会省略现代的一点。

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)

并且需要检查实例声明是否具有必需实例所在的type定义。

也许更类似世俗的东西

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

也会很好。 当然,这有fundep解决方法

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

但为了尝试Differentiable的相同技巧,似乎......很好......渐入佳境。

那么,是否有一个漂亮的解决方法,可以获得可重复的可区分性? (我想我可以建立一个表示GADT和和和...但有没有一种方法可以与类一起工作?)

是否有任何明显的障碍与建议,我们应该能够要求对类型(和,我想,数据)家庭时,我们声明他们,然后检查实例满足他们?


当然,显而易见的是直接简单地写出所需的约束条件:

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难以忍受时,往往会出现这种情况,我们必须采取某种欺骗手段。

回顾涉及类型hackery的GHC的一些相关特征:

  • 对于类型级别的非终止而言,它与使用者带来的实际不便无关。
  • 在考虑所有可用信息之前,它会高兴地致力于对类和实例的决策。
  • 它会尽职尽责地检查你欺骗它承诺的任何事情。
  • 这些是熟悉的旧仿造泛型实例的迂回原则,其中为了改进某些类型hackery结构的类型推断行为,类型与(~)事后统一。

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

    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约束出现在实例上下文中时随时分歧。 我会认为它是不必要地急于以某种方式检查实例约束的,并且可能会被另一层欺骗性分散很长时间,但我不能立即确定从哪里开始,并且已经耗尽了我今晚的午夜类型hackery的能力。


    关于#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
    

    然而,对于产品来说,递归的情况并不是那么容易被分割,并且在那里应用相同的改变改进了事情,只是因为我收到了上下文缩减堆栈溢出而不是简单地挂在无限循环中。


    你最好的选择可能是使用constraints包来定义一些东西:

    import Data.Constraint
    
    class Differentiable (f :: * -> *) where
      type D f :: * -> *
      witness :: p f -> Dict (Differentiable (D f))
    

    那么您可以在需要递归时手动打开字典。

    这可以让你在Casey的答案中使用解决方案的一般形式,但是没有编译器(或运行时)在归纳上永远旋转。


    使用GHC 8中的新UndecidableSuperclasses

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

    作品。

    链接地址: http://www.djcxy.com/p/66625.html

    上一篇: Can I constrain a type family?

    下一篇: Partially lift with liftIO