Unique Zippers

Posted by Niki Vazou May 24, 2013

Tags: basic, measures, sets, uniqueness

The story so far: Previously we saw how we can use LiquidHaskell to talk about set of values and specifically the set of values in a list.

Often, we want to enforce the invariant that a particular data structure contains no duplicates. For example, we may have a structure that holds a collection of file handles, or other resources, where the presence of duplicates could lead to unpleasant leaks.

In this post, we will see how to use LiquidHaskell to talk about the set of duplicate values in data structures, and hence, let us specify and verify uniqueness, that is, the absence of duplicates.

To begin, lets extend our vocabulary to talk about the set of duplicate values in lists. By constraining this set to be empty, we can specify a list without duplicates, or an unique list. Once we express uniqueness on lists, it is straightforward to describe uniqueness on other data structures that contain lists. As an example, we will illustrate the properties of a unique zipper.

37: module UniqueZipper where
38: 
39: import Prelude  hiding (reverse, (++), filter)
40: import Data.Set hiding (filter)

A Quick Recap

In the previous post we used a measure for the elements of a list, from Data/Set.spec 
48: measure listElts :: [a] -> (Set a)
49: listElts ([])    = {v | (? (Set_emp v))}
50: listElts (x:xs)  = {v | v = (Set_cup (Set_sng x) (listElts xs)) }

With this measure we defined predicate aliases that describe relations between lists:

57: {-@ predicate EqElts  X Y      = 
58:       ((listElts X) = (listElts Y))                        @-}
59: 
60: {-@ predicate DisjointElts X Y = 
61:       (Set_emp (Set_cap (listElts X) (listElts Y)))        @-}
62: 
63: {-@ predicate SubElts X Y      = 
64:       (Set_sub (listElts X) (listElts Y))                  @-}
65: 
66: {-@ predicate UnionElts X Y Z  = 
67:       ((listElts X) = (Set_cup (listElts Y) (listElts Z))) @-}
68: 
69: {-@ predicate ListElt N X      = 
70:       (Set_mem N (listElts X))                             @-}

These predicates were our vocabulary on specifying properties of list functions. Remember, that reverse returns an output list that has the same elements, i.e., EqElts, with the input list. We can extend these predicates and express list uniqueness. So reversing a unique list should again return an output list that has the same elements as the input list, and also it is unique.

Describing Unique Lists

To describe unique lists, we follow two steps:

  1. we describe the set of duplicate values of a list; and
  2. we demand this set to be empty.

Towards the first step, we define a measure dups that returns the duplicate values of its input list. This measure is recursively defined: The duplicates of an empty list is the empty set. We compute the duplicates of a non-empty list, namely x:xs, as follows:

  • If x is an element of xs, then x is a duplicate. Hence, dups is x plus the (recursively computed) duplicates in xs.

  • Otherwise, we can ignore x and recursively compute the duplicates of xs.

The above intuition can be formalized as a measure:

105: {-@
106:   measure dups :: [a] -> (Set a)
107:   dups([])   = {v | (? (Set_emp v))}
108:   dups(x:xs) = {v | v = (if (Set_mem x (listElts xs))
109:                          then (Set_cup (Set_sng x) (dups xs))
110:                          else (dups xs)) }
111:   @-}

With dups in hand, it is direct to describe unique lists:

A list is unique, if the set of duplicates, as computed by dups is empty.

We create a type alias for unique lists and name it UList.

121: {-@ predicate ListUnique X = (Set_emp (dups X)) @-}
122: 
123: {-@ type UList a = {v:[a] | (ListUnique v)}     @-}

Functions on Unique Lists

In the previous post, we proved interesting properties about the list trilogy, i.e., append, reverse, and filter. Now, we will prove that apart from these properties, all these functions preserve list uniqueness.

Append

To begin with, we proved that the output of append indeed includes the elements from both the input lists. Now, we can also prove that if both input lists are unique and their elements are disjoint, then the output list is also unique.

