Higher-Order Functions

Types scale to Higher-Order Functions

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 = {v : Int | v >= 0 && v >= lo && v <= hi} -> a -> ago {v : Int | v == 0 && v == lo && v >= 0}lo {VV : a | VV == base}base
52:   where 
53:     {v : Int | v >= 0 && v >= lo && v <= hi} -> a -> ago {VV : Int | VV >= 0 && VV >= lo && VV <= hi}i aacc 
54:       | {v : Int | v == i && v >= 0 && v >= lo && v <= hi}i x1:Int -> x2:Int -> {v : Bool | Prop v <=> x1 < v}< {v : Int | v == hi && v >= 0 && v >= lo}hi    = {VV : Int | VV >= 0 && VV >= lo && VV <= hi} -> a -> ago ({v : Int | v == i && v >= 0 && v >= lo && v <= hi}ix1:Int -> x2:Int -> {v : Int | v == x1 + x2}+{v : Int | v == (1  :  int)}1) ({v : Int | v >= 0 && v >= lo && v < hi} -> a -> af {v : Int | v == i && v >= 0 && v >= lo && v <= hi}i {VV : a | VV == acc}acc)
55:       | otherwise = {VV : a | VV == acc}acc

By subtyping, we infer f called with values (Btwn lo hi)

Example: Summing Lists

67: forall a. (Num a) => [a] -> alistSum [a]xs     = x1:{v : Int | v == 0 && v >= 0}
-> x2:{v : Int | v >= 0 && v >= x1}
-> a
-> ({v : Int | v >= 0 && v >= x1 && v < x2} -> a -> a)
-> aloop {v : Int | v == (0  :  int)}0 {v : Int | v == n && v == len xs}n a0 {v : Int | v >= 0 && v < n} -> a -> abody 
68:   where 
69:     {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}+ ({v : [a] | v == xs && len v >= 0}xs x1:[a] -> {v : Int | v < len x1 && 0 <= v} -> a!! {v : Int | v == i && v >= 0 && v < n}i)
70:     {v : Int | v == len xs}n          = x1:[a] -> {v : Int | v == len x1}length {v : [a] | v == xs && len v >= 0}xs

79: loop :: l -> h -> α -> (Btwn l h -> α -> α) -> α

89: body :: Btwn 0 (llen xs) -> Int -> Int

Example: Summing Lists

97: listSum xs     = loop 0 n 0 body 
98:   where 
99:     body i acc = acc + (xs !! i)
100:     n          = length xs

Function Subtyping

108: body :: Btwn 0 (llen xs) -> Int -> Int

So i is Btwn 0 (llen xs); indexing !! is verified safe.

Polymorphic Instantiation

Example: Summing Nats

140: {-@ sumNats :: [Nat] -> Nat @-}
141: [{v : Int | v >= 0}] -> {v : Int | v >= 0}sumNats [{v : Int | v >= 0}]xs  = ({v : Int | v >= 0} -> {v : Int | v >= 0} -> {v : Int | v >= 0})
-> {v : Int | v >= 0} -> [{v : Int | v >= 0}] -> {v : Int | v >= 0}foldl x1:Int -> x2:Int -> {v : Int | v == x1 + v}(+) {v : Int | v == (0  :  int)}0 {v : [{v : Int | v >= 0}] | v == xs && len v >= 0}xs 

148: foldl :: (α -> β -> α) -> α -> [β] -> α

Function Subtyping

162: (+) ::  x:Int -> y:Int -> {v:Int|v=x+y} 
163:     <:  Nat   -> Nat   -> Nat

172:              |- Nat       <: Int  -- Contra (in)
173: x:Nat, y:Nat |- {v = x+y} <: Nat  -- Co    (out)

183:   0<=x && 0<=y && v = x+y   => 0 <= v

Example: Summing Nats

194: {-@ sumNats :: [Nat] -> Nat @-}
195: sumNats xs  = foldl (+) 0 xs 

201: foldl :: (α -> β -> α) -> α -> [β] -> α
202: (+)   :: Nat -> Nat -> Nat

Instantiation And Inference

Polymorphism ubiquitous, so inference is critical!

Iteration Dependence

Problem: Cannot use parametric polymorphism to verify

257: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
258: 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:{v : Int | v == 0 && v >= 0}
-> x2:{v : Int | v >= 0 && v >= x1}
-> {v : Int | v >= 0 && v >= n}
-> ({v : Int | v >= 0 && v >= x1 && v < x2}
    -> {v : Int | v >= 0 && v >= n} -> {v : Int | v >= 0 && v >= n})
-> {v : Int | v >= 0 && v >= n}loop {v : Int | v == (0  :  int)}0 {v : Int | v == m && v >= 0}m {v : Int | v == n && v >= 0}n ({v : Int | v >= 0 && v < m}
-> x2:{v : Int | v >= 0 && v >= n}
-> {v : Int | v > 0 && v > x2 && v > n && v >= 0}\_ {VV : Int | VV >= 0 && VV >= n}i -> {v : Int | v == i && v >= 0 && v >= n}i x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+ {v : Int | v == (1  :  int)}1)