证明自然数的类型级加法的交换性

Question

我正在使用haskell为依赖类型编程提供的工具.我已经将一个代表自然数的GADT推广到了那个级别,并且为了增加自然数而建立了一个类型族.我还制作了你的标准"婴儿的第一个依赖类型数据类型"向量,参数化其长度和它包含的类型.代码如下:

data Nat where
    Z :: Nat
    S :: Nat -> Nat

type family (a :: Nat) + (b :: Nat) :: Nat where
    Z + n = n
    S m + n = S (m + n)

data Vector (n :: Nat) a where
    Nil :: Vector Z a
    Cons :: a -> Vector n a -> Vector (S n) a

此外,我做了一个append函数,它采用m向量,一个n-vetor并返回一个(m + n) - 向量.这可以和人们希望的一样有效.然而,只是为了它,我试图翻转它,所以它返回一个(n + m) - 矢量.这会产生编译器错误,因为GHC无法证明我的添加是可交换的.我还是比较新的打字家庭,所以我不知道如何自己写这个证明,或者如果你甚至可以用haskell做的话.

我最初的想法是以某种方式利用类型相等约束,但我不确定如何前进.

所以要明确:我想写这个功能

append :: Vector m a -> Vector n a -> Vector (n + m) a
append Nil xs         = xs
append (Cons x xs) ys = x `Cons` append xs ys

但它无法编译

    * Could not deduce: (n + 'Z) ~ n
      from the context: m ~ 'Z
        bound by a pattern with constructor: Nil :: forall a. Vector 'Z a,
                 in an equation for `append'

Answer 1

这是一个完整的解决方案.警告:包括一些无主.

我们从原始代码开始.

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, GADTs, PolyKinds #-}
{-# OPTIONS -Wall -O2 #-}
module CommutativeSum where

data Nat where
    Z :: Nat
    S :: Nat -> Nat

type family (a :: Nat) + (b :: Nat) :: Nat where
    'Z + n = n
    'S m + n = 'S (m + n)

data Vector (n :: Nat) a where
    Nil :: Vector 'Z a
    Cons :: a -> Vector n a -> Vector ('S n) a

旧的追加类型立即检查.

append :: Vector m a -> Vector n a -> Vector (m + n) a
append Nil xs         = xs
append (Cons x xs) ys = x `Cons` append xs ys

对于另一个附加,我们需要证明加法是可交换的.我们首先在类型级别定义相等性,利用GADT.

-- type equality, also works on Nat because of PolyKinds
data a :~: b where
   Refl :: a :~: a

我们引入单例类型,以便我们可以传递Nats和模式匹配.

-- Nat singleton, to reify type level parameters
data NatI (n :: Nat) where
  ZI :: NatI 'Z
  SI :: NatI n -> NatI ('S n)

我们可以将每个向量的长度关联为单个NatI.

-- length of a vector as a NatI
vecLengthI :: Vector n a -> NatI n
vecLengthI Nil = ZI
vecLengthI (Cons _ xs) = SI (vecLengthI xs)

现在是核心部分.我们需要n + m = m + n通过归纳证明.对于某些算术定律,这需要一些引理.

-- inductive proof of: n + Z = n  
sumZeroRight :: NatI n -> (n + 'Z) :~: n
sumZeroRight ZI = Refl
sumZeroRight (SI n') = case sumZeroRight n' of
   Refl -> Refl

-- inductive proof of: n + S m = S (n + m)
sumSuccRight :: NatI n -> NatI m -> (n + 'S m) :~: 'S (n + m)
sumSuccRight ZI _m = Refl
sumSuccRight (SI n') m  = case sumSuccRight n' m of
   Refl -> Refl

-- inductive proof of commutativity: n + m = m + n
sumComm :: NatI n -> NatI m -> (n + m) :~: (m + n)
sumComm ZI m = case sumZeroRight m of Refl -> Refl
sumComm (SI n') m = case (sumComm n' m, sumSuccRight m n') of
   (Refl, Refl) -> Refl

最后,我们可以利用上面的证据来说服GHC append按我们的意愿打字.请注意,我们可以使用旧类型重用该实现,然后说服GHC它也可以使用新类型.

-- append, with the wanted type
append2 :: Vector m a -> Vector n a -> Vector (n + m) a
append2 xs ys = case sumComm (vecLengthI xs) (vecLengthI ys) of
   Refl -> append xs ys

最后的评论.与完全依赖类型的语言(比如Coq)相比,我们不得不引入单身人士并花费更多的努力使它们发挥作用(Hasochism的"痛苦"部分).作为回报,我们可以简单地模式匹配Refl并让GHC弄清楚如何使用推导的方程式,而不会弄乱依赖匹配("快乐"部分).

总的来说,我认为使用完全依赖类型仍然更容易一些.如果/当GHC获得非擦除类型量词(pi n. ...超出forall n. ...)时,可能Haskell将变得更加方便.