使用類型系統來檢查輸出與輸入列表的長度

Question

假設列表L的長度爲n在列表J中交織，長度爲n + 1。 我們想知道，對於J的每個元素，L中的哪個鄰居是更大的。 下面的函數需L作爲其輸入，併產生一個列表K，也長度的 n + 1個，使得K的我個元素是J的我 th元素的期望鄰居

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（一種新的語言對我來說），因爲我有興趣是 能夠通過類型系統證明這個不變量持有。隨着幫助 的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)這使我們能夠促進任何數據類型級別（有自己的那種），這樣類型級別土黃真是活該被定義爲一個常規的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工作，這是非常有用的定義爲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 

---

讓我知道如果這個回答你的問題 - 開始使用這樣的事情涉及到很多新的東西。