145: infixr 5 ++
146: {-@ (++) :: xs:(UList a)
147:          -> ys:{v: UList a | (DisjointElts v xs)}
148:          -> {v: UList a | (UnionElts v xs ys)}
149:   @-}
150: (++)         :: [a] -> [a] -> [a]
151: [] forall a.
xs:{VV : [a] | ((Set_emp (dups VV)))}
-> ys:{VV : [a] | ((Set_emp (Set_cap (listElts VV) (listElts xs)))) && ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((listElts VV) == (Set_cup (listElts xs) (listElts ys)))}++ {VV : [a] | ((Set_emp (dups VV)))}ys     = {VV : [a] | ((Set_emp (dups VV))) && (VV == ys) && ((len VV) >= 0)}ys
152: (x:xs) ++ ys = {VV : a | (VV == x)}xforall <p :: a-> a-> Bool>.
y:a
-> ys:[{VV : a<p y> | true}]<p>
-> {VV : [a]<p> | ((dups VV) == (if ((Set_mem y (listElts ys))) then (Set_cup (Set_sng y) (dups ys)) else (dups ys))) && ((len VV) == (1 + (len ys))) && ((listElts VV) == (Set_cup (Set_sng y) (listElts ys)))}:({VV : [a] | (VV == xs) && ((len VV) >= 0)}xs xs:{VV : [a] | ((Set_emp (dups VV)))}
-> ys:{VV : [a] | ((Set_emp (Set_cap (listElts VV) (listElts xs)))) && ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((listElts VV) == (Set_cup (listElts xs) (listElts ys)))}++ {VV : [a] | ((Set_emp (dups VV))) && (VV == ys) && ((len VV) >= 0)}ys)

Reverse

Next, we can prove that if a unique list is reversed, the output list has the same elements as the input, and also it is unique.

