CompactStack.idr

{-

This is a proof about the amortized complexity of a
stack data structure which works by concatenating and
splitting arrays whose lengths are powers of two.
(Stack, push, pop).

(This is a formalization of https://github.com/treeowl/compact-sequences
where I already wrote this in Coq, but linear types would help make it more
precise.)

This "proof" is really a linearly and dependently typed program where:

1. using linear types, time resources ("debits") are represented explicitly as
   values that can be moved but not duplicated, they are stored in
   a "debit structure" which mirrors the structure of the stack;

2. using dependent types, we maintain invariants that bound the number
   of debits that can be stored in any place, from which we can
   deduce the amortized complexity bounds.

The main definitions in this file:

- The implementation

  + The type Stack_
  + push_
  + pop_

- The proof

  + The type DStack_ of stacks annotated with debits ("time units")
    representing the cost of append and split operations to be paid incrementally.
    (A little oversimplified; the true explanation also deals with laziness.)
  + dpush_, a version of push_ that deals with debits.
  + dpop_, a version of pop_ that deals with debits.

  Every time an append or split happens in push_ and pop_, i debits must be generated
  in dpush_ and dpop_. At the same time, dpush_ and dpop_ are allowed to remove
  up to (1 + depth_ s) debits from the debit structure. The constraints inside the
  definition of DStack_ ensure that debits only exist in bounded quantities.

(The underscores in identifiers mean that they are really "internal" functions,
handling details that would be hidden from the point of view of a user,
notably the index i representing the length of vectors. But from the point of view
of the implementation, they are where the work happens.)
-}

{- PROBLEM

dpop_ doesn't typecheck. I think the essence of the problem is best summarized by the following highly minimized example:

https://gist.github.com/Lysxia/9320064ae303d177a69fcfa02502fe85

Part of the difficulty might be the requirement that s is irrelevant (multiplicity 0). I could reasonably drop it,
but I am still running into obstacles:

https://gist.github.com/Lysxia/2e9f73004c5ba05cb2f9ff50d79ca9d7

-}

module CompactStack

import Data.Nat


-- 0. General definitions


-- 0.1. Linearity

infixr 0 #->, ?->

