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

Question

假设长度为n的列表L 在列表J中交织,长度为n + 1.我们想知道,对于J的每个元素,L的哪个邻居是更大的.下面的函数需L作为其输入,并产生一个列表K,也长度的 n + 1个,使得我个钾元素是所期望的邻居我个J.的元件

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

expand row = reverse (aux row 0 [])

我可以非正式地向自己证明,这个函数(我最初在Ocaml中写的)的结果长度比输入的长度大.但我跳到Haskell(一种新语言),因为我有兴趣通过类型系统证明这个不变量.在前面的答案的帮助下,我能够得到以下内容:

{-# 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(或TypeInType)允许我们将任何数据提升到类型级别(有自己的类型),所以类型级别自然真的值得定义为常规data(哎呀,这正是以前链接到GHC文档给出了!).你的List类型没有什么变化,但(:+:)真的应该是一个封闭的类型家庭(现在是类似的东西Nat).

-- 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,为自然数定义单例类型是有用的.

-- 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

让我知道如果这回答了你的问题 - 开始这类事情涉及很多新的东西.