{#hofs} ========= Higher-Order Specifications --------------------------- Types scale to *Higher-Order* Specifications
+ map + fold + visitors + callbacks + ...

Very difficult with *first-order program logics*
Higher Order Specifications =========================== Example: Higher Order Loop -------------------------- 
48: loop :: Int -> Int -> α -> (Int -> α -> α) -> α
49: forall a.
lo:{VV : (Int) | (VV == 0) && (VV >= 0)}
-> hi:{VV : (Int) | (VV >= 0) && (VV >= lo)}
-> a
-> ({VV : (Int) | (VV >= 0) && (VV >= lo) && (VV < hi)} -> a -> a)
-> aloop {VV : (Int) | (VV == 0) && (VV >= 0)}lo {VV : (Int) | (VV >= 0) && (VV >= lo)}hi abase {VV : (Int) | (VV >= 0) && (VV >= lo) && (VV < hi)} -> a -> af = {x4 : (Int) | (x4 >= 0) && (x4 >= lo) && (x4 <= hi)} -> a -> ago {x4 : (Int) | (x4 == 0) && (x4 == lo) && (x4 >= 0)}lo {VV : a | (VV == base)}base
50:   where 
51:     {VV : (Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)} -> a -> ago {VV : (Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)}i aacc 
52:       | {x5 : (Int) | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}i x1:{x12 : (Int) | (x12 >= 0) && (x12 >= i) && (x12 >= lo) && (x12 <= hi)}
-> x2:{x12 : (Int) | (x12 >= 0) && (x12 >= i) && (x12 >= lo) && (x12 <= hi)}
-> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}< {x4 : (Int) | (x4 == hi) && (x4 >= 0) && (x4 >= lo)}hi    = {VV : (Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)} -> a -> ago ({x5 : (Int) | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}ix1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+{x2 : (Int) | (x2 == (1  :  int))}1) ({x4 : (Int) | (x4 >= 0) && (x4 >= lo) && (x4 < hi)} -> a -> af {x5 : (Int) | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}i {VV : a | (VV == acc)}acc)
53:       | otherwise = {VV : a | (VV == acc)}acc

