递归定义的实例和约束

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 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实例)不需要这样的jiggery pokery

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应该效仿.肯定有进步的空间,我们正在努力!