## 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

```50: loop :: Int -> Int -> α -> (Int -> α -> α) -> α
51: 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
52:   where
53:     {VV : Int | (VV >= 0) && (VV >= lo) && (VV <= hi)} -> a -> ago {VV : Int | (VV >= 0) && (VV >= lo) && (VV <= hi)}i aacc
54:       | {x5 : Int | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}i x1:Int -> x2:Int -> {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)
55:       | otherwise = {VV : a | (VV == acc)}acc
```

LiquidHaskell infers `f` called with values `(Btwn lo hi)`

## Example: Summing Lists

```67: listSum     :: [Int] -> Int
68: [Int] -> IntlistSum [Int]xs  = x1:{x14 : Int | (x14 == 0) && (x14 >= 0)}
-> x2:{x11 : Int | (x11 >= 0) && (x11 >= x1)}
-> Int
-> ({x7 : Int | (x7 >= 0) && (x7 >= x1) && (x7 < x2)}
-> Int -> Int)
-> Intloop {x2 : Int | (x2 == (0  :  int))}0 {x3 : Int | (x3 == n) && (x3 == (len xs))}n {x2 : Int | (x2 == (0  :  int))}0 {x5 : Int | (x5 >= 0) && (x5 < n)} -> Int -> Intbody
69:   where
70:     {VV : Int | (VV >= 0) && (VV < n)} -> Int -> Intbody    = \{VV : Int | (VV >= 0) && (VV < n)}i Intacc -> {x2 : Int | (x2 == acc)}acc x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+ ({x3 : [Int] | (x3 == xs) && ((len x3) >= 0)}xs x1:[Int] -> {x4 : Int | (x4 < (len x1)) && (0 <= x4)} -> Int!! {x4 : Int | (x4 == i) && (x4 >= 0) && (x4 < n)}i)
71:     {x2 : Int | (x2 == (len xs))}n       = x1:[Int] -> {x2 : Int | (x2 == (len x1))}length {x3 : [Int] | (x3 == xs) && ((len x3) >= 0)}xs
```

Function Subtyping

• `body` called with `i :: Btwn 0 (llen xs)`

• Hence, indexing with `!!` is safe.
Demo: Tweak `loop` exit condition?

# Polymorphic Instantiation

## Example: Summing `Nat`s

```98: {-@ sumNats :: [Nat] -> Nat @-}
99: [{v : Int | (v >= 0)}] -> {v : Int | (v >= 0)}sumNats [{v : Int | (v >= 0)}]xs  = ({x14 : Int | (x14 >= 0)}
-> {x12 : Int | (x12 >= 0)} -> {x14 : Int | (x14 >= 0)})
-> {x14 : Int | (x14 >= 0)}
-> [{x12 : Int | (x12 >= 0)}]
-> {x14 : Int | (x14 >= 0)}foldl x1:Int -> x2:Int -> {x2 : Int | (x2 == (x1 + x2))}(+) {x2 : Int | (x2 == (0  :  int))}0 {x3 : [{x6 : Int | (x6 >= 0)}] | (x3 == xs) && ((len x3) >= 0)}xs
```

Recall
```106: foldl :: (α -> β -> α) -> α -> [β] -> α
```

How to instantiate `α` and `β` ?

## Function Subtyping

```120: (+) ::  x:Int -> y:Int -> {v:Int|v=x+y}
121:     <:  Nat   -> Nat   -> Nat
```

Because,

```130:                |- Nat       <: Int  -- Contra
131:   x:Nat, y:Nat |- {v = x+y} <: Nat  -- Co
```

Because,

```141:   0<=x && 0<=y && v = x+y   => 0 <= v
```

## Example: Summing `Nat`s

```149: {-@ sumNats :: [Nat] -> Nat @-}
150: sumNats xs  = foldl (+) 0 xs
```

Where:
```156: foldl :: (α -> β -> α) -> α -> [β] -> α
157: (+)   :: Nat -> Nat -> Nat
```

`sumNats` verified by instantiating `α,β := Nat`

`α` is loop invariant, instantiation is invariant synthesis

## Instantiation And Inference

Polymorphic instantiation happens everywhere...

... so automatic inference is crucial

Cannot use unification (unlike indexed approaches)

LiquidHaskell uses SMT and Abstract Interpretation.

## Iteration Dependence

Problem: Cannot use parametric polymorphism to verify

```198: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
199: x1:{v : Int | (v >= 0)}
-> x2:{v : Int | (v >= 0)}
-> {v : Int | (v == (x2 + x1)) && (v >= 0)}add {v : Int | (v >= 0)}n {v : Int | (v >= 0)}m = x1:{x22 : Int | (x22 == 0) && (x22 >= 0)}
-> x2:{x19 : Int | (x19 >= 0) && (x19 >= x1)}
-> {x16 : Int | (x16 >= 0) && (x16 >= n)}
-> ({x13 : Int | (x13 >= 0) && (x13 >= x1) && (x13 < x2)}
-> {x16 : Int | (x16 >= 0) && (x16 >= n)}
-> {x16 : Int | (x16 >= 0) && (x16 >= n)})
-> {x16 : Int | (x16 >= 0) && (x16 >= 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 iteration ...

... cannot instantiate `α := {v:Int | v = n + m}`

Problem: Need iteration-dependent invariants...    [Continue]