11_Evaluation.lhs

 {#ASda}
========

Evaluation
----------

<div class="hidden">

\begin{code}
main = putStrLn "Easter Egg: to force Makefile"
\end{code}

</div>


Evaluation
==========

LiquidHaskell 
-------------

<br>

**Diverse Code Bases**

<br>

10KLoc

<br>

56 Modules

LiquidHaskell 
-------------

<br>

**Complex Properties**

<br>

Memory Safety


Functional Correctness*


Termination

<br>

<div class="fragment">
**Inference is Crucial**
</div>

Benchmarks
----------

<div align="center">

**Library**                     
---------------------------   ---------
`XMonad.StackSet`                      
`Data.List`                         
`Data.Set.Splay`                    
`Data.Vector.Algorithms`           
`HsColour`                        
`Data.Map.Base`                
`Data.Text`                        
`Data.Bytestring`                  
---------------------------   ---------

</div>


Benchmarks 
----------

<div align="center">

**Library**                     **LOC**
---------------------------   ---------
`XMonad.StackSet`                   256 
`Data.List`                         814
`Data.Set.Splay`                    149
`Data.Vector.Algorithms`           1219
`HsColour`                         1047
`Data.Map.Base`                    1396
`Data.Text`                        3128
`Data.Bytestring`                  3505
**Total**                     **11512**
---------------------------   ---------

</div>

Benchmarks
----------

<div align="center">

**Library**                     **LOC**     **Specs**    
---------------------------   ---------   -----------    
`XMonad.StackSet`                   256            74    
`Data.List`                         814            46    
`Data.Set.Splay`                    149            27    
`Data.Vector.Algorithms`           1219            76    
`HsColour`                         1047            19    
`Data.Map.Base`                    1396           125    
`Data.Text`                        3128           305    
`Data.Bytestring`                  3505           307    
**Total**                     **11512**       **977**    
---------------------------   ---------   -----------    

</div>


Code v. Specs 
-------------

<img src="../img/code-spec-indiv.png" height=400px>


Code v. Specs 
-------------

<br>

<img src="../img/code-spec-total.png" height=100px>
 
**About 8.5%**

*Very* coarse measure...

Running Time
------------

<div align="center">

**Library**                     **LOC**     **Specs**      **Time**
---------------------------   ---------   -----------    ----------
`XMonad.StackSet`                   256            74          27s
`Data.List`                         814            46          26s
`Data.Set.Splay`                    149            27          27s
`Data.Vector.Algorithms`           1219            76          89s 
`HsColour`                         1047            19         196s
`Data.Map.Base`                    1396           125         174s
`Data.Text`                        3128           305         499s
`Data.Bytestring`                  3505           307         294s
**Total**                     **11512**       **977**    **1336s**
---------------------------   ---------   -----------    ----------

</div>



 {#comments}
============

Types as Comments
-----------------

<br>

**Types are Machine Checked Comments**

<br>

+ Express same *requirements*

+ But *connected to* code

<br>

<div class="fragment">
**Always in sync as code changes**
</div>

Liquid Types as Machine Checked Comments
========================================

Example: Data.Map
-----------------

<br>

**Requirement**

<br>

`Map a b` is a *binary search* ordered tree

Example: Data.Map
-----------------

**Comment**

\begin{spec}
-- @join@ assumes that all values in [l] < [k]
-- and all values in [r] > [k], and
-- that [l] and [r] are valid trees.
\end{spec}

<br>

<div class="fragment">

**Type**

\begin{spec}
join :: k:a -> b
     -> l:Map {v:a | v < k} b
     -> r:Map {v:a | v > k} b
     -> Map a b 
\end{spec}

</div>

Example: Data.ByteString
------------------------

<br>

**Requirement**

<br>

Fast, low-level indices into a `ByteString` must be in bounds.


Example: Data.ByteString
------------------------

**Comment**

\begin{spec}
-- Unsafe 'ByteString' index (subscript) ...
-- omits the bounds check, which means there
-- is an obligation to ensure the bounds are
-- checked in some other way.
\end{spec}

<br>

<div class="fragment">

**Type**

\begin{spec}
unsafeIndex :: b:ByteString
            -> {v:Nat | v < bLength b}
            -> Word8 
\end{spec}

</div>

Example: Data.ByteString
------------------------

<br>

**Requirement**

<br>

Fast *truncation* requires valid size.


Example: Data.ByteString
------------------------

**Comment**

\begin{spec}
-- omits the checks on @n@ so there is
-- an obligation to provide a proof
-- that @0 <= n <= 'length' xs@             
\end{spec}

<br>

<div class="fragment">
**Type**

\begin{spec}
unsafeTake :: n:Nat
           -> {v:ByteString | n <= bLength v}
           -> {v:ByteString | n = bLength v} 
\end{spec}

</div>

 {#cont}
=========


Continue
--------

<br>
<br>
<br>

[[continue...]](12_Conclusion.lhs.slides.html)

 {#recap}
=========


Recap
-----

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Strengthened Constructors
4. Abstract: Refinements over functions and data
5. **Evaluation**
6. <div class="fragment"><a href="12_Conclusion.lhs.slides.html" target="_blank">Conclusion</a></div>

<br>
<br>