Division By Zero

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

λ> average [100, 202, 300]
2

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

Partial Functions

λ> head "compose"
'c'

λ> head []
*** Exception: Prelude.head: empty list

Fuctional Correctness

λ> sort [42, 5, 3, 1]
[5, 3]

λ> (incr . incr) 40
0

Goal: Extend Type System

• To prevent wider class of errors

• To enforce program specific properties

Plan

1. Refinements Types
2. Data Types
3. Abstract Refinements
4. Bounded Refinements

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

Thank You!

cabal install liquidhaskell
http://www.refinement-types.org
online demo @ http://goto.ucsd.edu/liquidhaskell