163: {-@ reverse :: xs:(UList a) -> {v: UList a | (EqElts v xs)} @-}
164: reverse :: [a] -> [a]
165: forall a.
xs:{VV : [a] | ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((listElts VV) == (listElts xs))}reverse = x1:{VV : [{VV : a | false}]<\_ VV -> false> | ((Set_emp (dups VV))) && ((len VV) == 0)}
-> x2:{VV : [a] | ((Set_emp (Set_cap (listElts VV) (listElts x1)))) && ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((listElts VV) == (Set_cup (listElts x1) (listElts x2))) && ((listElts VV) == (Set_cup (listElts x2) (listElts x1))) && ((len VV) >= 0)}go {VV : [{VV : a | false}]<\_ VV -> false> | ((Set_emp (dups VV))) && ((Set_emp (listElts VV))) && ((len VV) == 0) && ((len VV) >= 0)}[]
166:   where
167:     a:{VV : [a] | ((Set_emp (dups VV))) && ((len VV) >= 0)}
-> x1:{VV : [a] | ((Set_emp (Set_cap (listElts VV) (listElts a)))) && ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((listElts VV) == (Set_cup (listElts a) (listElts x1))) && ((listElts VV) == (Set_cup (listElts x1) (listElts a))) && ((len VV) >= 0)}go {VV : [a] | ((Set_emp (dups VV))) && ((len VV) >= 0)}a []     = {VV : [a] | ((Set_emp (dups VV))) && (VV == a) && ((len VV) >= 0)}a
168:     go a (x:xs) = a:{VV : [a] | ((Set_emp (dups VV))) && ((len VV) >= 0)}
-> x1:{VV : [a] | ((Set_emp (Set_cap (listElts VV) (listElts a)))) && ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((listElts VV) == (Set_cup (listElts a) (listElts x1))) && ((listElts VV) == (Set_cup (listElts x1) (listElts a))) && ((len VV) >= 0)}go ({VV : a | (VV == x)}xforall <p :: a-> a-> Bool>.
y:a
-> ys:[{VV : a<p y> | true}]<p>
-> {VV : [a]<p> | ((dups VV) == (if ((Set_mem y (listElts ys))) then (Set_cup (Set_sng y) (dups ys)) else (dups ys))) && ((len VV) == (1 + (len ys))) && ((listElts VV) == (Set_cup (Set_sng y) (listElts ys)))}:{VV : [a] | ((Set_emp (dups VV))) && (VV == a) && ((len VV) >= 0)}a) {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs

Filter

Finally, filtering a unique list returns a list with a subset of values of the input list, that once again is unique!

178: {-@ filter :: (a -> Bool) 
179:            -> xs:(UList a) 
180:            -> {v:UList a | (SubElts v xs)} 
181:   @-}
182: forall a.
(a -> (GHC.Types.Bool))
-> x2:{VV : [a] | ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((Set_sub (listElts VV) (listElts x2))) && ((len VV) >= 0)}filter a -> (GHC.Types.Bool)p [] = forall <p :: a-> a-> Bool>.
{VV : [{VV : a | false}]<p> | ((Set_emp (dups VV))) && ((Set_emp (listElts VV))) && ((len VV) == 0)}[]
183: filter p (x:xs) 
184:   | a -> (GHC.Types.Bool)p {VV : a | (VV == x)}x       = {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
y:a
-> ys:[{VV : a<p y> | true}]<p>
-> {VV : [a]<p> | ((dups VV) == (if ((Set_mem y (listElts ys))) then (Set_cup (Set_sng y) (dups ys)) else (dups ys))) && ((len VV) == (1 + (len ys))) && ((listElts VV) == (Set_cup (Set_sng y) (listElts ys)))}: forall a.
(a -> (GHC.Types.Bool))
-> x2:{VV : [a] | ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((Set_sub (listElts VV) (listElts x2))) && ((len VV) >= 0)}filter a -> (GHC.Types.Bool)p {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs
185:   | otherwise = forall a.
(a -> (GHC.Types.Bool))
-> x2:{VV : [a] | ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((Set_sub (listElts VV) (listElts x2))) && ((len VV) >= 0)}filter a -> (GHC.Types.Bool)p {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs

Unique Zipper

That was easy enough! Now, lets look at a slightly more interesting structure fashioned from lists. A zipper is an aggregate data stucture that is used to arbitrary traverse the structure and update its contents.

We define a zipper as a data type that contains an element (called focus) that we are currently using, a list of elements (called up) before the current one, and a list of elements (called down) after the current one.

202: data Zipper a = Zipper { forall a. (UniqueZipper.Zipper a) -> afocus :: a       -- focused element in this set
203:                        , forall a. (UniqueZipper.Zipper a) -> [a]up    :: [a]     -- elements to the left
204:                        , forall a. (UniqueZipper.Zipper a) -> [a]down  :: [a] }   -- elements to the right

One well-known application of zippers is in the XMonad tiling window manager. The set of windows being managed is stored in a zipper similar to the above. The focus happily coincides with the window currently in focus, and the up and down to the list of windows that come before and after it.

One crucial invariant maintained by XMonad is that the zipper structure is unique – i.e. each window appears at most once inside the zipper.

Lets see how we can state and check that all the values in a zipper are unique.

To start with, we would like to refine the Zipper data declaration to express that both the lists in the structure are unique and do not include focus in their values.

LiquidHaskell allow us to refine data type declarations, using the liquid comments. So, apart from above definition definition for the Zipper, we add a refined one, stating that the data structure always enjoys the desired properties.

229: {-@ data Zipper a = Zipper { focus :: a
230:                            , up    :: UListDif a focus
231:                            , down  :: UListDif a focus}
232:   @-}
233: 
234: {-@ type UListDif a N = {v:(UList a) | (not (ListElt N v))} @-}

It is worth noting that the above is kind of dependent record in that the types of the up and down fields depend on the value of the focus field.

With this annotation any time we use a Zipper in the code LiquidHaskell knows that the up and down components are unique lists that do not include focus. Moreover, when a new Zipper is constructed LiquidHaskell proves that this property holds, otherwise a liquid type error is reported.

Hold on a minute!

The awake reader will have noticed that values inside the Zipper as specified so far, are not unique, as nothing prevents a value from appearing in both the up and the down components.

So, we have to specify that the contents of those two fields are disjoint.

One way to achieve this is by defining two measures getUp and getDown that return the relevant parts of the Zipper

260: {-@ measure getUp :: forall a. (Zipper a) -> [a] 
261:     getUp (Zipper focus up down) = up
262:   @-}
263: 
264: {-@ measure getDown :: forall a. (Zipper a) -> [a] 
265:     getDown (Zipper focus up down) = down
266:   @-}

With these definitions, we create a type alias UZipper that states that the two list components are disjoint, and hence, that we have a unique zipper with no duplicates.

274: {-@ 
275:   type UZipper a = {v:Zipper a | (DisjointElts (getUp v) (getDown v))} 
276:   @-}

Functions on Unique Zippers

Now that we have defined a unique zipper, it is straightforward for LiquidHaskell to prove that operations on zippers preserve uniqueness.

Differentiation

We can prove that a zipper that built from elements from a unique list is indeed unique.

293: {-@ differentiate :: UList a -> Maybe (UZipper a) @-}
294: forall a.
{VV : [a] | ((Set_emp (dups VV)))}
-> (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))})differentiate []     = forall a. {VV : (Data.Maybe.Maybe a) | (((isJust VV)) <=> false)}Nothing
295: differentiate (x:xs) = x:{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> {VV : (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}) | (((isJust VV)) <=> true) && ((fromJust VV) == x)}Just ({VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
 -> (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}))
-> {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))})$ focus:a
-> up:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> down:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> {VV : (UniqueZipper.Zipper a) | ((getDown VV) == down) && ((getUp VV) == up)}Zipper {VV : a | (VV == x)}x {VV : [{VV : a | false}]<\_ VV -> false> | ((Set_emp (dups VV))) && ((Set_emp (listElts VV))) && ((len VV) == 0) && ((len VV) >= 0)}[] {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs

Integration

And vice versa, all elements of a unique zipper yield a unique list.

304: {-@ integrate :: UZipper a -> UList a @-}
305: forall a.
{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> {VV : [a] | ((Set_emp (dups VV)))}integrate (Zipper x l r) = xs:{VV : [a] | ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((listElts VV) == (listElts xs))}reverse {VV : [a] | (not (((Set_mem x (listElts VV))))) && ((Set_emp (dups VV))) && (VV == l) && ((len VV) >= 0)}l xs:{VV : [a] | ((Set_emp (dups VV)))}
-> ys:{VV : [a] | ((Set_emp (Set_cap (listElts VV) (listElts xs)))) && ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((listElts VV) == (Set_cup (listElts xs) (listElts ys)))}++ {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
y:a
-> ys:[{VV : a<p y> | true}]<p>
-> {VV : [a]<p> | ((dups VV) == (if ((Set_mem y (listElts ys))) then (Set_cup (Set_sng y) (dups ys)) else (dups ys))) && ((len VV) == (1 + (len ys))) && ((listElts VV) == (Set_cup (Set_sng y) (listElts ys)))}: {VV : [a] | (not (((Set_mem x (listElts VV))))) && ((Set_emp (dups VV))) && (VV == r) && ((len VV) >= 0)}r

Recall the types for ++ and reverse that we proved earlier – hover your mouse over the identifiers to refresh your memory. Those types are essential for establishing the type of integrate.

  • By the definition of UZipper we know that l is a unique list and that x is not an element of l.

  • Thus via the type of reverse we know that reverse l is also unique and disjoint from x and r.

  • Finally, using the previously established type for ++ LiquidHaskell can prove that since x : r is a unique list with elements disjoint from reverse l the concatenation of the two lists is also a unique list.

With the exact same reasoning, we use the above list operations to create more zipper operations.

Reverse

We can reverse a unique zipper

332: {-@ reverseZipper :: UZipper a -> UZipper a @-}
333: reverseZipper :: Zipper a -> Zipper a
334: forall a.
{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}reverseZipper (Zipper t ls rs) = focus:a
-> up:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> down:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> {VV : (UniqueZipper.Zipper a) | ((getDown VV) == down) && ((getUp VV) == up)}Zipper {VV : a | (VV == t)}t {VV : [a] | (not (((Set_mem t (listElts VV))))) && ((Set_emp (dups VV))) && (VV == rs) && ((len VV) >= 0)}rs {VV : [a] | (not (((Set_mem t (listElts VV))))) && ((Set_emp (dups VV))) && (VV == ls) && ((len VV) >= 0)}ls

Shifting Focus

More the focus up or down

343: {-@ focusUp   :: UZipper a -> UZipper a @-}
344: forall a.
{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}focusUp (Zipper t [] rs)     = focus:a
-> up:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> down:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> {VV : (UniqueZipper.Zipper a) | ((getDown VV) == down) && ((getUp VV) == up)}Zipper {VV : a | (VV == x) && (VV == x)}x {VV : [a] | (not (((Set_mem x (listElts VV))))) && (not (((Set_mem x (listElts VV))))) && ((Set_emp (dups VV))) && (VV == xs) && (VV == xs) && ((len VV) == (len xs)) && ((listElts VV) == (Set_cup (listElts xs) (listElts xs))) && ((listElts VV) == (listElts xs)) && ((len VV) >= 0)}xs {VV : [{VV : a | false}]<\_ VV -> false> | ((Set_emp (dups VV))) && ((Set_emp (listElts VV))) && ((len VV) == 0) && ((len VV) >= 0)}[] 
345:   where 
346:     ({VV : a | (VV == x)}x:{VV : [a] | (not (((Set_mem x (listElts VV))))) && (not (((Set_mem x (listElts VV))))) && ((Set_emp (dups VV))) && (VV == xs) && ((len VV) == (len xs)) && ((listElts VV) == (Set_cup (listElts xs) (listElts xs))) && ((listElts VV) == (listElts xs)) && ((len VV) >= 0)}xs)                   = xs:{VV : [a] | ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((listElts VV) == (listElts xs))}reverse ({VV : a | (VV == t)}tforall <p :: a-> a-> Bool>.
y:a
-> ys:[{VV : a<p y> | true}]<p>
-> {VV : [a]<p> | ((dups VV) == (if ((Set_mem y (listElts ys))) then (Set_cup (Set_sng y) (dups ys)) else (dups ys))) && ((len VV) == (1 + (len ys))) && ((listElts VV) == (Set_cup (Set_sng y) (listElts ys)))}:{VV : [a] | (not (((Set_mem t (listElts VV))))) && ((Set_emp (dups VV))) && (VV == rs) && ((len VV) >= 0)}rs)
347: 
348: focusUp (Zipper t (l:ls) rs) = focus:a
-> up:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> down:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> {VV : (UniqueZipper.Zipper a) | ((getDown VV) == down) && ((getUp VV) == up)}Zipper {VV : a | (VV == l)}l {VV : [a] | (VV == ls) && ((len VV) >= 0)}ls ({VV : a | (VV == t)}tforall <p :: a-> a-> Bool>.
y:a
-> ys:[{VV : a<p y> | true}]<p>
-> {VV : [a]<p> | ((dups VV) == (if ((Set_mem y (listElts ys))) then (Set_cup (Set_sng y) (dups ys)) else (dups ys))) && ((len VV) == (1 + (len ys))) && ((listElts VV) == (Set_cup (Set_sng y) (listElts ys)))}:{VV : [a] | (not (((Set_mem t (listElts VV))))) && ((Set_emp (dups VV))) && (VV == rs) && ((len VV) >= 0)}rs)
349: 
350: {-@ focusDown :: UZipper a -> UZipper a @-}
351: forall a.
{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}focusDown = {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}reverseZipper forall <q :: (UniqueZipper.Zipper a)-> (UniqueZipper.Zipper a)-> Bool, p :: (UniqueZipper.Zipper a)-> (UniqueZipper.Zipper a)-> Bool>.
(x:{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
 -> {VV : (UniqueZipper.Zipper a)<p x> | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))})
-> (y:{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
    -> {VV : (UniqueZipper.Zipper a)<q y> | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))})
-> x:{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> exists [z:{VV : (UniqueZipper.Zipper a)<q x> | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}].{VV : (UniqueZipper.Zipper a)<p z> | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}. {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}focusUp forall <q :: (UniqueZipper.Zipper a)-> (UniqueZipper.Zipper a)-> Bool, p :: (UniqueZipper.Zipper a)-> (UniqueZipper.Zipper a)-> Bool>.
(x:{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
 -> {VV : (UniqueZipper.Zipper a)<p x> | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))})
-> (y:{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
    -> {VV : (UniqueZipper.Zipper a)<q y> | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))})
