Liquid Types For Haskell

Ranjit Jhala

University of California, San Diego

Joint work with:

N. Vazou, E. Seidel, P. Rondon, D. Vytiniotis, S. Peyton-Jones

29: {x2 : (IO ()) | (x2 == Main.main)}main = [Char] -> (IO ())putStrLn {x2 : [Char] | ((len x2) >= 0)}"Easter Egg: to force Makefile"

Division By Zero

46: λ> let average xs = sum xs `div` length xs
47: 
48: λ> average [1,2,3]
49: 2

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

Missing Keys

67: λ> :m +Data.Map 
68: λ> let m = fromList [ ("haskell", "lazy")
69:                     , ("ocaml"  , "eager")]
70: 
71: λ> m ! "haskell"
72: "lazy"

78: λ> m ! "javascript"
79: "*** Exception: key is not in the map

Segmentation Faults

88: λ> :m +Data.Vector 
89: λ> let v = fromList ["haskell", "ocaml"]
90: λ> unsafeIndex v 0
91: "haskell"

97: λ> V.unsafeIndex v 3
98: 
99: 
100: 'ghci' terminated by signal SIGSEGV ...

"HeartBleeds"

109: λ> :m + Data.Text Data.Text.Unsafe 
110: λ> let t = pack "Kanazawa"
111: λ> takeWord16 5 t
112: "Kanaz"

123: λ> takeWord16 20 t
124: "Kanazawa\1912\3148\SOH\NUL\15928\2486\SOH\NUL"

Goal

Extend Hindley-Milner To Prevent More Errors

LiquidHaskell

Automatic

Liquid Types, PLDI 08

• Abstract Interpretation

• SMT Solvers

Expressive

This talk ...

Try Yourself

google: "liquidhaskell demo"

[continue]

Plan

1. Refinements
2. Measures
3. Higher-Order Functions
4. Abstract Refinements: Code, Data,...,...
5. Lazy Evaluation
6. Termination
7. Evaluation