\( \require{color} \definecolor{kvcol}{RGB}{203,23,206} \definecolor{tycol}{RGB}{5,177,93} \definecolor{refcol}{RGB}{18,110,213} \newcommand{\quals}{\mathbb{Q}} \newcommand{\defeq}{\ \doteq\ } \newcommand{\subty}{\preceq} \newcommand{\True}{\mathit{True}} \newcommand{\Int}{\mathtt{Int}} \newcommand{\Nat}{\mathtt{Nat}} \newcommand{\Zero}{\mathtt{Zero}} \newcommand{\foo}[4]{{#1}^{#4} + {#2}^{#4} = {#3}^{#4}} \newcommand{\reft}[3]{\{\bindx{#1}{#2} \mid {#3}\}} \newcommand{\ereft}[3]{\bindx{#1}{\{#2 \mid #3\}}} \newcommand{\bindx}[2]{{#1}\!:\!{#2}} \newcommand{\reftx}[2]{\{{#1}\mid{#2}\}} \newcommand{\inferrule}[3][]{\frac{#2}{#3}\;{#1}} \newcommand{\kvar}[1]{\color{kvcol}{\mathbf{\kappa_{#1}}}} \newcommand{\llen}[1]{\mathtt{llen}(#1)} \)

Evaluation

Evaluation

LiquidHaskell Is For Real


Substantial code bases.


Complex properties.


Inference is crucial.

Numbers

Library LOC
Data.List 814
Data.Set.Splay 149
Data.Vector.Algorithms 1219
Data.Map.Base 1396
Data.Text 3125
Data.Bytestring 3501
Total 10224

Numbers

Library LOC Time
Data.List 814 52s
Data.Set.Splay 149 26s
Data.Vector.Algorithms 1219 196s
Data.Map.Base 1396 247s
Data.Text 3125 809s
Data.Bytestring 3501 549s
Total 10224 1880s

Termination

Proving termination is easy in practice.


  • 503 recursive functions
  • 67% automatically proved
  • 30% need witnesses /[...]
  • 1 witness per 100 lines of code
  • 20 not proven to terminate
  • 12 do not terminate (e.g. top-level IO loops)
  • 8 currently outside scope of LiquidHaskell