我可以限制类型家庭吗？ [英] Can I constrain a type family?

问题描述

在我最近的这个答案中，我碰巧打开了这个古老的板栗（一个程序如此老旧，一半它在十七世纪由莱布尼兹写成，并在七十年代由我的父亲写在计算机上）。

  class差异化f其中
 type D f :: * - > * 
 
 newtype K a x = K a 
 newtype I x = I x 
 data（f：+：g）x = L（f x）
 | R（gx）
 data（f：*：g）x = fx：&g; 
 
 instance可微分（K a）其中
类型D（K a）= K无效
实例可微分I其中
类型DI = K（）
实例（Differentiable f，Differentiable g）=>可微（f：+：g）其中
类型D（f：+：g）= D f：+：D g 
实例（Differentiable f，Differentiable g）=>差分（f：*：g）其中
类型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其中
类型WhatsIn c 
实例Ord（WhatsIn c）
 ... 
  

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

  class Ord w => SortContainer c w | c  - > w其中... 
  

但为了尝试 Differentiable 似乎......好......被消除了。



那么，是否有一个漂亮的解决方法可以获得可重复的可微分性？ （我想我可以构建一个表示GADT和和和......但有没有一种方法可以与类一起工作？）



这个建议是否存在明显的障碍我们应该能够在声明它们时要求对类型（以及我认为是数据）族的约束，然后检查实例是否满足它们？


解决方案

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

  class（Differentiable D f））=>差异化（f :: *  - > *）其中
  

唉，GHC对此感到厌烦并拒绝：

  ConstrainTF.hs：17：1：