(#->) : Type -> Type -> Type
a #-> b = (1 _ : a) -> b

(?->) : Type -> Type -> Type
a ?-> b = (0 _ : a) -> b


infixl 60 :>
infixl 70 :*

-- Linear pairs. "Tensor" in linear logic.
-- Nesting them creates heterogeneous lists, snoc lists because of the associativity.
data (:*) : Type -> Type -> Type where
  (:>) : a #-> b #-> a :* b

first : (a #-> b) #-> a :* c #-> b :* c
first f (x :> y) = f x :> y


infixl 40 >>=+, >>=-

(>>=+) : a :* b #-> (b #-> c :* d) #-> a :* c :* d
(>>=+) (x :> y) f = let z :> w = f y in x :> z :> w

(>>=-) : a :* b #-> (b #-> ()) #-> a
(>>=-) (x :> y) f = let () = f y in x

interface Consumable a where
  consume : a #-> ()


infixl 60 :+

data (:+) : Type -> Type -> Type where
  L : a #-> a :+ b
  R : b #-> a :+ b


data Maybe' : Type -> Type where
  Nothing' : Maybe' a
  Just' : a #-> Maybe' a

-- 0.2. Equality

eqApp :
  {0 f : a -> b} -> {0 g : a -> b} -> (f = g) ?->
  {0 x : a} -> {0 y : a} -> (x = y) ?->
  (f x = g y)
eqApp Refl Refl = Refl

infixl 70 `eqApp`

rw : (a = b) ?-> a #-> b
rw Refl x = x


-- 0.3. Arithmetic

plusLteMonotone : a `LTE` c #-> b `LTE` d #-> a + b `LTE` c + d

-- The name refers to the adjunction (S -| pred)
lteAdjPred : S n `LTE` m -> n `LTE` pred m
lteAdjPred (LTESucc p) = p

invertPred : S n `LTE` m -> (S (pred m) = m)
invertPred (LTESucc _) = Refl

t2 : 1 `LTE` i ?-> 1 `LTE` 2 * i
t2 p = rewrite sym (invertPred p) in LTESucc LTEZero

t2' : 1 `LTE` i ?-> 1 `LTE` i + i
t2' p = rewrite sym (invertPred p) in LTESucc LTEZero


-- 1. Compact stacks


-- 1.1. Vectors

-- (Vec i a) is the type of vectors of length i, with elements of type a
data Vec : Nat -> Type -> Type

singleton : a #-> Vec 1 a
extract : Vec 1 a #-> a
append : Vec i a #-> Vec i a #-> Vec (2 * i) a
split : Vec (2 * i) a #-> Vec i a :* Vec i a


-- 1.2. Compact stack

-- A stack of length i.
data Stack_ : Nat -> Type -> Type where
  Empty : Stack_ i a
  One   :                         Vec i a #-> Stack_ (2 * i) a #-> Stack_ i a
  Two   :             Vec i a #-> Vec i a #-> Stack_ (2 * i) a #-> Stack_ i a
  Three : Vec i a #-> Vec i a #-> Vec i a #-> Stack_ (2 * i) a #-> Stack_ i a

Stack : Type -> Type
Stack = Stack_ 1


-- 1.3. Push

push_ : Vec i a #-> Stack_ i a #-> Stack_ i a
push_ w Empty = One w Empty
push_ w (One       z s) = Two w z s
push_ w (Two     y z s) = Three w y z s
push_ w (Three x y z s) = Two w x (push_ (append y z) s)

push : a #-> Stack a #-> Stack a
push e = push_ (singleton e)


-- 1.4. Pop

data StackView_ : Nat -> Type -> Type where
  Empty' : StackView_ i a
  Cons' : Vec i a #-> Stack_ i a #-> StackView_ i a

popFlatten_ : StackView_ (2 * i) a #-> Stack_ i a
popFlatten_ Empty' = Empty
popFlatten_ (Cons' w s') =
  let x :> y = split w in
  Two x y s'

pop_ : Stack_ i a #-> StackView_ i a
pop_ Empty = Empty'
pop_ (One z s) = Cons' z (popFlatten_ (pop_ s))
pop_ (Two     y z s) = Cons' y (One z s)
pop_ (Three x y z s) = Cons' x (Two y z s)

pop : Stack a #-> Maybe' (a :* Stack a)
pop s = case pop_ s of
  Empty' => Nothing'
  Cons' w s' => Just' (extract w :> s')


-- 1.5. Depth and length

depth_ : Stack_ i a -> Nat
depth_ Empty = 0
depth_ (One       _ s) = 1 + depth_ s
depth_ (Two     _ _ s) = 1 + depth_ s
depth_ (Three _ _ _ s) = 1 + depth_ s

depth : Stack a -> Nat
depth = depth_

length_ : {i : Nat} -> Stack_ i a -> Nat
length_ Empty           = 0
length_ (One       _ s) =     i + length_ s
length_ (Two     _ _ s) = 2 * i + length_ s
length_ (Three _ _ _ s) = 3 * i + length_ s

length : Stack a -> Nat
length = length_


-- 2. Formalization of amortized algorithmic complexity


-- Debits are represented as values of an abstract type d.
-- (x : d) represents one "unit of time".
-- Ultimately, we don't care about constant factors, but
-- that only affects how much is generated vs how much is
-- taken out by each operation.
-- Inbetween, during the lifetime of debits, every debit must be accounted for
-- exactly: it cannot be duplicated or discarded.

-- 2.1. Debit list

-- (UpTo d n) is a type of container with at most d debits.
data UpTo : Type -> Nat -> Type where
  UT_Z : UpTo d n
  UT_S : d #-> UpTo d n #-> UpTo d (1 + n)

implementation Consumable (UpTo d 0) where
  consume UT_Z = ()

splitUpTo : (1 i : Nat) -> {0 j : Nat} -> UpTo d (i + j) #-> UpTo d i :* UpTo d j
splitUpToR : {1 i : Nat} -> (0 j : Nat) -> UpTo d (i + j) #-> UpTo d j :* UpTo d i

addUpTo : UpTo d i #-> UpTo d j #-> UpTo d (i + j)

-- This functions uses some trickery to make the LTE proof irrelevant (multiplicity 0).
raiseUpTo : (0 b_ : b `LTE` b') -> UpTo d b #-> UpTo d b'
raiseUpTo _ UT_Z = UT_Z
raiseUpTo b_ (UT_S q p) =
  rewrite (sym (invertPred b_)) in UT_S q (raiseUpTo (lteAdjPred b_) p)

succUpTo : UpTo d acc #-> UpTo d (S acc)
succUpTo UT_Z = UT_Z
succUpTo (UT_S q p) = UT_S q (succUpTo p)


-- 2.2. Debit structure for compact stacks

-- (DStack d acc s) is a "debit structure" associated with stacks s.
--
-- Only nodes Two store debits, and each Two node stores at most as many debits
-- (up to a constant factor, here 1/2) as there are elements in all Two nodes
-- above it (where the top of the stack is where elements are pushed and
-- popped, and the bottom is where the oldest elements live).
data DStack_ : (d : Type) -> Nat -> Stack_ i a -> Type where
  DEmpty : DStack_ d acc Empty
  DOne   :                DStack_ d  acc      s #-> DStack_     d acc (One       z s)
  DTwo   : UpTo d acc #-> DStack_ d (acc + i) s #-> DStack_ {i} d acc (Two     y z s)
  DThree :                DStack_ d  acc      s #-> DStack_     d acc (Three x y z s)

-- The base case is (acc=1) so that all consecutive Two nodes from the
-- beginning have a debt allowance acc that's a power of two.
--
-- DTwo 1 (DTwo 2 (DTwo 4 (DTwo 8 (...))))
DStack : Type -> Stack a -> Type
DStack d = DStack_ d 1


-- 2.3. Auxiliary operations on debit structures

draise_ : acc `LTE` acc' ?-> DStack_ d acc s #-> DStack_ d acc' s
draise_ acc_ DEmpty = DEmpty
draise_ acc_ (DOne ds) = DOne (draise_ acc_ ds)
draise_ acc_ (DTwo p ds) =
  let 0 acc_' = (plusLteMonotone acc_ lteRefl) in
  DTwo (raiseUpTo acc_ p) (draise_ acc_' ds)
draise_ acc_ (DThree ds) = DThree (draise_ acc_ ds)

ddecr : DStack_ d (S acc) s #-> DStack_ d acc s :* UpTo d (depth_ s)
ddecr DEmpty = DEmpty :> UT_Z
ddecr (DOne ds) =
  let ds' :> q = ddecr ds in
  DOne ds' :> succUpTo q
ddecr (DTwo {i=i'} p ds) =
  let ds' :> q = ddecr ds in
  let q1 :> p' = splitUpTo 1 p in
  DTwo p' ds' :> addUpTo q1 q
ddecr (DThree ds) =
  let ds' :> q = ddecr ds in
  DThree ds' :> succUpTo q


-- 2.4 Push

debit_append : d -> {i : Nat} -> UpTo d i
debit_append supply {i} = case i of
  Z => UT_Z
  S i => UT_S supply (debit_append supply)

-- Transform a debit structure for s to a debit structure for (push_ w s),
-- taking out up to (1 + depth_ s) debits.
-- Debits may be created using the infinitely duplicable (supply : d).
dpush_ : {i : Nat} -> {0 a : Type} -> {0 w : Vec i a} -> {0 s : Stack_ i a} ->
  (0 one : 1 `LTE` i) ->
  d -> DStack_ {i} {a} d 1 s #-> DStack_ {i} {a} d i (push_ w s) :* UpTo d (1 + depth_ s)
dpush_ one _ DEmpty = DOne DEmpty :> UT_Z
dpush_ one _ (DOne ds) = DTwo UT_Z (draise_ (t2' one) ds) :> UT_Z
dpush_ _ one (DTwo p ds) =
  let ds' :> qdepth = ddecr ds in
  DThree ds' :> addUpTo p (succUpTo qdepth)
dpush_ one supply (DThree ds) =
  let ds' :> qdepth = dpush_ (t2 one) supply ds in
  let m = rewrite plusZeroRightNeutral i in Refl in
  let ds'' = rw m ds' in
  DTwo {i} (debit_append supply) ds'' :> succUpTo qdepth

-- The base case is i=1
dpush : d -> DStack d s #-> DStack d (push x s) :* UpTo d (1 + depth s)
dpush = dpush_ lteRefl


-- 2.5 Pop

data DStackView_ : Type -> StackView_ i a -> Type where
  DEmpty' : DStackView_ d Empty'
  DCons' : DStack_ d i s #-> DStackView_ {i} d (Cons' w s)

data DSplit : Type -> Vec i a :* Vec i a -> Type where
  DSplitCost : UpTo d i -> DSplit d (x :> y)

debit_split : d -> {i : Nat} -> (0 w : Vec (2 * i) a) -> DSplit {i} d (split w)

{-
dpopFlatten_ : {i : Nat} -> {0 a : Type} -> {0 s' : StackView_ (2 * i) a} ->
  d -> DStackView_ d s' #-> DStack_ {i} d i (popFlatten_ s') :* UpTo d i
dpopFlatten_ _ DEmpty' = DEmpty :> UT_Z
dpopFlatten_ {s'=Cons' w _} supply (DCons' ds) =
  case debit_split supply w of
    DSplit q => ?aa :> debit_append supply
-}

dpop_ : {i : Nat} -> {0 a : Type} -> {s : Stack_ i a} ->
  (0 one : 1 `LTE` i) ->
  DStack_ d 1 s -> DStackView_ d (pop_ s) :* UpTo d (1 + depth_ s)
dpop_ _ DEmpty = DEmpty' :> UT_Z
dpop_ one (DOne {s=s'} ds) with (pop_ s')
 dpop_ one (DOne {s=s'} ds) | Empty' with (dpop_ (t2 one) ds)
 dpop_ one (DOne {s=s'} ds) | Empty' | DEmpty' :> q = ?www  -- TODO: make this typecheck
 -- TODO: Cons' case
dpop_ one (DTwo p ds) =
  let ds' :> qdepth = ddecr ds in
  DCons' (DOne ds') :> addUpTo p (succUpTo qdepth)
dpop_ one (DThree ds) = DCons' (DTwo UT_Z (draise_ (t2' one) ds)) :> UT_Z