-> x:{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> exists [z:{VV : (UniqueZipper.Zipper a)<q x> | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}].{VV : (UniqueZipper.Zipper a)<p z> | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}. {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}reverseZipper

Filter

Finally, using the filter operation on lists allows LiquidHaskell to prove that filtering a zipper also preserves uniqueness.

361: {-@ filterZipper :: (a -> Bool) -> UZipper a -> Maybe (UZipper a) @-}
362: forall a.
(a -> (GHC.Types.Bool))
-> {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))})filterZipper a -> (GHC.Types.Bool)p (Zipper f ls rs) 
363:   = case (a -> (GHC.Types.Bool))
-> xs:{VV : [a] | ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((Set_sub (listElts VV) (listElts xs)))}filter a -> (GHC.Types.Bool)p ({VV : a | (VV == f)}fforall <p :: a-> a-> Bool>.
y:a
-> ys:[{VV : a<p y> | true}]<p>
-> {VV : [a]<p> | ((dups VV) == (if ((Set_mem y (listElts ys))) then (Set_cup (Set_sng y) (dups ys)) else (dups ys))) && ((len VV) == (1 + (len ys))) && ((listElts VV) == (Set_cup (Set_sng y) (listElts ys)))}:{VV : [a] | (not (((Set_mem f (listElts VV))))) && ((Set_emp (dups VV))) && (VV == rs) && ((len VV) >= 0)}rs) of
364:       f':rs' -> x:{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> {VV : (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}) | (((isJust VV)) <=> true) && ((fromJust VV) == x)}Just ({VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
 -> (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}))
