47

在我最近的回答中，我碰巧打开了这个旧栗子（一个如此古老的程序，其中一半是莱布尼茨在 17 世纪编写的，而我父亲在 70 年代在计算机上编写的）。我将省略现代部分以节省空间。

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 和 and and ......但是有没有一种方法可以与类一起使用？）

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

4

4 回答 4

49

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

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 的一些相关特性，其中涉及类型黑客：

  • 它对类型级别的非终止是偏执的，这与它给用户带来的实际不便程度相去甚远。
  • 在考虑所有可用信息之前，它会愉快地做出关于类和实例的决定。
  • 它会尽职尽责地尝试检查你欺骗它承诺的任何事情。

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

然而，在这种情况下，与其将类型信息偷偷溜过 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 :: * -> *

由它自己的petard提升！

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

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)

我们现在对 sum 有一个表现得更好的递归：

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

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

于 2013-01-03T05:33:09.030 回答
19

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

import Data.Constraint

class Differentiable (f :: * -> *) where
  type D f :: * -> *
  witness :: p f -> Dict (Differentiable (D f))

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

这将让您在 Casey 的回答中采用解决方案的一般形式，但不会让编译器（或运行时）在归纳时永远旋转。

于 2013-01-04T00:37:28.963 回答
12

随着UndecidableSuperclassesGHC 8 中的新功能

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

作品。

于 2016-03-23T17:12:56.673 回答
9

这可以按照 Edward 建议的相同方式完成，即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

Sum 和 product 都需要来自其组件的两个导数的字典才能推断出字典的导数。

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通常只会让使用 get to make :: a -> f a，而不是 tomake :: 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
于 2014-08-30T00:20:56.713 回答