Refinement Types for Haskell

Niki Vazou (University of California, San Diego)






With: R. Jhala, E. Seidel, P. Rondon, D. Vytiniotis, S. P. Jones, ...










Well-Typed Programs Can Go Wrong



















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 ! "racket"
*** Exception: key is not in the map













Unexpected Behaviors

λ> sort [1, 2, 3]
[1, 2, 3]

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













Non Termination

λ> let fact n = n * fact (n-1)
λ> fact 42














"HeartBleeds"

λ> :m + Data.Text Data.Text.Unsafe
λ> let t = pack "CUFP2015"
λ> takeWord16 4 t
"CUFP"


Memory overflows leaking secrets...


λ> takeWord16 20 t
"CUFP2015\2043\9834\1912\3148\NUL\15928\2486\SOH\NUL"













Goal: Extend Type System



  • To prevent wider class of errors

  • To enforce program specific properties

  • Reason about semantics (apart from structural) properties











Plan

Part I: Features



Part II: Case Studies













Conclusion


Refinement Types: Automated Dependent Typing via SMT


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













Current & Future Work


Expressiveness

How expressive is decidable logic?

  • how to "fake" functions?
  • what can/cannot be expressed?













Current & Future Work


Technology


  • GHC
  • Speed
  • Error Messages













Current & Future Work


Applications


  • Testing
  • Security
  • Machine Learning
  • Web frameworks
  • Concurrency













Thank You!



http://www.refinement-types.org