Division By Zero

λ> let average xs = sum xs `div` length xs

λ> average [100, 202, 300]
2

λ> average []
*** Exception: divide by zero

Missing Keys

λ> :m +Data.Map
λ> let m = fromList [ ("haskell"    , "lazy")
                    , ("javascript" , "eager")]

λ> m ! "haskell"
"lazy"

λ> m ! "clojure"
"*** Exception: key is not in the map

Segmentation Faults

λ> :m +Data.Vector
λ> let v = fromList ["haskell", "javascript"]
λ> unsafeIndex v 0
"haskell"

λ> V.unsafeIndex v 3

'ghci' terminated by signal SIGSEGV ...

"HeartBleeds"

λ> :m + Data.Text Data.Text.Unsafe
λ> let t = pack "StrangeLoop"
λ> takeWord16 5 t
"Stran"

Memory overflows leaking secrets...

λ> takeWord16 20 t
"StrangeLoop\1912\3148\NUL\15928\2486\SOH\NUL"

Goal: Extend Type System

• To prevent wider class of errors

• To enforce program specific properties

Plan

Part I: Refinement Types

• Refinements
• Data Types

Part II: Case Studies

• Insertion Sort
• Well Scoped Evaluator
• Low-level Memory

Evaluation

• Diverse Code Bases

• 10KLoc / 56 Modules

• Memory Safety, Termination, Functional Correctness

Inference is Crucial

Evaluation

• Specifications: 1 / 10 LOC (ok)

• Compile Time: 1s / 10 LOC (not ok!)

Conclusion

Refinement Types: Automated Dependent Typing via SMT

Current & Future Work

• GHC Integration
• Faster Checking
• Easier Errors
• Code Synthesis

Thank You!

http://www.refinement-types.org