实时持续队列总数 [英] Total real-time persistent queues

问题描述

Okasaki描述了使用类型

 数据Queue a = forall x可以在Haskell中实现的持久实时队列。 Queue 
 {front :: [a] 
，rear :: [a] 
，schedule :: [x] 
} 
  

增量循环保持不变

 长度计划=长度前部 - 后部
  

更多详情

如果您熟悉涉及的队列，可以跳过本节。

循环函数看起来像

  rotate :: [a]  - > [a]  - > [a]  - > [a] 
 rotate []（y：_）a = y：a 
 rotate（x：xs）（y：ys）a = 
x：rotate xs ys（y：a） 
  

它由智能构造函数调用

  exec :: [a]  - > [a]  - > [x]  - >队列
 exec fr（_：s）= Queue frs 
 exec fr [] =队列f'[] f'其中
 f'=旋转fr [] 
  

在每个队列操作之后。在 length s = length f - length r + 1 时总是调用smart构造函数，确保中的模式匹配旋转会成功的。

问题

我讨厌部分功能！我很想找到表达结构不变式的方法。通常的依赖矢量似乎是一个可能的选择：

  data Nat = Z | S Nat 
 
 data Vec n a where 
 Nil :: Vec'Z a 
 Cons :: a  - > Vec n a  - > Vec（'s n）a 
  

然后（也许）

 数据Queue a = forall x rl sl。队列
 {front :: Vec（sl：+ rl）a 
，rear :: Vec rl a 
，schedule :: Vec sl x 
} 
  

麻烦在于我一直无法弄清楚如何处理类型。为了提高效率，很可能需要少量的 unsafeCoerce 。但是，我还没有能够想出一个甚至可以模糊处理的方法。是否有可能在Haskell中做得很好？

解决方案

这是我得到的结果：



 打开导入函数
打开导入Data.Nat.Base 
打开导入Data.Vec 
 
 grotate：∀{ nm} {A：Set} 
  - > （B：ℕ - > Set）
  - > （∀{n}  - > A  - > B n  - > B（suc n））
  - > Vec A n 
  - > Vec A（suc n + m）
  - > B m 
  - > B（suc n + m）
 grotate B cons []（y∷ys）a = cons ya 
 grotate B cons（x∷xs）（y∷ys）a = grotate（B∘suc） cons xs ys（cons ya）
 
 rotate：∀{nm} {A：Set}  - > Vec A n  - > Vec A（suc n + m） - > Vec A m  - > Vec A（suc n + m）
 rotate = grotate（Vec _）_∷
 
记录Queue（A：Set）：Set 1其中
构造函数队列
字段
 {X}：设置
 {nm}：ℕ
 front：Vec A（n + m）
后面：Vec A m 
时间表：Vec X n 
 
打开导入Relation.Binary.PropositionalEquality 
打开导入Data.Nat.Properties.Simple 
 
 exec：∀{mn A}  - > Vec A（n + m） - > Vec A（suc m） - > Vec A n  - >队列A 
 exec {m} {suc n} fr（_∷s）= queue（subst（Vec _）（sym（+ -suc nm））f）rs 
 exec {m} fr [ ] =队列（带有零的f'）[] f'其中
与零= subst（Vec _∘suc）（sym（+ -right-identity m））
 without-zero = subst （+ -right-identity m）
 
 f'= without-zero（rotate f（with-zero r）[]）
  

rotate 定义为 grotate 出于同样的原因 reverse 是根据 foldl （或 枚举根据 genumerate ）：因为 Vec A（suc n + m）不是定义 Vec A （$ m code>），而（B∘suc）m 定义为 B（suc m） subst s），但我不确定类型： r 必须是非空的吗？

Okasaki describes persistent real-time queues which can be realized in Haskell using the type

data Queue a = forall x . Queue
  { front :: [a]
  , rear :: [a]
  , schedule :: [x]
  }

where incremental rotations maintain the invariant

length schedule = length front - length rear

More details

If you're familiar with the queues involved, you can skip this section.

The rotation function looks like

rotate :: [a] -> [a] -> [a] -> [a]
rotate [] (y : _) a = y : a
rotate (x : xs) (y : ys) a =
  x : rotate xs ys (y : a)

and it's called by a smart constructor

exec :: [a] -> [a] -> [x] -> Queue a
exec f r (_ : s) = Queue f r s
exec f r [] = Queue f' [] f' where
  f' = rotate f r []

after each queue operation. The smart constructor is always called when length s = length f - length r + 1, ensuring that the pattern match in rotate will succeed.

The problem

I hate partial functions! I'd love to find a way to express the structural invariant in the types. The usual dependent vector seems a likely choice:

data Nat = Z | S Nat

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

and then (perhaps)

data Queue a = forall x rl sl . Queue
  { front :: Vec (sl :+ rl) a
  , rear :: Vec rl a
  , schedule :: Vec sl x
  }

The trouble is that I haven't been able to figure out how to juggle the types. It seems extremely likely that some amount of unsafeCoerce will be needed to make this efficient. However, I haven't been able to come up with an approach that's even vaguely manageable. Is it possible to do this nicely in Haskell?

解决方案

Here is what I got:

open import Function
open import Data.Nat.Base
open import Data.Vec

grotate : ∀ {n m} {A : Set}
        -> (B : ℕ -> Set)
        -> (∀ {n} -> A -> B n -> B (suc n))
        -> Vec A n
        -> Vec A (suc n + m)
        -> B m
        -> B (suc n + m)
grotate B cons  []      (y ∷ ys) a = cons y a
grotate B cons (x ∷ xs) (y ∷ ys) a = grotate (B ∘ suc) cons xs ys (cons y a)

rotate : ∀ {n m} {A : Set} -> Vec A n -> Vec A (suc n + m) -> Vec A m -> Vec A (suc n + m)
rotate = grotate (Vec _) _∷_

record Queue (A : Set) : Set₁ where
  constructor queue
  field
    {X}      : Set
    {n m}    : ℕ
    front    : Vec A (n + m)
    rear     : Vec A m
    schedule : Vec X n

open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties.Simple

exec : ∀ {m n A} -> Vec A (n + m) -> Vec A (suc m) -> Vec A n -> Queue A
exec {m} {suc n} f r (_ ∷ s) = queue (subst (Vec _) (sym (+-suc n m)) f) r s
exec {m}         f r  []     = queue (with-zero f') [] f' where
 with-zero    = subst (Vec _ ∘ suc) (sym (+-right-identity m))
 without-zero = subst (Vec _ ∘ suc) (+-right-identity m)

 f' = without-zero (rotate f (with-zero r) [])

rotate is defined in terms of grotate for the same reason reverse is defined in terms of foldl (or enumerate in terms of genumerate): because Vec A (suc n + m) is not definitionally Vec A (n + suc m), while (B ∘ suc) m is definitionally B (suc m).

exec has the same implementation as you provided (modulo those substs), but I'm not sure about the types: is it OK that r must be non-empty?

这篇关于实时持续队列总数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！