**1.**Introduction {#intro}**1.1.**Well-Typed Programs Do Go Wrong {#gowrong}**1.2.**Refinement Types**1.3.**Audience**1.4.**Getting Started**2.**Logic & SMT**2.1.**Syntax**2.2.**Semantics {#semantics}**2.3.**Verification Conditions**2.4.**Examples: Propositions**2.5.**Examples: Arithmetic**2.6.**Examples: Uninterpreted Function**2.7.**Recap**3.**Refinement Types**3.1.**Defining Types {#definetype}**3.2.**Errors**3.3.**Subtyping**3.4.**Writing Specifications**3.5.**Refining Function Types: Pre-conditions**3.6.**Refining Function Types: Post-conditions**3.7.**Testing Values: Booleans and Propositions {#propositions}**3.8.**Putting It All Together**3.9.**Recap**4.**Polymorphism {#polymorphism}**4.1.**Specification: Vector Bounds {#vectorbounds}**4.2.**Verification: Vector Lookup**4.3.**Inference: Our First Recursive Function**4.4.**Higher-Order Functions: Bottling Recursion in a`loop`

**4.5.**Refinements and Polymorphism {#sparsetype}**4.6.**Recap**5.**Refined Datatypes {#refineddatatypes}**5.1.**Sparse Vectors Revisited {#autosmart}**5.2.**Ordered Lists {#orderedlists}**5.3.**Ordered Trees {#binarysearchtree}**5.4.**Recap**6.**Boolean Measures {#boolmeasures}**6.1.**Partial Functions**6.2.**Lifting Functions to Measures {#usingmeasures}**6.3.**A Safe List API**6.4.**Recap**7.**Numeric Measures {#numericmeasure}**7.1.**Wholemeal Programming**7.2.**Specifying List Dimensions**7.3.**Lists: Size Preserving API**7.4.**Lists: Size Reducing API {#listreducing}**7.5.**Dimension Safe Vector API**7.6.**Dimension Safe Matrix API**7.7.**Recap**8.**Elemental Measures {#setmeasure}**8.1.**Talking about Sets**8.2.**Proving QuickCheck Style Properties {#quickcheck}**8.3.**Content-Aware List API {#listelems}**8.4.**Permutations**8.5.**Uniqueness**8.6.**Unique Zippers**8.7.**Recap**9.**Case Study: Okasaki's Lazy Queues {#lazyqueue}**10.**Case Study: Associative Maps**10.1.**Specifying Maps {#mapapi}**10.2.**Using Maps: Well Scoped Expressions**10.3.**Implementing Maps: Binary Search Trees {#lemmas}**10.4.**Recap**11.**Case Study: Pointers & Bytes {#case-study-pointers}**11.1.**HeartBleeds in Haskell**11.2.**Low-level Pointer API**11.3.**A Refined Pointer API**11.4.**Assumptions vs Guarantees**11.5.**ByteString API**11.6.**Application API**11.7.**Nested ByteStrings**11.8.**Recap: Types Against Overflows**12.**Case Study: AVL Trees {#case-study-avltree}

Lets start with a case study that is simple enough to explain without
pages of code, yet complex enough to show off whats cool about
dependency: Chris Okasaki’s beautiful Lazy
Queues. This structure leans heavily on an invariant to provide fast
*insertion* and *deletion*. Let’s see how to enforce that
invariant with LiquidHaskell.

{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--maxparams=3" @-}
module Tutorial_09_Case_Study_Lazy_Queues
(Queue, insert, remove, emp, realSize)
where
import Prelude hiding (replicate, take, length)
-- | Size function actually returns the size: (Duh!)
{-@ size :: q:SList a -> {v:Nat | v = size q} @-}
{-@ die :: {v:String | false} -> a @-}
die x = error x
{-@ invariant {v:SList a | size v >= 0} @-}
-- Source: Okasaki, JFP 1995
-- http://www.westpoint.edu/eecs/SiteAssets/SitePages/Faculty%20Publication%20Documents/Okasaki/jfp95queue.pdf
replicate :: Int -> a -> Queue a
-- {-@ ignore badList @-}
-- {-@ ignore hd @-}
-- {-@ ignore tl @-}
-- {-@ ignore badQ @-}

A queue
is a structure into which we can `insert`

and
`remove`

data such that the order in which the data is
removed is the same as the order in which it was inserted.

**To efficiently implement** a queue we need to have rapid
access to both the front as well as the back because we
`remove`

elements from former and `insert`

elements into the latter. This is quite straightforward with explicit
pointers and mutation – one uses an old school linked list and maintains
pointers to the head and the tail. But can we implement the structure
efficiently without having stoop so low?

**Chris Okasaki** came up with a very cunning way to
implement queues using a *pair* of lists – let’s call them
`front`

and `back`

which represent the
corresponding parts of the Queue.

- To
`insert`

elements, we just*cons*them onto the`back`

list, - To
`remove`

elements, we just*un-cons*them from the`front`

list.

**The catch** is that we need to shunt elements from the
back to the front every so often, e.g. we can transfer the elements from
the `back`

to the `front`

, when:

- a
`remove`

call is triggered, and - the
`front`

list is empty.

**Okasaki's first insight** was to note that every element
is only moved *once* from the back to the front; hence, the time
for `insert`

and `remove`

could be
`O(1)`

when *amortized* over all the operations. This
is perfect, *except* that some set of unlucky `remove`

calls (which occur when the `front`

is empty) are stuck
paying the bill. They have a rather high latency up to `O(n)`

where `n`

is the total number of operations.

**Okasaki's second insight** saves the day: he observed
that all we need to do is to enforce a simple *balance
invariant*:

\[\mbox{Size of front} \geq \mbox{Size of back}\]

If the lists are lazy i.e. only constructed as the head value is
demanded, then a single `remove`

needs only a tiny
`O(log n)`

in the worst case, and so no single
`remove`

is stuck paying the bill.

**Lets implement Queues** and ensure the crucial
invariant(s) with LiquidHaskell. What we need are the following
ingredients:

A type for

`List`

s, and a way to track their`size`

,A type for

`Queue`

s which encodes the balance invariantA way to implement the

`insert`

,`remove`

and`transfer`

operations.

The first part is super easy. Let’s define a type:

data SList a = SL { size :: Int, elems :: [a] }

We have a special field that saves the `size`

because
otherwise, we have a linear time computation that wrecks Okasaki’s
careful analysis. (Actually, he presents a variant which does
*not* require saving the size as well, but that’s for another
day.)

How can we be sure that `size`

is indeed the *real
size* of `elems`

? Let’s write a function to
*measure* the real size:

{-@ measure realSize @-}
realSize :: [a] -> Int
realSize [] = 0
realSize (_:xs) = 1 + realSize xs

Now, we can simply specify a *refined* type for
`SList`

that ensures that the *real* size is saved in
the `size`

field:

{-@ data SList a = SL {
size :: Nat
, elems :: {v:[a] | realSize v = size}
}
@-}

As a sanity check, consider this:

okList = SL 1 ["cat"] -- accepted
badList = SL 1 [] -- rejected

**Lets define an alias** for lists of a given size
`N`

:

{-@ type SListN a N = {v:SList a | size v = N} @-}

Finally, we can define a basic API for `SList`

.

**To Construct lists**, we use `nil`

and
`cons`

:

{-@ nil :: SListN a 0 @-}
nil = SL 0 []
{-@ cons :: a -> xs:SList a -> SListN a {size xs + 1} @-}
cons x (SL n xs) = SL (n+1) (x:xs)

**Exercise: (Destructing Lists): **We can destruct lists by
writing a `hd`

and `tl`

function as shown below.
Fix the specification or implementation such that the definitions
typecheck.

{-@ tl :: xs:SList a -> SListN a {size xs - 1} @-}
tl (SL n (_:xs)) = SL (n-1) xs
tl _ = die "empty SList"
{-@ hd :: xs:SList a -> a @-}
hd (SL _ (x:_)) = x
hd _ = die "empty SList"

**Hint: **When you are done, `okHd`

should be
verified, but `badHd`

should be rejected.

{-@ okList :: SListN String 1 @-}
okHd = hd okList -- accepted
badHd = hd (tl okList) -- rejected

It is quite straightforward to define the `Queue`

type, as
a pair of lists, `front`

and `back`

, such that the
latter is always smaller than the former:

{-@ data Queue a = Q {
front :: SList a
, back :: SListLE a (size front)
}
@-}
data Queue a = Q
{ front :: SList a
, back :: SList a
}

**The alias** `SListLE a L`

corresponds to lists
with at most `N`

elements:

{-@ type SListLE a N = {v:SList a | size v <= N} @-}

As a quick check, notice that we *cannot represent illegal
Queues*:

okQ = Q okList nil -- accepted, |front| > |back|
badQ = Q nil okList -- rejected, |front| < |back|

Almost there! Now all that remains is to define the
`Queue`

API. The code below is more or less identical to
Okasaki’s (I prefer `front`

and `back`

to his
`left`

and `right`

.)

**The Empty Queue** is simply one where both
`front`

and `back`

are both empty:

emp = Q nil nil

**To Remove** an element we pop it off the
`front`

by using `hd`

and `tl`

. Notice
that the `remove`

is only called on non-empty
`Queue`

s, which together with the key balance invariant,
ensures that the calls to `hd`

and `tl`

are
safe.

remove (Q f b) = (hd f, makeq (tl f) b)

**Exercise: (Whither pattern matching?): **Can you explain
why we (or Okasaki) didn’t use pattern matching here, and have instead
opted for the explicit `hd`

and `tl`

?

**Exercise: (Queue Sizes): **If you did the *List
Destructing* exercise above, then you will notice that the code for
`remove`

has a type error: namely, the calls to
`hd`

and `tl`

may fail if the `f`

list
is empty.

- Write a
*measure*to describe the queue size, - Use it to complete the definition of
`QueueN`

below, and - Use it to give
`remove`

a type that verifies the safety of the calls made to`hd`

and`tl`

.

**Hint: **When you are done, `okRemove`

should be accepted, `badRemove`

should be rejected, and
`emp`

should have the type shown below:

-- | Queues of size `N`
{-@ type QueueN a N = {v:Queue a | true} @-}
okRemove = remove example2Q -- accept
badRemove = remove example0Q -- reject
{-@ emp :: QueueN _ 0 @-}
{-@ example2Q :: QueueN _ 2 @-}
example2Q = Q (1 `cons` (2 `cons` nil)) nil
{-@ example0Q :: QueueN _ 0 @-}
example0Q = Q nil nil

**To Insert** an element we just `cons`

it to
the `back`

list, and call the *smart constructor*
`makeq`

to ensure that the balance invariant holds:

insert e (Q f b) = makeq f (e `cons` b)

**Exercise: (Insert): **Write down a type for
`insert`

such that `replicate`

and
`okReplicate`

are accepted by LiquidHaskell, but
`badReplicate`

is rejected.

{-@ replicate :: n:Nat -> a -> QueueN a n @-}
replicate 0 _ = emp
replicate n x = insert x (replicate (n-1) x)
{-@ okReplicate :: QueueN _ 3 @-}
okReplicate = replicate 3 "Yeah!" -- accept
{-@ badReplicate :: QueueN _ 3 @-}
badReplicate = replicate 1 "No!" -- reject

**To Ensure the Invariant** we use the smart constructor
`makeq`

, which is where the heavy lifting happens. The
constructor takes two lists, the front `f`

and back
`b`

and if they are balanced, directly returns the
`Queue`

, and otherwise transfers the elements from
`b`

over using the rotate function `rot`

described
next.

{-@ makeq :: f:SList a -> b:SList a -> QueueN a {size f + size b} @-}
makeq f b
| size b <= size f = Q f b
| otherwise = Q (rot f b nil) nil

**Exercise: (Rotate): ** The Rotate function
`rot`

is only called when the `back`

is one larger
than the `front`

(we never let things drift beyond that). It
is arranged so that it the `hd`

is built up fast, before the
entire computation finishes; which, combined with laziness provides the
efficient worst-case guarantee. Write down a type for `rot`

so that it typechecks and verifies the type for `makeq`

.

**Hint: **You may have to modify a precondition in
`makeq`

to capture the relationship between `f`

and `b`

.

rot f b acc
| size f == 0 = hd b `cons` acc
| otherwise = hd f `cons` rot (tl f) (tl b) (hd b `cons` acc)

**Exercise: (Transfer): **Write down a signature for
`take`

which extracts `n`

elements from its input
`q`

and puts them into a new output Queue. When you are done,
`okTake`

should be accepted, but `badTake`

should
be rejected.

take :: Int -> Queue a -> (Queue a, Queue a)
take 0 q = (emp , q)
take n q = (insert x out , q'')
where
(x , q') = remove q
(out, q'') = take (n-1) q'
{-@ okTake :: (QueueN _ 2, QueueN _ 1) @-}
okTake = take 2 exampleQ -- accept
badTake = take 10 exampleQ -- reject
exampleQ = insert "nal" $ insert "bob" $ insert "alice" $ emp

Well there you have it; Okasaki’s beautiful lazy Queue, with the invariants easily expressed and checked with LiquidHaskell. This example is particularly interesting because

- The refinements express invariants that are critical for efficiency,
- The code introspects on the
`size`

to guarantee the invariants, and - The code is quite simple and we hope, easy to follow!