# Higher Order Specifications

```8: module Loop where
9:
10: {-@ LIQUID "--no-termination"@-}
```

# Higher Order Specifications

Consider a `loop` function:

```20: loop :: Int -> Int -> a -> (Int -> a -> a) -> a
21: forall a.
lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}
-> a
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
-> a -> a)
-> aloop {VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}lo {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}hi abase {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
-> a -> af        = {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)}
-> a -> ago {VV : (GHC.Types.Int) | (VV == 0) && (VV == lo) && ((VV mod 2) == 0) && (VV >= 0)}lo {VV : a | (VV == base)}base
22:   where
23:     forall a.
lo:{VV : (GHC.Types.Int) | (VV == 0) && (VV == lo) && (VV == (lo + lo)) && ((VV mod 2) == 0) && (VV >= 0) && (VV <= hi)}
-> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi)) && (VV >= 0) && (VV >= lo) && (VV >= lo)}
-> {VV : a | (VV == base)}
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi)}
-> a -> a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}
-> a
-> ago {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}i aacc | {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}i x1:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 < x2))}< {VV : (GHC.Types.Int) | (VV == hi) && (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi)) && (VV >= 0) && (VV >= lo) && (VV >= lo)}hi    = forall a.
lo:{VV : (GHC.Types.Int) | (VV == 0) && (VV == lo) && (VV == (lo + lo)) && ((VV mod 2) == 0) && (VV >= 0) && (VV <= hi)}
-> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi)) && (VV >= 0) && (VV >= lo) && (VV >= lo)}
-> {VV : a | (VV == base)}
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi)}
-> a -> a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}
-> a
-> ago ({VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}ix1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+{VV : (GHC.Types.Int) | (VV == (1  :  int))}1) ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi)}
-> a -> af {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}i {VV : a | (VV == acc)}acc)
24:              | otherwise = {VV : a | (VV == acc)}acc
```

• if `lo <= hi` then `f` called with `lo <= i < hi`

# Higher Order Specifications

Lets use `(!!)` to write a function that sums an `Int` list

```40: {-@ listSum :: [Int] -> Int @-}
41: listSum     :: [Int] -> Int
42: [(GHC.Types.Int)] -> (GHC.Types.Int)listSum [(GHC.Types.Int)]xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}
-> (GHC.Types.Int)
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
-> (GHC.Types.Int) -> (GHC.Types.Int))
-> (GHC.Types.Int)loop {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == n) && (VV == (len xs))}n {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> (GHC.Types.Int) -> (GHC.Types.Int)body
43:   where
44:     {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> (GHC.Types.Int) -> (GHC.Types.Int)body    = \{VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}i (GHC.Types.Int)acc -> {VV : (GHC.Types.Int) | (VV == acc)}acc x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ ({VV : [(GHC.Types.Int)] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs x1:[(GHC.Types.Int)]
-> {VV : (GHC.Types.Int) | (VV < (len x1)) && (0 <= VV)}
-> (GHC.Types.Int)!! {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV < n)}i)
45:     {VV : (GHC.Types.Int) | (VV == (len xs))}n       = x1:[(GHC.Types.Int)] -> {VV : (GHC.Types.Int) | (VV == (len x1))}length {VV : [(GHC.Types.Int)] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs
```

• `body` called with `0 <= i < llen xs`
• hence, indexing safe.

Demo: Let's change the `0` to `-1` and see what happens!

# Higher Order Specifications

We can give this function a better type:

```62: {-@ listNatSum :: [Nat] -> Nat @-}
63: listNatSum     :: [Int] -> Int
64: [{VV : (GHC.Types.Int) | (VV >= 0)}]
-> {VV : (GHC.Types.Int) | (VV >= 0)}listNatSum [{VV : (GHC.Types.Int) | (VV >= 0)}]xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0)}loop {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == n) && (VV == (len xs))}n {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> acc:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= acc)}body
65:   where
66:     {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> acc:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= acc)}body       = \{VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}i {VV : (GHC.Types.Int) | (VV >= 0)}acc -> {VV : (GHC.Types.Int) | (VV == acc) && (VV >= 0)}acc x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ ({VV : [{VV : (GHC.Types.Int) | (VV >= 0)}] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs x1:[{VV : (GHC.Types.Int) | (VV >= 0)}]
-> {VV : (GHC.Types.Int) | (VV < (len x1)) && (0 <= VV)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}!! {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV < n)}i)
67:     {VV : (GHC.Types.Int) | (VV == (len xs))}n          = x1:[{VV : (GHC.Types.Int) | (VV >= 0)}]
-> {VV : (GHC.Types.Int) | (VV == (len x1))}length {VV : [{VV : (GHC.Types.Int) | (VV >= 0)}] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs
```

To verify this type, note: `(+) :: Nat -> Nat -> Nat`

LiquidHaskell instantiates `a` in `loop` with `Nat`

• `loop :: Int -> Int -> Nat -> (Int -> Nat -> Nat) -> Nat`

Yielding the output.

# Higher Order Specifications

By the same analysis, LiquidHaskell verifies that

```84: {-@ listEvenSum :: [Even] -> Even @-}
85: listEvenSum     :: [Int] -> Int
86: [{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}]
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}listEvenSum [{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}]xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}loop {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == n) && (VV == (len xs))}n {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}body
87:   where {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}body   = \{VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}i {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}acc -> {VV : (GHC.Types.Int) | (VV == acc) && ((VV mod 2) == 0)}acc x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ ({VV : [{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs x1:[{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}]
-> {VV : (GHC.Types.Int) | (VV < (len x1)) && (0 <= VV)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}!! {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV < n)}i)
88:         {VV : (GHC.Types.Int) | (VV == (len xs))}n      = x1:[{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}]
-> {VV : (GHC.Types.Int) | (VV == (len x1))}length {VV : [{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs
```

Here, the system deduces that `(+)` has type

• `x:Int-> y:Int -> {v:Int| v=x+y} <: Even -> Even -> Even`

Hence, verification proceeds by instantiating `a` with `Even`

• `loop :: Int -> Int -> Even -> (Int -> Even -> Even) -> Even`

# Another Example

Consider a simpler example:

```107: {-@ add :: n:Nat -> m:Nat -> {v:Int| v = m + n} @-}
108: add     :: Int -> Int -> Int
109: n:{VV : (GHC.Types.Int) | (VV >= 0)}
-> m:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == (m + n))}add {VV : (GHC.Types.Int) | (VV >= 0)}n {VV : (GHC.Types.Int) | (VV >= 0)}m = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)}
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)})
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)}loop {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == m) && (VV >= 0)}m {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n ({VV : (GHC.Types.Int) | (VV >= 0) && (VV < m)}
-> i:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)}
-> {VV : (GHC.Types.Int) | (VV > 0) && (VV > i) && (VV > n) && (VV >= 0)}\_ {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)}i -> {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= n)}i x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
```

Cannot use parametric polymorphism as before!

• Cannot instantiate `a` with `{v:Int|v = n + m}` ...
• ... as this only holds after last iteration of loop!

Require Higher Order Invariants

• On values computed in intermediate iterations...
• ... i.e. invariants that depend on the iteration index.