Standard Refinement Types

Division by Zero

module Refinements where div0 :: () -> Int div0 _ = 42 div 0

• Here: Press Play

• Locally:

liquid Foo.lhs

Division by a variable.

The input x might be 0.

divx :: Int -> Int divx x = 42 div x

Fixes:

• Divide with a provably non-zero value (e.g., x*x+1)

• Make divx only accept non-zero arguments.

Constrain Propagation

Now you can only call divx on non-zero inputs!

readDivx :: IO Int readDivx = do i <- getLine let x = read i :: Int return \$ divx x

Q: Change the code to only call divx on non-zero.

Q: What if the call to div in divx changes?

Refinement Types

Refinements of Haskell types with logical predicates!

{-@ divx :: x:{Int | x /= 0} -> Int @-}

The special comments {-@ ... @-} are

• interpreted by Liquid Haskell, but

• ignored by ghc.

Another check: head on only non-empty lists.

Q: Can you fix the error?

Fixes:

• Make the list (provably) nonempty

• Better, refine the type to only accept nonempty lists!

List Appending

{-@ headxsys :: [a] -> xs:{[a] | 0 < len xs } -> a @-} headxsys :: [a] -> [a] -> a headxsys ys xs = head (xs ++ ys)

The type is good, but too restrictive.

Q: Can you make the below pass?

foo :: () -> Int foo _ = headxsys [1, 2, 3] []

Example: Avegerage on Lists

{-@ avg :: [Int] -> Int @-} avg :: [Int] -> Int avg xs = sum xs div length xs

Q: Can you fix the type error?

We saw verification under two constraints

{-@ div  :: Int -> x:{Int | 0 /= x } -> Int @-}

{-@ head :: xs:{[a] | 0 < len xs } -> a @-}

Where do these constraints come from?

What takes to verify take?

{-@ safeTake :: i:Int -> xs:[a] -> [a] @-} safeTake :: Int -> [a] -> [a] safeTake 0 [] = [] safeTake i (x:xs) = if i == 0 then [] else x:safeTake (i-1) xs safeTake i [] = error "Out of bounds indexing!"

Q: Can you fix the error?

In-bounds indexing to prevent Heartbleed

λ> :m +Data.Text Data.Text.Unsafe
λ>  takeWord16 10 (pack "zurihac")
"zurihac\NUL\26984\1930"

{-@ takeWord16 :: i:Nat -> xs:{Text | i < tlen xs } -> Text @-} heartbleed :: Text heartbleed = takeWord16 10 (pack "zurihac")

Length of a Text

{-@ takeWord16 :: i:Nat -> xs:{Text | i < tlen xs } -> Text @-}

Define logical functions as measures.

{-@ measure tlen :: Text -> Int @-} {-@ pack :: s:String -> {t:Text | len s == tlen t} @-} safe :: Text safe = takeWord16 4 (pack "zurihac") unsafe :: Text unsafe = takeWord16 10 (pack "zurihac") {-@ depends :: i:{Nat | i < 7 } -> Text @-} depends :: Int -> Text depends i = takeWord16 i (pack "zurihac")

Recap

• Refinement Types: Haskell Types + Predicates

• Used to:

• Catch runtime crashing.

• Propagate & discharge constraints.

• Remove runtime checks (make unsafe functions safe!).

• Other checked properties: Totality & Termination

Appendix

{-@ LIQUID "--no-termination" @-}
data Text = Text pack :: String -> Text pack _ = undefined takeWord16 :: Int -> Text -> Text takeWord16 _ _ = Text