在我最近的这个答案中,我碰巧打开了这个老板栗(这个程序太旧了,其中一半是莱布尼兹在十七世纪写的,七十年代由我父亲在电脑上写的).我会省去现代的位以节省空间.
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必须是可区分的.当然,这些实例都尊重这个属性,你可以编写有趣的程序,它们可以利用这种能力来区分一个仿函数,在越来越多的地方拍摄漏洞:Taylor扩展,那种事情.
我希望能够说出类似的话
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而且......而且有没有一种方法适用于类？)
有没有明显的障碍,我们应该能够在声明它们时要求对类型(以及我想,数据)系列的约束,然后检查实例是否满足它们？
C. *_*ann 46
当然,显而易见的是直接编写所需的约束:
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的一些相关特征,其中涉及类型hackery:
这些是熟悉的旧仿伪通用实例的基本原理,其中类型是事后统一的(~),以便改进某些类型的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处理类上下文约束的方式,看起来我们可以通过pickier约束族来稍微修补一下.使用这个:
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
然而,递归情况不能轻易地对产品进行分割,并且应用相同的更改只会在我收到上下文减少堆栈溢出而不是简单地挂在无限循环中时改进了问题.
Edw*_*ETT 20
您最好的选择可能是使用constraints包定义一些东西:
import Data.Constraint
class Differentiable (f :: * -> *) where
type D f :: * -> *
witness :: p f -> Dict (Differentiable (D f))
然后你可以在需要递归时手动打开字典.
这可以让你在Casey的答案中使用解决方案的一般形状,但不会让编译器(或运行时)在归纳时永远旋转.
Ice*_*ack 11
随着UndecidableSuperclassesGHC 8 的新成功
class Differentiable (D f) => Differentiable (f :: Type -> Type) 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
现在我们可以讨论无限可微的类型,其衍生物也必须是可微分的
class Differentiable f where
type D f :: * -> *
d2 :: p f -> Dict (Differentiable (D f))
-- This is just something to recover from the dictionary
make :: a -> f a
d2获取该类型的代理,并恢复字典以获取二阶导数.代理允许我们轻松指定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
多项式函子类型,乘积,和,常数和零都是无限可微的.我们将为d2每种类型定义证人
data K x = K deriving (Show)
newtype I x = I x deriving (Show)
data (f :+: g) x = L (f x)
| R (g x)
deriving (Show)
data (f :*: g) x = f x :&: g x deriving (Show)
零和常数不需要任何额外的知识来捕获它们的衍生物 Dict
instance Differentiable K where
type D K = K
make = const K
d2 = const Dict
instance Differentiable I where
type D I = 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 -> f a,但不能使用make :: a -> D f a或make :: a -> D (D f) a.
make1 :: Differentiable f => p f -> a -> D f a
make1 p = withDict (d2 p) make
make2 :: Differentiable f => p f -> a -> D (D f) a
make2 p = withDict (d (d2 p)) make