Refinement Types For Haskell ============================ {#berg} -------- <br> + Niki Vazou + Eric Seidel + *Ranjit Jhala* <br> **UC San Diego** <div class="hidden"> <pre><span class=hs-linenum>20: </span><a class=annot href="#"><span class=annottext>{x2 : (IO ()) | (x2 == Main.main)}</span><span class='hs-definition'>main</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>[(Char)] -> (IO ())</span><span class='hs-varid'>putStrLn</span></a> <a class=annot href="#"><span class=annottext>{x3 : [(Char)] | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-str'>"Easter Egg"</span></a> </pre> </div> Install ------- <br> `cabal install liquidhaskell` <br> <div class="fragment"> Requires an SMTLIB2 binary <br> + `http://z3.codeplex.com` + `http://cvc4.cs.nyu.edu` + `http://mathsat.fbk.eu` </div> Try Online ---------- <br> `http://goto.ucsd.edu/liquid/haskell/demo` Follow Slides ------------- <br> `goto.ucsd.edu/~rjhala/liquid/haskell/plpv/lhs/` {#plan} -------- 1. <div class="fragment"><a href="01_SimpleRefinements.lhs.slides.html" target= "_blank">Refinements</a></div> 2. <div class="fragment"><a href="02_Measures.lhs.slides.html" target= "_blank">Measures</a></div> 3. <div class="fragment"><a href="03_HigherOrderFunctions.lhs.slides.html" target= "_blank">Higher-Order Functions</a></div> 4. <div class="fragment"><a href="04_AbstractRefinements.lhs.slides.html" target= "_blank">Abstract Refinements</a></div> - <div class="fragment"><a href="05_Composition.lhs.slides.html" target="_blank">Dependency</a><a href="06_Inductive.lhs.slides.html" target= "_blank">, Induction</a> <a href="07_Array.lhs.slides.html" target= "_blank">, Indexing</a> <a href="08_Recursive.lhs.slides.html" target= "_blank">, Recursion</a></div> 5. <div class="fragment"><a href="09_Laziness.lhs.slides.html" target="_blank">Lazy Evaluation</a></div> 6. <div class="fragment"><a href="10_Termination.lhs.slides.html" target="_blank">Termination</a></div> <!-- [Higher Order Functions](03_HigherOrderFunctions.lhs.slides.html) </div> 4. <div class="fragment"> [Abstract Refinements](04_AbstractRefinements.lhs.slides.html) </div> - <div class="fragment">[Dependency](05_Composition.lhs.slides.html), [Induction](06_Inductive.lhs.slides.html), [Indexing](07_Array.lhs.slides.html), [Recursion](08_Recursive.lhs.slides.html) </div> 5. <div class="fragment"> [Lazy Evaluation](09_Laziness.lhs.slides.html) </div> 6. <div class="fragment"> [Termination](10_Termination.lhs.slides.html) </div> --> Evaluation ========== LiquidHaskell Is For Real ------------------------- <br> Substantial code bases, tricky properties. <br> <div class="fragment">Inference, FTW.</div> Numbers ------- <div align="center"> **Library** LOC --------------------------- ------ `GHC.List` 310 `Data.List` 504 `Data.Set.Splay` 149 `Data.Vector.Algorithms` 1219 `Data.Map.Base` 1396 `Data.Text` 3125 `Data.Bytestring` 3501 --------------------------- ------ </div> Evaluation: Termination ----------------------- How bad is *termination* requirement anyway? - <div class="fragment">`520` recursive functions</div> - <div class="fragment">`67%` automatically proved</div> - <div class="fragment">`30%` need *witnesses* `/[...]`</div> - <div class="fragment">`18` *not proven terminating*</div> - <div class="fragment">`12` don't actually terminate (top-level `IO`)</div> - <div class="fragment">`6` *probably* terminate, but *we* can't tell why.</div> Future Work ----------- - Error Messages - Speed - Case Studies Thank You! ---------- `cabal install liquidhaskell`