递归定义的实例和约束

Question

我一直在使用新的DataKinds扩展名将大小编码在其类型中的向量和矩阵。它基本上是这样的：

data Nat = Zero | Succ Nat
data Vector :: Nat -> * -> * where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a

现在我们想要典型的实例，例如 Functor 和 Applicative . Functor很简单：

instance Functor (Vector n) where
    fmap f VNil = VNil
    fmap f (VCons a v) = VCons (f a) (fmap f v)

但是对于Applicative实例，存在一个问题：我们不知道以纯值返回哪种类型。但是，我们可以在向量的大小上归纳定义实例：

instance Applicative (Vector Zero) where
    pure = const VNil
    VNil <*> VNil = VNil
instance Applicative (Vector n) => Applicative (Vector (Succ n)) where
    pure a = VCons a (pure a)
    VCons f fv <*> VCons a v = VCons (f a) (fv <*> v)

但是，即使此实例适用于所有向量，类型检查器也不知道这一点，因此我们每次使用该实例时都必须携带Applicative约束。

现在，如果这仅适用于Applicative实例，那将不是问题，但事实证明，在使用这些类型进行编程时，递归实例声明的技巧是必不可少的。例如，如果我们使用 TypeCompose 库将矩阵定义为行向量的向量，

type Matrix nx ny a = (Vector nx :. Vector ny) a

我们必须定义一个类型类并添加递归实例声明来实现转置和矩阵乘法。这导致我们每次使用代码时都必须携带的约束大量扩散，即使这些实例实际上适用于所有向量和矩阵(使约束变得无用(。

有没有办法避免携带所有这些限制？是否有可能扩展类型检查器，以便它可以检测这种感应结构？

Answer 1

pure的定义确实是问题的核心。它的类型应该是什么，完全量化和合格？

pure :: forall (n :: Nat) (x :: *). x -> Vector n x            -- (X)

不会这样做，因为在运行时没有可用的信息来确定pure应该发出VNil还是VCons。相应地，就目前的情况来看，你不能只拥有

instance Applicative (Vector n)                                -- (X)

你能做什么？好吧，使用Strathclyde Haskell增强功能，在Vec.lhs示例文件中，我定义了pure的前体

vec :: forall x. pi (n :: Nat). x -> Vector {n} x
vec {Zero}    x = VNil
vec {Succ n}  x = VCons x (vec n x)

使用pi类型，要求在运行时传递n的副本。这pi (n :: Nat).脱糖

forall n. Natty n ->

其中 Natty ，在现实生活中有一个更平淡无奇的名字，是单例 GADT 由

data Natty n where
  Zeroy :: Natty Zero
  Succy :: Natty n -> Natty (Succ n)

vec方程中的大括号只是将构造函数Nat转换为构造函数Natty。然后我定义以下恶魔实例(关闭默认函子实例(

instance {:n :: Nat:} => Applicative (Vec {n}) where
  hiding instance Functor
  pure = vec {:n :: Nat:} where
  (<*>) = vapp where
    vapp :: Vec {m} (s -> t) -> Vec {m} s -> Vec {m} t
    vapp  VNil          VNil          = VNil
    vapp  (VCons f fs)  (VCons s ss)  = VCons (f s) vapp fs ss

这仍然需要进一步的技术。约束{:n :: Nat:}脱糖到需要存在Natty n见证的东西，并且通过作用域类型变量的力量，与显式见证的{:n :: Nat:}传票相同。长手，就是这样

class HasNatty n where
  natty :: Natty n
instance HasNatty Zero where
  natty = Zeroy
instance HasNatty n => HasNatty (Succ n) where
  natty = Succy natty

我们将约束{:n :: Nat:}替换为 HasNatty n，将相应的项替换为 (natty :: Natty n) 。系统地做这个构造相当于在类型类Prolog中编写Haskell类型检查器的片段，这不是我的快乐想法，所以我使用计算机。

请注意，Traversable实例(请原谅我的成语括号和我的静默默认函子和可折叠实例(不需要这种抖动扑克

instance Traversable (Vector n) where
  traverse f VNil         = (|VNil|)
  traverse f (VCons x xs) = (|VCons (f x) (traverse f xs)|)

这就是获得矩阵乘法所需的全部结构，而无需进一步显式递归。

TL;DR 使用单一实例构造及其关联的类型类将所有递归定义的实例折叠到类型级数据的运行时见证中，您可以通过显式递归从中计算。

设计含义是什么？

GHC 7.4 具有类型促进技术，但 SHE 仍然具有单例构造pi类型。关于提升的数据类型，一个明显重要的事情是它们是封闭的，但这还没有真正干净地出现：单例见证的可构造性是这种封闭性的表现。不知何故，如果你有forall (n :: Nat).那么要求单例总是合理的，但这样做会对生成的代码产生影响：无论是像我的pi结构那样显式的，还是像{:n :: Nat:}字典中那样隐式的，都有额外的运行时信息需要吊索，以及相应的弱自由定理。

对于未来版本的 GHC 来说，一个悬而未决的设计问题是，如何管理类型级数据运行时见证的存在与否之间的这种区别。一方面，我们需要它们来约束。另一方面，我们需要对它们进行模式匹配。例如，pi (n :: Nat).是否应该意味着明确的

forall (n :: Nat). Natty n ->

或隐含的

forall (n :: Nat). {:n :: Nat:} =>

？当然，像Agda和Coq这样的语言都有这两种形式，所以也许Haskell应该效仿。当然还有取得进展的空间，我们正在努力！