我可以约束一个types的家庭吗？
在我的这个最近的回答中 ，我碰巧揭开了这个古老的板栗（一个很老的程序，其中一半是由莱布尼兹在十七世纪写成的，七十年代由我父亲写在计算机上）。 为了节省空间，我会省略现代的一点。
class Differentiable f where type D f :: * -> * newtype K ax = K a newtype I x = I x data (f :+: g) x = L (fx) | R (gx) data (f :*: g) x = fx :&: gx instance Differentiable (K a) where type D (K a) = K Void instance Differentiable I where type DI = 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 cw | c -> w where ...
但为了尝试Differentiable的相同的技巧似乎…好…渐渐消失。
那么，有没有一个漂亮的解决scheme，让我可重复的可微性？ （我想我可以build立一个表示GADT和和…但是有没有一种方法可以与类一起工作？）
是否有任何明显的障碍与build议，我们应该能够要求在types（和，我想，数据）家庭的时候，我们宣布他们，然后检查实例满足他们？
当然，显而易见的是直接简单地写出所需的约束：
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'
所以，当试图描述types限制足以让GHC难以忍受时，往往是这样，我们必须采取某种欺骗手段。
回顾涉及typeshackery的GHC的一些相关特征：
- types级别的非终止与用户给实际带来的不便不相称是偏执的。
- 在考虑所有可用的信息之前，它将高兴地致力于关于类和实例的决定。
- 它会尽职地检查你所欺骗的任何东西。
这些是熟悉的旧的仿造通用实例的潜在原理，其中为了改进某些types的hackery结构的types推断行为，types与(~)事后统一。
然而，在这种情况下，我们需要以某种方式防止GHC注意到一个类别约束 ，而不是通过GHC偷偷types的信息，而这是一种完全不同的types … 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 DI = K ()
但是，如果我们提供一些废话，而不是：
instance Differentiable I where type DI = []
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)
我们现在有一个更好的recursion总和：
instance (Differentiable (D f), Differentiable (D g)) => Differentiable (f :+: g) where type D (f :+: g) = D f :+: D g
然而，对于产品来说，recursion的情况不能那么容易地被平分，并且在那里应用相同的改变改进了问题，只是因为我收到上下文缩减堆栈溢出而不是简单地挂在无限循环中。
你最好的select可能是使用constraints包来定义一些东西：
import Data.Constraint class Differentiable (f :: * -> *) where type D f :: * -> * witness :: pf -> Dict (Differentiable (D f))
那么你可以手动打开词典，只要你需要recursion。
这可以让你在Casey的答案中使用解决scheme的一般forms，但是没有编译器（或运行时）在归纳上永远旋转。
用GHC 8中新的UndecidableSuperclasses
class (Differentiable (D f)) => Differentiable (f :: * -> *) where
作品。
这可以用爱德华提出的小Dict实现的方式完成。 首先，让我们获得语言扩展和导入。
{-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy
TypeOperators仅用于您的示例问题。
小字典
我们可以做我们自己的小Dict执行。 Dict使用GADT和ConstraintKinds来捕获GADT的构造函数中的任何约束。
data Dict c where Dict :: c => Dict c
withDict和withDict2通过GADT上的模式匹配重新引入约束。 我们只需要能够用一个或两个约束来源来推理术语。
withDict :: Dict c -> (c => x) -> x withDict Dict x = x withDict2 :: Dict a -> Dict b -> ((a, b) => x) -> x withDict2 Dict Dict x = x
无限可分的types
现在我们可以谈论无限可微types，其衍生物也必须是可微的
class Differentiable f where type D f :: * -> * d2 :: pf -> Dict (Differentiable (D f)) -- This is just something to recover from the dictionary make :: a -> fa
d2代表该types的代理，并恢复字典以获得二阶导数。 代理允许我们轻松地指定我们正在讨论哪种types的d2 。 我们可以通过应用d来获得更深的字典：
d :: Dict (Differentiable t) -> Dict (Differentiable (D t)) d d1 = withDict d1 (d2 (pt (d1))) where pt :: Dict (Differentiable t) -> Proxy t pt = const Proxy
夺取冠军
多项式函数types，乘积，常数和零都是无限可微的。 我们将为每个types定义d2目击者
data K x = K deriving (Show) newtype I x = I x deriving (Show) data (f :+: g) x = L (fx) | R (gx) deriving (Show) data (f :*: g) x = fx :&: gx deriving (Show)
零和常量不需要任何额外的知识来捕获他们的派生Dict
instance Differentiable K where type DK = K make = const K d2 = const Dict instance Differentiable I where type DI = K make = I d2 = const Dict
总和和产品都需要来自两个组件的衍生词典都能够推导出它们的派生词典。
instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where type D (f :+: g) = D f :+: D g make = R . make d2 p = withDict2 df dg $ Dict where df = d2 . pf $ p dg = d2 . pg $ p pf :: p (f :+: g) -> Proxy f pf = const Proxy pg :: p (f :+: g) -> Proxy g pg = const Proxy instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where type D (f :*: g) = (D f :*: g) :+: (f :*: D g) make x = make x :&: make x d2 p = withDict2 df dg $ Dict where df = d2 . pf $ p dg = d2 . pg $ p pf :: p (f :*: g) -> Proxy f pf = const Proxy pg :: p (f :*: g) -> Proxy g pg = const Proxy
恢复字典
我们可以恢复字典的约束，否则我们将没有足够的信息来推断。 Differentiable f通常只允许使用make :: a -> fa ，但不能make :: a -> D fa或make :: a -> D (D f) a 。
make1 :: Differentiable f => pf -> a -> D fa make1 p = withDict (d2 p) make make2 :: Differentiable f => pf -> a -> D (D f) a make2 p = withDict (d (d2 p)) make
