content: 
   {#measures}
  ============
  
  Measuring Data Types
  --------------------
  
  <div class="hidden">
  
  \begin{code}
  module Measures where
  import Prelude hiding ((!!), length)
  import Language.Haskell.Liquid.Prelude
  
  length      :: L a -> Int
  (!)         :: L a -> Int -> a
  insert      :: Ord a => a -> L a -> L a
  insertSort  :: Ord a => [a] -> L a
  
  infixr `C`
  \end{code}
  
  </div>
  
  
  Measuring Data Types
  ====================
  
  Recap
  -----
  
  1. <div class="fragment">**Refinements:** Types + Predicates</div>
  2. <div class="fragment">**Subtyping:** SMT Implication</div>
  
  
  Example: Length of a List
  -------------------------
  
  Given a type for lists:
  
  <br>
  
  \begin{code}
  data L a = N | C a (L a)
  \end{code}
  
  <div class="fragment">
  <br>
  
  We can define the **length** as:
  
  <br>
  
  \begin{code}
  {-@ measure llen  :: (L a) -> Int
      llen (N)      = 0
      llen (C x xs) = 1 + (llen xs)  @-}
  \end{code}
  
  </div>
  
  Example: Length of a List
  -------------------------
  
  \begin{code} <div/>
  {-@ measure llen  :: (L a) -> Int
      llen (N)      = 0
      llen (C x xs) = 1 + (llen xs)  @-}
  \end{code}
  
  <br>
  
  We **strengthen** data constructor types
  
  <br>
  
  \begin{code} <div/>
  data L a where
    N :: {v: L a | (llen v) = 0}
    C :: a -> t:_ -> {v:_| llen v = 1 + llen t}
  \end{code}
  
  Measures Are Uninterpreted
  --------------------------
  
  \begin{code} <br>
  data L a where
    N :: {v: L a | (llen v) = 0}
    C :: a -> t:_ -> {v:_| llen v = 1 + llen t}
  \end{code}
  
  <br>
  
  `llen` is an **uninterpreted function** in SMT logic
  
  Measures Are Uninterpreted
  --------------------------
  
  <br>
  
  In SMT, [uninterpreted function](http://fm.csl.sri.com/SSFT12/smt-euf-arithmetic.pdf) $f$ obeys **congruence** axiom:
  
  <br>
  
  $$\forall \overline{x}, \overline{y}. \overline{x} = \overline{y} \Rightarrow
  f(\overline{x}) = f(\overline{y})$$
  
  <br>
  
  <div class="fragment">
  Other properties of `llen` asserted when typing **fold** & **unfold**
  </div>
  
  <br>
  
  <div class="fragment">
  Crucial for *efficient*, *decidable* and *predictable* verification.
  </div>
  
  Measures Are Uninterpreted
  --------------------------
  
  Other properties of `llen` asserted when typing **fold** & **unfold**
  
  <br>
  
  <div class="fragment">
  \begin{code}**Fold**<br>
  z = C x y     -- z :: {v | llen v = 1 + llen y}
  \end{code}
  </div>
  
  <br>
  
  <div class="fragment">
  \begin{code}**Unfold**<br>
  case z of
    N     -> e1 -- z :: {v | llen v = 0}
    C x y -> e2 -- z :: {v | llen v = 1 + llen y}
  \end{code}
  </div>
  
  
  Measured Refinements
  --------------------
  
  Now, we can verify:
  
  <br>
  
  \begin{code}
  {-@ length      :: xs:L a -> (EqLen xs) @-}
  length N        = 0
  length (C _ xs) = 1 + length xs
  \end{code}
  
  <div class="fragment">
  
  <br>
  
  Where `EqLen` is a type alias:
  
  \begin{code}
  {-@ type EqLen Xs = {v:Nat | v = (llen Xs)} @-}
  \end{code}
  
  </div>
  
  List Indexing Redux
  -------------------
  
  We can type list lookup:
  
  \begin{code}
  {-@ (!)      :: xs:L a -> (LtLen xs) -> a @-}
  (C x _)  ! 0 = x
  (C _ xs) ! i = xs ! (i - 1)
  _        ! _ = liquidError "never happens!"
  \end{code}
  
  <br>
  
  <div class="fragment">
  Where `LtLen` is a type alias:
  
  \begin{code}
  {-@ type LtLen Xs = {v:Nat | v < (llen Xs)} @-}
  \end{code}
  
  <br>
  
  <a href="https://liquidhaskell.goto.ucsd.edu/index.html#?demo=HaskellMeasure.hs" target= "_blank">Demo:</a>
  &nbsp; What if we *remove* the precondition?
  
  </div>
  
  Multiple Measures
  -----------------
  
  <br>
  
  Support **many** measures on a type ...
  
  <br>
  
  <div class="fragment">
  ... by **conjoining** the constructor refinements.
  </div>
  
  [[Skip...]](#/refined-data-cons)
  
  
  <!--
  
  Multiple Measures
  =================
  
   {#adasd}
  ---------
  
  We allow *many* measures for a type
  
  Ex: List Emptiness
  ------------------
  
  Measure describing whether a `List` is empty
  
  \begin{code}
  {-@ measure isNull :: (L a) -> Prop
      isNull (N)      = true
      isNull (C x xs) = false           @-}
  \end{code}
  
  <br>
  
  <div class="fragment">
  We **strengthen** data constructors
  
  \begin{code} <div/>
  data L a where
    N :: {v : L a | (isNull v)}
    C :: a -> L a -> {v:(L a) | not (isNull v)}
  \end{code}
  
  </div>
  
  Conjoining Refinements
  ----------------------
  
  Data constructor refinements are **conjoined**
  
  \begin{code} <br>
  data L a where
    N :: {v:L a |  (llen v) = 0
                && (isNull v) }
    C :: a
      -> xs:L a
      -> {v:L a |  (llen v) = 1 + (llen xs)
                && not (isNull v)          }
  \end{code}
  
  -->
  
  Multiple Measures: Red-Black Trees
  ==================================
  
   {#rbtree}
  ----------
  
  <img src="../img/RedBlack.png" height=300px>
  
  + <div class="fragment">**Color:** `Red` nodes have `Black` children</div>
  + <div class="fragment">**Height:** Number of `Black` nodes equal on *all paths*</div>
  <br>
  
  [[Skip...]](#/refined-data-cons)
  
  Basic Type
  ----------
  
  \begin{code} <br>
  data Tree a = Leaf
              | Node Color a (Tree a) (Tree a)
  
  data Color  = Red
              | Black
  \end{code}
  
  Color Invariant
  ---------------
  
  `Red` nodes have `Black` children
  
  <div class="fragment">
  \begin{code} <br>
  measure isRB        :: Tree a -> Prop
  isRB (Leaf)         = true
  isRB (Node c x l r) = c=Red => (isB l && isB r)
                        && isRB l && isRB r
  \end{code}
  </div>
  
  <div class="fragment">
  \begin{code} where <br>
  measure isB         :: Tree a -> Prop
  isB (Leaf)          = true
  isB (Node c x l r)  = c == Black
  \end{code}
  </div>
  
  *Almost* Color Invariant
  ------------------------
  
  <br>
  
  Color Invariant **except** at root.
  
  <br>
  
  <div class="fragment">
  \begin{code} <br>
  measure isAlmost        :: Tree a -> Prop
  isAlmost (Leaf)         = true
  isAlmost (Node c x l r) = isRB l && isRB r
  \end{code}
  </div>
  
  
  Height Invariant
  ----------------
  
  Number of `Black` nodes equal on **all paths**
  
  <div class="fragment">
  \begin{code} <br>
  measure isBH        :: RBTree a -> Prop
  isBH (Leaf)         =  true
  isBH (Node c x l r) =  bh l = bh r
                      && isBH l && isBH r
  \end{code}
  </div>
  
  <div class="fragment">
  \begin{code} where <br>
  measure bh        :: RBTree a -> Int
  bh (Leaf)         = 0
  bh (Node c x l r) = bh l
                    + if c = Red then 0 else 1
  \end{code}
  </div>
  
  Refined Type
  ------------
  
  \begin{code} <br>
  -- Red-Black Trees
  type RBT a  = {v:Tree a | isRB v && isBH v}
  
  -- Almost Red-Black Trees
  type ARBT a = {v:Tree a | isAlmost v && isBH v}
  \end{code}
  
  <br>
  
  [Details](https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/RBTree.hs)
  
  <!--
  
  Measures vs. Index Types
  ========================
  
  Decouple Property & Type
  ------------------------
  
  Unlike [indexed types](http://dl.acm.org/citation.cfm?id=270793) ...
  
  <br>
  
  <div class="fragment">
  
  + Measures **decouple** properties from structures
  
  + Support **multiple** properties over structures
  
  + Enable  **reuse** of structures in different contexts
  
  </div>
  
  <br>
  
  <div class="fragment">Invaluable in practice!</div>
  
  -->
  
  Refined Data Constructors
  =========================
  
   {#refined-data-cons}
  ---------------------
  
  Can encode invariants **inside constructors**
  
  <div class="fragment">
  
  <br>
  
  \begin{code}
  {-@ data L a = N
               | C { x  :: a
                   , xs :: L {v:a| x <= v} } @-}
  \end{code}
  </div>
  <br>
  
  <div class="fragment">
  Head `x` is less than **every** element of tail `xs`
  </div>
  
  <br>
  
  <div class="fragment">
  i.e. specifies **increasing** Lists
  </div>
  
  Increasing Lists
  ----------------
  
  \begin{code} <br>
  data L a where
    N :: L a
    C :: x:a -> xs: L {v:a | x <= v} -> L a
  \end{code}
  
  <br>
  
  - <div class="fragment">We **check** property when **folding** `C`</div>
  - <div class="fragment">We **assume** property when **unfolding** `C`</div>
  
  Increasing Lists
  ----------------
  
  <a href="https://liquidhaskell.goto.ucsd.edu/index.html#?demo=HaskellInsertSort.hs" target= "_blank">Demo: Insertion Sort</a> (hover for inferred types)
  
  <br>
  
  \begin{code}
  insertSort = foldr insert N
  
  insert y (x `C` xs)
    | y <= x    = y `C` (x `C` xs)
    | otherwise = x `C` insert y xs
  insert y N    = y `C` N
  \end{code}
  
  <br>
  
  <div class="fragment">**Problem 1:** What if we need [increasing & decreasing lists](http://web.cecs.pdx.edu/~sheard/Code/QSort.html)?</div>
  
  Recap
  -----
  
  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. **Measures:** Strengthened Constructors
      - <div class="fragment">**Decouple** property from structure</div>
      <!-- - <div class="fragment">**Reuse** structure across *different* properties</div> -->
  
  <br>
  
  <div class="fragment"><a href="03_HigherOrderFunctions.lhs.slides.html" target="_blank">[continue]</a></div>
  