-> {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))})$ focus:a
-> up:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> down:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> {VV : (UniqueZipper.Zipper a) | ((getDown VV) == down) && ((getUp VV) == up)}Zipper {VV : a | (VV == f')}f' ((a -> (GHC.Types.Bool))
-> xs:{VV : [a] | ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((Set_sub (listElts VV) (listElts xs)))}filter a -> (GHC.Types.Bool)p {VV : [a] | (not (((Set_mem f (listElts VV))))) && ((Set_emp (dups VV))) && (VV == ls) && ((len VV) >= 0)}ls) {VV : [a] | (VV == rs') && ((len VV) >= 0)}rs'
365:       []     -> case (a -> (GHC.Types.Bool))
-> xs:{VV : [a] | ((Set_emp (dups VV)))}
-> {VV : [a] | ((Set_emp (dups VV))) && ((Set_sub (listElts VV) (listElts xs)))}filter a -> (GHC.Types.Bool)p {VV : [a] | (not (((Set_mem f (listElts VV))))) && ((Set_emp (dups VV))) && (VV == ls) && ((len VV) >= 0)}ls of                  
366:                   f':ls' -> x:{VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> {VV : (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}) | (((isJust VV)) <=> true) && ((fromJust VV) == x)}Just ({VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
 -> (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}))
-> {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))}
-> (Data.Maybe.Maybe {VV : (UniqueZipper.Zipper a) | ((Set_emp (Set_cap (listElts (getUp VV)) (listElts (getDown VV)))))})$ focus:a
-> up:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> down:{VV : [a] | (not (((Set_mem focus (listElts VV))))) && ((Set_emp (dups VV)))}
-> {VV : (UniqueZipper.Zipper a) | ((getDown VV) == down) && ((getUp VV) == up)}Zipper {VV : a | (VV == f')}f' {VV : [a] | (VV == ls') && ((len VV) >= 0)}ls' {VV : [{VV : a | false}]<\_ VV -> false> | ((Set_emp (dups VV))) && ((Set_emp (listElts VV))) && ((len VV) == 0) && ((len VV) >= 0)}[]
367:                   []     -> forall a. {VV : (Data.Maybe.Maybe a) | (((isJust VV)) <=> false)}Nothing

Conclusion

That’s all for now! This post illustrated

  1. How we can use set theory to express properties the values of the list, such as list uniqueness.

  2. How we can use LuquidHaskell to prove that these properties are preserved through list operations.

  3. How we can embed this properties in complicated data structures that use lists, such as a zipper.

390: -- TODO: Dummy function to provide qualifier hint.
391: {-@ q :: x:a ->  {v:[a] |(not (Set_mem x (listElts v)))} @-}
392: q :: a -> [a]
393: forall a. x:a -> {VV : [a] | (not (((Set_mem x (listElts VV)))))}q _ = forall <p :: a-> a-> Bool>.
{VV : [{VV : a | false}]<p> | ((Set_emp (dups VV))) && ((Set_emp (listElts VV))) && ((len VV) == 0)}[]