总实时持久队列

Question

Okasaki描述了可以使用该类型在Haskell中实现的持久实时队列

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

增量旋转保持不变量

length schedule = length front - length rear

更多细节

如果您熟悉所涉及的队列,则可以跳过本节.

旋转功能看起来像

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] -> Queue a
exec f r (_ : s) = Queue f r s
exec f r [] = Queue f' [] f' where
  f' = rotate f r []

每次队列操作后.始终调用智能构造函数length s = length f - length r + 1,确保模式匹配rotate成功.

问题

我讨厌部分功能!我很想找到一种方法来表达类型中的结构不变量.通常的依赖向量似乎是一个可能的选择:

data Nat = Z | S Nat

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

然后(也许)

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

问题是我无法弄清楚如何兼顾类型.这似乎极有可能是一些量unsafeCoerce将需要使这个高效.但是,我还没有想出一个甚至模糊可控的方法.在Haskell中可以很好地完成这项工作吗？

Answer 1

这是我得到的:

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在以下方面被定义grotate为相同的原因reverse是在以下方面所定义foldl(或enumerate在以下方面genumerate):因为Vec A (suc n + m)是不definitionally Vec A (n + suc m),而(B ? suc) m是definitionally B (suc m).

exec具有与您提供的相同的实现(模数为substs),但我不确定类型:是否r可以非空？