在类声明中循环（通过超类）：
可差异 - >可区分的
在`Differentiable'类的声明中
  

所以，试图描述类型约束的幻想足以让GHC不屈不挠，我们必须诉诸某种欺骗手段。回顾GHC涉及类型hackery的一些相关特征： / p>

• 类型级别的非终止与用户给实际带来的不便无关。 b
• 在考虑所有可用信息之前，它会高兴地致力于决定类和实例。


• 它会尽职地检查你欺骗它的任何事情， 。
  
  
  

  这些都是熟悉的旧仿人通用实例的迂回原则，其中类型与（〜）以改进某些类型hackery缺点的类型推断行为然而，在这种情况下，我们需要以某种方式防止GHC注意到，而不是偷窃类型过去的GHC信息。

  >类约束，这是一种完全不同的类型...... heeeey，waaaitaminute ....
  
  

    import GHC.Prim 
   
   type family DiffConstraint（f :: *  - > *）::约束
  类型实例DiffConstraint f =可区分的f 
   
   class（DiffConstraint（D f））=> Differentiable（f :: *  - > *）其中
   type D f :: *  - > * 
    

  葫芦丝！ >这也是真正的交易。这些都被接受了，正如你所希望的那样：
  
  

    instance Differentiable（K a）其中
   type D（K a ）= K无效
  实例差异性I其中
  类型DI = K（）
    

  但是如果我们提供一些废话：
  
  

    instance可区分的我其中
   type DI = [] 
    

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

    ConstrainTF.hs：29：10：
  由于实例声明的超类产生的（Differentiable []）
  没有实例
  可能的修正：添加一个实例声明（Differentiable []）
  在Differentiable I的实例声明中
    

  当然有一个小障碍，那就是：
  
  pre $ instance（Differentiable f，Differentiable g ）=>可区分的（f：+：g）其中
类型D（f：+：g）= D f：+：D g


  ...事实上不如我们所说的那样，因为我们已经告诉GHC检查，无论何时（f：+：g） Differentiable ，所以（D f：+：D g）或者完全可以）。
  
  

  避免这种情况的最简单方法通常是在一堆明确的基本情况下进行样板化，但是这里GHC似乎意图随时分散一个 Differentiable 约束出现在实例上下文中。我会认为它是不必要地急于以某种方式检查实例约束，并且可能会用另一层欺骗来分散很长时间，但是我不能立即确定从哪里开始，并且已经用尽了我今晚的午夜类型hackery的能力。 / p>
  
  

  ---

  
  
  

  一些关于#haskell的IRC讨论在GHC如何处理类上下文约束方面略微推敲了我的记忆，我们可以通过一个更挑剔的约束族来修补一些东西。使用这个：
  
  

    type family DiffConstraint（f :: *  - > *）::约束
  类型实例DiffConstraint （K a）=可微分（K a）
  类型实例DiffConstraint I =可微分I 
  类型实例DiffConstraint（f：+：g）=（可微分f，可微分g）
    

  我们现在有更好的递归递归：

<$ p （可微（D f），可微（D g））=>可区分的（f：+：g）其中
类型D（f：+：g）= D f：+：D g


  然而，对于产品而言，递归的情况并非如此简单，只要我收到上下文缩减堆栈溢出而不是简单地挂在无限循环中，在那里应用相同的更改就可以改善问题。
  

  In this recent answer of mine, I happened to crack open this old chestnut (a program so old, half of it was written in the seventeenth century by Leibniz and written on a computer in the seventies by my dad). I'll leave out the modern bit to save space.

  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)
  

  Now, here's the frustrating thing. I don't know how to stipulate that D f must itself be differentiable. Certainly, these instances respect that property, and there might well be fun programs you can write which make use of the ability to keep differentiating a functor, shooting holes in more and more places: Taylor expansions, that sort of thing.

  I'd like to be able to say something like

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

  and require a check that instance declarations have type definitions for which the necessary instances exist.

  Maybe more mundane stuff like

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

  would also be nice. That, of course, has the fundep workaround

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

  but to attempt the same trick for Differentiable seems... well... involuted.

  So, is there a nifty workaround that gets me repeatable differentiability? (I guess I could build a representation GADT and and and... but is there a way that works with classes?)

  And are there any obvious snags with the suggestion that we should be able to demand constraints on type (and, I suppose, data) families when we declare them, then check that the instances satisfy them?

  解决方案

  Certainly, the obvious thing would be to simply write the desired constraint directly:

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

  Alas, GHC gets huffy about that and refuses to play along:

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

  So, as is often the case when attempting to describe type constraints fancy enough to leave GHC recalcitrant, we must resort to some manner of underhanded trickery.

  Recalling some relevant features of GHC where type hackery is involved:

  • It is paranoid about type-level nontermination far out of proportion to the actual inconvenience it entails for the user.
  • It will cheerfully commit itself to decisions about classes and instances before it has considered all the information available.
  • It will dutifully attempt to check anything you've tricked it into committing to.

  These are the devious principles underlying the familiar old faux-generic instances, where types are unified post-hoc with (~) in order to improve the type inference behavior of certain type hackery constructs.

  In this case, however, rather than sneaking type information past GHC, we would need to somehow prevent GHC from noticing a class constraint, which is an entirely different kind of... 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 :: * -> *
  

  Hoist by its own petard!

  It's the real deal, too. These are accepted, as you'd hope:

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

  But if we offer it some nonsense instead:

  instance Differentiable I where
    type D I = []
  

  GHC presents us with precisely the error message we'd like to see:

  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'
  

  There is one small snag, of course, namely that this:

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

  ...turns out to be less than well-founded, as we've told GHC to check that, whenever (f :+: g) is Differentiable, so is (D f :+: D g), which does not end well (or at all).

  The easiest way to avoid this would usually be to boilerplate on a pile of explicit base cases, but here GHC seems intent on diverging any time a Differentiable constraint appears in an instance context. I would assume it's being unnecessarily eager in checking instance constraints somehow, and could perhaps be distracted long enough with another layer of trickery, but I'm not immediately sure where to start and have exhausted my capacity for post-midnight type hackery tonight.

  ---

  A bit of IRC discussion on #haskell managed to jog my memory slightly on how GHC handles class context constraints, and it appears we can patch things up a little bit by means of a pickier constraint family. Using this:

  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)
  

  We now have a much more well-behaved recursion for sums:

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

  The recursive case cannot be so easily bisected for products, however, and applying the same changes there improved matters only insofar as I received a context reduction stack overflow rather than it simply hanging in an infinite loop.

  这篇关于我可以限制类型家庭吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！