Standard Refinement Types

























Division by Zero


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

To run Liquid Haskell on your Refinements.lhs file

  • Here: Press Play

  • Locally:

cabal install liquidhaskell
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.












Head of lists


Another check: head on only non-empty lists.


headEmp :: () -> a headEmp _ = head []


Q: Can you fix the error?












Head on variables

headxs :: [a] -> a headxs xs = head xs

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

Reminder of Haskell Heartbleed.

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

Detect Heartbleed with Liquid Haskell.

{-@ 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