Programming with Refinement Types

Ranjit Jhala (University of California, San Diego)

Well-Typed Programs Can Go Wrong

Division By Zero

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

λ> average [100, 202, 300]

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

Missing Keys

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

λ> m ! "haskell"

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

Segmentation Faults

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

λ> V.unsafeIndex v 3

'ghci' terminated by signal SIGSEGV ...


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

Memory overflows leaking secrets...

λ> takeWord16 20 t

Goal: Extend Type System

  • To prevent wider class of errors

  • To enforce program specific properties


Part I: Refinement Types

Part II: Case Studies


  • Diverse Code Bases

  • 10KLoc / 56 Modules

  • Memory Safety, Termination, Functional Correctness

Inference is Crucial


  • Specifications: 1 / 10 LOC (ok)

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


Refinement Types: Automated Dependent Typing via SMT

Properties: Predicates + Types
Proofs: SMT Solvers + Subtyping
Inference: Abstract Interpretation + Hindley-Milner

Current & Future Work

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

Thank You!