# Higher Order Specifications

```8: module Loop where
9: import Prelude hiding ((!!), length)
10: import SimpleRefinements
```

# 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:(GHC.Types.Int)
-> 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 (GHC.Types.Int)hi abase {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
-> a -> af        = {VV : (GHC.Types.Int) | (VV == 0) && (VV == lo) && (VV == (lo + lo)) && ((VV mod 2) == 0) && (VV >= 0)}
-> {VV : a | (VV == base)} -> 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)}
-> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi))}
-> {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)}
-> a
-> ago {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo)}i aacc | {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= lo) && (VV >= lo)}i x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x < y))}< {VV : (GHC.Types.Int) | (VV == hi) && (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi))}hi    = forall a.
lo:{VV : (GHC.Types.Int) | (VV == 0) && (VV == lo) && (VV == (lo + lo)) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi))}
-> {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)}
-> a
-> ago ({VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= lo) && (VV >= lo)}ix:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+{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)}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 :: L Int -> Int @-}
41: listSum     :: L Int -> Int
42: (SimpleRefinements.L (GHC.Types.Int)) -> (GHC.Types.Int)listSum (SimpleRefinements.L (GHC.Types.Int))xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:(GHC.Types.Int)
-> (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 == (llen 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 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ ({VV : (SimpleRefinements.L (GHC.Types.Int)) | (VV == xs)}xs ls:(SimpleRefinements.L (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen ls))}
-> (GHC.Types.Int)!! {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV < n)}i)
45:     {VV : (GHC.Types.Int) | (VV == (llen xs))}n       = xs:(SimpleRefinements.L (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}length {VV : (SimpleRefinements.L (GHC.Types.Int)) | (VV == xs)}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 :: L Nat -> Nat @-}
63: listNatSum     :: L Int -> Int
64: (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0)}listNatSum (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:(GHC.Types.Int)
-> {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 == (llen 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 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ ({VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)}) | (VV == xs)}xs ls:(SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen ls))}
-> {VV : (GHC.Types.Int) | (VV >= 0)}!! {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV < n)}i)
67:     {VV : (GHC.Types.Int) | (VV == (llen xs))}n          = xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}length {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)}) | (VV == xs)}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 :: L Even -> Even @-}
85: listEvenSum     :: L Int -> Int
86: (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}listEvenSum (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:(GHC.Types.Int)
-> {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 == (llen 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 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ ({VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}) | (VV == xs)}xs ls:(SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen ls))}
-> {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 == (llen xs))}n      = xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}length {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}) | (VV == xs)}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:(GHC.Types.Int)
-> {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 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ {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.