content:   {#hofs}
  =========
  
  <div class="hidden">
  \begin{code}
  module Loop (
      listSum
    , sumNats
    ) where
  
  import Prelude
  
  {-@ LIQUID "--no-termination"@-}
  sumNats  :: [Int] -> Int
  add         :: Int -> Int -> Int
  \end{code}
  </div>
  
  Higher-Order Functions 
  ----------------------
  
  Types scale to *Higher-Order Functions*  
  
  <br>
  
  <div class="fragment">
  
  + map
  + fold
  + visitors
  + callbacks
  + ...
  
  </div>
  
  <br>
  
  <div class="fragment">Difficult with *first-order program logics*</div>
  
  
  Higher Order Specifications 
  ===========================
  
  Example: Higher Order Loop
  --------------------------
  
  <br>
  
  \begin{code}
  loop :: Int -> Int -> α -> (Int -> α -> α) -> α
  loop lo hi base f = go lo base
    where 
      go i acc 
        | i < hi    = go (i+1) (f i acc)
        | otherwise = acc
  \end{code}
  
  <br>
  
  By subtyping, we infer `f` called with values `(Btwn lo hi)`
  
  
  Example: Summing Lists
  ----------------------
  
  \begin{code}
  listSum xs     = loop 0 n 0 body 
    where 
      body i acc = acc + (xs !! i)
      n          = length xs
  \end{code}
  
  <br>
  
  <div class="fragment">
  **Function Subtyping** 
  
  \begin{spec}
  loop :: l -> h -> α -> (Btwn l h -> α -> α) -> α
  \end{spec}
  </div>
  
  <br>
  
  <div class="fragment">
  At callsite, since `l := 0` and `h := llen xs` 
  
  \begin{spec}
  body :: Btwn 0 (llen xs) -> Int -> Int
  \end{spec}
  </div>
  
  Example: Summing Lists
  ----------------------
  
  \begin{spec}
  listSum xs     = loop 0 n 0 body 
    where 
      body i acc = acc + (xs !! i)
      n          = length xs
  \end{spec}
  
  <br>
  
  **Function Subtyping** 
  
  \begin{spec}
  body :: Btwn 0 (llen xs) -> Int -> Int
  \end{spec}
  
  <br>
  
  So `i` is `Btwn 0 (llen xs)`; indexing `!!` is verified safe.
  
  
   {#polyinst}
  ============
  
  Polymorphic Instantiation
  -------------------------
  
  <br>
  <br>
  <br>
  
  <div class="fragment">
  "Plugging in" summaries at call-sites
  </div>
  
  Polymorphic Instantiation
  =========================
  
   {#poly}
  --------
  
  Example: Summing `Nat`s
  -----------------------
  
  \begin{code}
  {-@ sumNats :: [Nat] -> Nat @-}
  sumNats xs  = foldl (+) 0 xs 
  \end{code}
  
  <br>
  
  <div class="fragment">
  \begin{spec} Recall 
  foldl :: (α -> β -> α) -> α -> [β] -> α
  \end{spec}
  </div>
  
  <br>
  
  <div class="fragment">
  How to **instantiate** `α` and `β` ?
  </div>
  
  Function Subtyping
  ------------------
  
  \begin{spec}<div/>
  (+) ::  x:Int -> y:Int -> {v:Int|v=x+y} 
      <:  Nat   -> Nat   -> Nat
  \end{spec}
  
  <br>
  
  <div class="fragment">
  Because,
  
  \begin{spec}<div/>
               |- Nat       <: Int  -- Contra (in)
  x:Nat, y:Nat |- {v = x+y} <: Nat  -- Co    (out)
  \end{spec}
  </div>
  
  <br>
  
  <div class="fragment">
  Because,
  
  \begin{spec}<div/>
    0<=x && 0<=y && v = x+y   => 0 <= v
  \end{spec}
  </div>
  
  
  
  
  Example: Summing `Nat`s
  -----------------------
  
  \begin{spec} <div/> 
  {-@ sumNats :: [Nat] -> Nat @-}
  sumNats xs  = foldl (+) 0 xs 
  \end{spec}
  
  <br>
  
  \begin{spec} Where:
  foldl :: (α -> β -> α) -> α -> [β] -> α
  (+)   :: Nat -> Nat -> Nat
  \end{spec}
  
  <br>
  
  <div class="fragment">
  Hence, `sumNats` verified by **instantiating** `α,β := Nat`
  </div>
  
  <br>
  
  <div class="fragment">
  `α` is **loop invariant**, instantiation is invariant **inference**
  </div>
  
  Instantiation And Inference
  ---------------------------
  
  Polymorphism ubiquitous, so inference is critical!
  
  <br>
  
  <div class="fragment">
  **Step 1. Templates** 
  Instantiate with unknown refinements
  
  $$
  \begin{array}{rcl}
  \alpha & \defeq & \reft{v}{\Int}{\kvar{\alpha}}\\
  \beta  & \defeq & \reft{v}{\Int}{\kvar{\beta}}\\
  \end{array}
  $$
  </div>
  
  <br>
  <div class="fragment">
  **Step 2. Horn-Constraints** 
  By type checking the templates
  </div>
  
  <br>
  <div class="fragment">
  **Step 3. Fixpoint** 
  Abstract interpretation to get solution for $\kvar{}$
  </div>
  
  
  Iteration Dependence
  --------------------
  
  **Problem:** Cannot use parametric polymorphism to verify
  
  <br>
  
  \begin{code}
  {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
  add n m = loop 0 m n (\_ i -> i + 1)
  \end{code}
  
  <br>
  
  <div class="fragment">
  As property only holds after **last iteration** ...
  
  <br>
  
  ... cannot instantiate $\alpha \defeq \reft{v}{\Int}{v = n + m}$
  </div>
  
  <br>
  
  <div class="fragment">
  **Problem:** *Iteration-dependent* invariants...? &nbsp; &nbsp; [[Continue]](04_AbstractRefinements.lhs.slides.html)
  </div>
  
  