\begin{code}

λ> let average xs = sum xs `div` length xs λ> average [1,2,3] 2 \end{code}

\begin{code}
λ> average [] *** Exception: divide by zero \end{code}

Missing Keys ------------

\begin{code}

λ> :m +Data.Map λ> let m = fromList [ ("haskell", "lazy") , ("ocaml" , "eager")] λ> m ! "haskell" "lazy" \end{code}

\begin{code}
λ> m ! "javascript" "*** Exception: key is not in the map \end{code}

Segmentation Faults -------------------

\begin{code}

λ> :m +Data.Vector λ> let v = fromList ["haskell", "ocaml"] λ> unsafeIndex v 0 "haskell" \end{code}

\begin{code}
λ> V.unsafeIndex v 3 'ghci' terminated by signal SIGSEGV ... \end{code}

"HeartBleeds" ------------- \begin{code}

λ> :m + Data.Text Data.Text.Unsafe λ> let t = pack "Kanazawa" λ> takeWord16 5 t "Kanaz" \end{code}

Memory overflows **leaking secrets**...
\begin{code}

λ> takeWord16 20 t "Kanazawa\1912\3148\SOH\NUL\15928\2486\SOH\NUL" \end{code}

Goal ---- Extend Hindley-Milner To Prevent More Errors Liquid Types for Haskell ======================== LiquidHaskell -------------

Refine **types** with **predicates**

**Expressive** specification & **Automatic** verification

Automatic --------- [Liquid Types, PLDI 08](http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf)
+ Abstract Interpretation (covered briefly...) + SMT Solvers Expressive ----------

This talk ... Try Yourself ------------
**google: ** `"liquidhaskell demo"` {#zog} --------

[[continue]](01_SimpleRefinements.lhs.slides.html) Plan ---- + Refinements +

Measures

Higher-Order Functions

Abstract Refinements: Code, Data,...,...