LiquidHaskell infers `f` called with values `(Btwn lo hi)` Example: Summing Lists ---------------------- 
65: forall a. (Num a) => [a] -> alistSum [a]xs  = x1:{x12 : (Int) | (x12 == 0) && (x12 >= 0)}
-> x2:{x9 : (Int) | (x9 >= 0) && (x9 >= x1)}
-> a
-> ({x6 : (Int) | (x6 >= 0) && (x6 >= x1) && (x6 < x2)} -> a -> a)
-> aloop {x2 : (Int) | (x2 == (0  :  int))}0 {x3 : (Int) | (x3 == n) && (x3 == (len xs))}n a0 {x3 : (Int) | (x3 >= 0) && (x3 < n)} -> a -> abody 
66:   where 
67:     {VV : (Int) | (VV >= 0) && (VV < n)} -> a -> abody    = \{VV : (Int) | (VV >= 0) && (VV < n)}i aacc -> {VV : a | (VV == acc)}acc x1:a -> x2:a -> {VV : a | (VV == (x1 + x2))}+ ({x4 : [a] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs x1:[a] -> {x3 : (Int) | (x3 < (len x1)) && (0 <= x3)} -> a!! {x4 : (Int) | (x4 == i) && (x4 >= 0) && (x4 < n)}i)
68:     {x2 : (Int) | (x2 == (len xs))}n       = x1:[a] -> {x2 : (Int) | (x2 == (len x1))}length {x4 : [a] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs

-
*Function subtyping:* `body` called on `i :: Btwn 0 (llen xs)`
-
Hence, indexing with `!!` is safe.
Demo: Tweak `loop` exit condition?
Example: Summing `Nat`s ----------------------- 
87: {-@ listNatSum :: [Nat] -> Nat @-}
88: [{VV : (Int) | (VV >= 0)}] -> {VV : (Int) | (VV >= 0)}listNatSum [{VV : (Int) | (VV >= 0)}]xs  = x1:{x20 : (Int) | (x20 == 0) && (x20 >= 0)}
-> x2:{x17 : (Int) | (x17 >= 0) && (x17 >= x1)}
-> {x14 : (Int) | (x14 >= 0)}
-> ({x12 : (Int) | (x12 >= 0) && (x12 >= x1) && (x12 < x2)}
    -> {x14 : (Int) | (x14 >= 0)} -> {x14 : (Int) | (x14 >= 0)})
-> {x14 : (Int) | (x14 >= 0)}loop {x2 : (Int) | (x2 == (0  :  int))}0 {x3 : (Int) | (x3 == n) && (x3 == (len xs))}n {x2 : (Int) | (x2 == (0  :  int))}0 {x8 : (Int) | (x8 >= 0) && (x8 < n)}
-> x2:{x5 : (Int) | (x5 >= 0)}
-> {x3 : (Int) | (x3 >= 0) && (x3 >= x2)}body 
89:   where 
90:     {VV : (Int) | (VV >= 0) && (VV < n)}
-> acc:{VV : (Int) | (VV >= 0)}
-> {VV : (Int) | (VV >= 0) && (VV >= acc)}body       = \{VV : (Int) | (VV >= 0) && (VV < n)}i {VV : (Int) | (VV >= 0)}acc -> {x3 : (Int) | (x3 == acc) && (x3 >= 0)}acc x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+ ({x4 : [{x7 : (Int) | (x7 >= 0)}] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs x1:[{x9 : (Int) | (x9 >= 0)}]
-> {x5 : (Int) | (x5 < (len x1)) && (0 <= x5)}
-> {x9 : (Int) | (x9 >= 0)}!! {x4 : (Int) | (x4 == i) && (x4 >= 0) && (x4 < n)}i)
91:     {x2 : (Int) | (x2 == (len xs))}n          = x1:[{x6 : (Int) | (x6 >= 0)}] -> {x2 : (Int) | (x2 == (len x1))}length {x4 : [{x7 : (Int) | (x7 >= 0)}] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs

---- ---- --------------------------------------- (+) `::` `x:Int -> y:Int -> {v:Int| v=x+y}` `<:` `Nat -> Nat -> Nat` ---- ---- ---------------------------------------
Example: Summing `Nat`s ----------------------- 
109: {-@ listNatSum :: [Nat] -> Nat @-}
110: listNatSum xs  = loop 0 n 0 body 
111:   where 
112:     body       = \i acc -> acc + (xs !! i)
113:     n          = length xs

Hence, verified by *instantiating* `α` of `loop` with `Nat`
`Int -> Int -> Nat -> (Int -> Nat -> Nat) -> Nat`
Example: Summing `Nat`s ----------------------- 
126: {-@ listNatSum :: [Nat] -> Nat @-}
127: listNatSum xs  = loop 0 n 0 body 
128:   where 
129:     body       = \i acc -> acc + (xs !! i)
130:     n          = length xs

+ Parameter `α` corresponds to *loop invariant* + Instantiation corresponds to invariant *synthesis* Instantiation And Inference --------------------------- +
Polymorphic instantiation happens *everywhere*
+
Automatic inference is crucial
+
*Cannot use* unification (unlike indexed approaches)
+
*Can reuse* [SMT/predicate abstraction.](http://goto.ucsd.edu/~rjhala/papers/liquid_types.html)
Iteration Dependence -------------------- **Cannot** use parametric polymorphism to verify: 
161: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
162: n:{VV : (Int) | (VV >= 0)}
-> m:{VV : (Int) | (VV >= 0)}
-> {VV : (Int) | (VV == (m + n)) && (VV >= 0)}add {VV : (Int) | (VV >= 0)}n {VV : (Int) | (VV >= 0)}m = x1:{x24 : (Int) | (x24 == 0) && (x24 >= 0)}
-> x2:{x21 : (Int) | (x21 >= 0) && (x21 >= x1)}
-> {x18 : (Int) | (x18 >= 0) && (x18 >= n)}
-> ({x15 : (Int) | (x15 >= 0) && (x15 >= x1) && (x15 < x2)}
    -> {x18 : (Int) | (x18 >= 0) && (x18 >= n)}
    -> {x18 : (Int) | (x18 >= 0) && (x18 >= n)})
-> {x18 : (Int) | (x18 >= 0) && (x18 >= n)}loop {x2 : (Int) | (x2 == (0  :  int))}0 {x3 : (Int) | (x3 == m) && (x3 >= 0)}m {x3 : (Int) | (x3 == n) && (x3 >= 0)}n ({x11 : (Int) | (x11 >= 0) && (x11 < m)}
-> x2:{x8 : (Int) | (x8 >= 0) && (x8 >= n)}
-> {x5 : (Int) | (x5 > 0) && (x5 > x2) && (x5 > n) && (x5 >= 0)}\_ {VV : (Int) | (VV >= 0) && (VV >= n)}i -> {x4 : (Int) | (x4 == i) && (x4 >= 0) && (x4 >= n)}i x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+ {x2 : (Int) | (x2 == (1  :  int))}1)

-
As property only holds after **last** loop iteration...
-
... cannot instantiate `α` with `{v:Int | v = n + m}`
**Problem:** Need *iteration-dependent* invariants...