haskell - 使用类型系统检查输出与输入列表的长度

Question

假设长度为 n 的列表 L 与长度为 n + 1 的列表 J 交错。 我们想知道，对于 J 的每个元素，L 中它的邻居中哪个元素更大。 以下函数将 L 作为输入，并生成一个列表 K，其长度也是 n + 1，使得 K 的第 i 个元素是 J 的第 i 个元素的所需邻居。

aux [] prev acc = prev:acc
aux (hd:tl) prev acc = aux tl hd ((max hd prev):acc)

expand row = reverse (aux row 0 [])

我可以非正式地向自己证明这个函数结果的长度(我 最初用 Ocaml 编写)比输入的长度大 1。但是我 跳到 Haskell(对我来说是一门新语言)，因为我对成为 能够通过类型系统证明这个不变量成立。有了。。的帮助 的this previous answer ， 我曾是 能够达到以下目的:

{-# LANGUAGE GADTs, TypeOperators, TypeFamilies #-}

data Z
data S n

type family (:+:) a b :: *
type instance (:+:) Z n = n
type instance (:+:) (S m) n = S (m :+: n)

-- A List of length 'n' holding values of type 'a'
data List a n where
    Nil  :: List a Z
    Cons :: a -> List a m -> List a (S m)

aux :: List a n -> a -> List a m -> List a (n :+: (S m))
aux Nil prev acc = Cons prev acc
aux (Cons hd tl) prev acc = aux tl hd (Cons (max hd prev) acc)

但是，最后一行会产生以下错误:

* Could not deduce: (m1 :+: S (S m)) ~ S (m1 :+: S m)
  from the context: n ~ S m1
    bound by a pattern with constructor:
               Cons :: forall a m. a -> List a m -> List a (S m),
             in an equation for `aux'
    at pyramid.hs:23:6-15
  Expected type: List a (n :+: S m)
    Actual type: List a (m1 :+: S (S m))
* In the expression: aux tl hd (Cons (max hd prev) acc)
  In an equation for `aux':
      aux (Cons hd tl) prev acc = aux tl hd (Cons (max hd prev) acc)
* Relevant bindings include
    acc :: List a m (bound at pyramid.hs:23:23)
    tl :: List a m1 (bound at pyramid.hs:23:14)
    aux :: List a n -> a -> List a m -> List a (n :+: S m)
      (bound at pyramid.hs:22:1)

看来我需要做的是告诉编译器(x :+: (S y)) ~ S (x :+: y)。这可能吗？

或者，有没有比类型系统更好的工具来解决这个问题？

Answer 1

首先，一些导入和语言扩展:

{-# LANGUAGE GADTs, TypeInType, RankNTypes, TypeOperators, TypeFamilies, TypeApplications, AllowAmbiguousTypes #-}

import Data.Type.Equality

我们现在有DataKinds (or TypeInType)这允许我们将任何数据提升到类型级别(具有其自己的类型)，因此类型级别自然值确实值得被定义为常规数据(哎呀，这个正是前面的 GHC 文档链接给出的激励示例!)。 List 类型没有任何变化，但 (:+:) 确实应该是一个封闭类型系列(现在超过了类似的纳特)。

-- A natural number type (that can be promoted to the type level)
data Nat = Z | S Nat

-- A List of length 'n' holding values of type 'a'
data List a n where
  Nil  :: List a Z
  Cons :: a -> List a m -> List a (S m)

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

现在，为了使证明适用于 aux，定义 singleton types 很有用。对于自然数。

-- A singleton type for `Nat`
data SNat n where
  SZero :: SNat Z
  SSucc :: SNat n -> SNat (S n)

-- Utility for taking the predecessor of an `SNat`
sub1 :: SNat (S n) -> SNat n
sub1 (SSucc x) = x

-- Find the size of a list
size :: List a n -> SNat n
size Nil = SZero
size (Cons _ xs) = SSucc (size xs)

现在，我们已经准备好开始证明一些东西了。来自 Data.Type.Equality , a :~: b 表示 a ~ b 的证明。我们需要证明关于算术的一件简单的事情。

-- Proof that     n + (S m) == S (n + m)
plusSucc :: SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSucc SZero _ = Refl
plusSucc (SSucc n) m = gcastWith (plusSucc n m) Refl

最后，我们可以使用 gcastWith在 aux 中使用这个证明。哦，您缺少 Ord a 约束。 :)

aux :: Ord a => List a n -> a -> List a m -> List a (n + S m)
aux Nil prev acc = Cons prev acc
aux (Cons hd tl) prev acc = gcastWith (plusSucc (size tl) (SSucc (size acc)))
                                      aux tl hd (Cons (max hd prev) acc)

-- append to a list
(|>) :: List a n -> a -> List a (S n)
Nil |> y = Cons y Nil
(Cons x xs) |> y = Cons x (xs |> y)

-- reverse 'List'
rev :: List a n -> List a n
rev Nil = Nil
rev (Cons x xs) = rev xs |> x

<小时/>

如果这能回答您的问题，请告诉我 - 开始处理此类事情涉及很多新东西。