13

我一直在使用新的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实例有一个问题：我们不知道在 pure 中返回什么类型。但是，我们可以根据向量的大小归纳定义实例：

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

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

有没有办法避免必须进行所有这些限制？是否可以扩展类型检查器以检测这种归纳结构？

4

1 回答 1

15

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

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

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

instance Applicative (Vector n)                                -- (X)

你能做什么？好吧，使用Strathclyde Haskell Enhancement在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构造函数。然后我定义了以下恶魔实例（关闭默认的 Functor 实例）

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实例（请原谅我的成语括号和我的默认 Functor 和 Foldable 实例）不需要这样的诡计

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 应该效仿。当然还有进步的空间，我们正在努力！

于 2012-05-10T09:22:00.293 回答