伊德里斯 - 矢量隊列和重寫規則

我想實現像在伊德里斯功能隊列，但它攜帶在類型元素的數目 - 如Queue ty n m (n+m)其中n是一個Vect n ty元素的數量，m是第二個元素Vect m ty，而(n+m)是總元素。伊德里斯 - 矢量隊列和重寫規則

的問題是，我遇到了問題與操縱這些尺寸爲隱式參數時應用重寫規則：

module Queue 

import Data.Vect as V 

data Queue : Type -> Nat -> Nat -> Nat -> Type where 
    mkQueue : (front : V.Vect n ty) 
      -> (back : V.Vect m ty) 
      -> Queue ty n m (n + m) 

%name Queue queue 

top : Queue ty n m (S k) -> ty 
top {n = S j} {m} {k = j + m} (mkQueue front back) = 
    V.head front 
top {n = Z} {m = S j} {k = j} (mkQueue front back) = 
    V.head $ V.reverse back 

bottom : Queue ty n m (S k) -> ty 
bottom {m = S j} {n} {k = n + j} (mkQueue front back) = 
    ?some_rewrite_1 (V.head back) 
bottom {m = Z} {n = S j} {k = j} (mkQueue front back) = 
    ?some_rewrite_2 (V.head $ V.reverse front)

top作品，但bottom沒有。看起來我需要提供plusZeroRightNeutral和plusRightSuccRight重寫，但我不確定在哪裏放置這些內容，或者是否有其他選項。以下是錯誤消息：

錯誤上的bottom第一行：

  Type mismatch between 
       Queue ty n (S j) (n + S j) (Type of mkQueue front back) 
     and 
       Queue ty n (S j) (S (n + j)) (Expected type) 

     Specifically: 
       Type mismatch between 
         plus n (S j) 
       and 
         S (n + j)

錯誤上的bottom秒行：

  Type mismatch between 
       Queue ty (S j) 0 (S j + 0) (Type of mkQueue front back) 
     and 
       Queue ty (S j) 0 (S j) (Expected type) 

     Specifically: 
       Type mismatch between 
         plus (S j) 0 
       and 
         S j

單獨的大小告訴我，當我需要旋轉兩Vect s，整體大小告訴我什麼時候我有一個空的或非空的Queue，所以如果可能的話我想跟蹤所有的信息。

來源

2016-12-16 nomicflux

作爲注意，我不會將'front' /'back'大小添加到該類型，只是總大小;我認爲前者是一個應該從客戶端代碼隱藏的實現/表示細節。 – Cactus

@Cactus：我一直在把我的代碼移動到那個格式，所以我只需要'Queue ty k'，其中'MkQueue'中的'k'仍然是'（n + m）'， 'Vect's，因爲這是一個不變的我想保證。不過，我的問題是，我不能拉'{N}'和'{M}'在正確的地方implicits爲'top'和'這裏bottom'。仍然在這個問題上.... – nomicflux

相關：[總實時持久隊列]（http://stackoverflow.com/questions/36611533/total-real-time-persistent-queues）。 – user3237465

解決這個問題的一種可能的方法是破壞n以及。這一次，伊德里斯的理解是，最後一個參數不爲零，它基本上是抱怨：

total 
bottom : Queue ty n m (S k) -> ty 
bottom {m = S m} {n = S n} (MkQueue _ back) = V.head back 
bottom {m = S m} {n = Z} (MkQueue _ back) = V.head back 
bottom {m = Z} {n = S n} (MkQueue front _) = V.head $ V.reverse front 
bottom {m = Z} {n = Z} (MkQueue _ _) impossible

作爲一個方面說明，我建議讓top功能合計：

total 
top : Queue ty n m (S k) -> ty 
top {n = S n}   (MkQueue front _) = V.head front 
top {n = Z} {m = S m} (MkQueue _ back) = V.head $ V.reverse back 
top {n = Z} {m = Z} (MkQueue _ _) impossible

來源

2016-12-16 16:10:50

優秀 - 完美工作，解決了問題，關於總體的說明也很有用。謝謝！ – nomicflux

伊德里斯 - 矢量隊列和重寫規則

回答

相關問題