Measures and Case Splitting
Liquid Haskell has a flag called --no-case-expand
which can make verification of your code much faster,
especially when your code is using ADTs with many alternatives.
This flag says relax precision to get fast verification,
thus may lead to rejecting safe code.
In this post, I explain how --no-case-expand
works using a trivial example!
(Click here to demo)
28: 29: module MeasuresAndCaseSplitting where
Measures¶
Let's define a simple data type with three alternatives
40: data ABC = A | B | C
and a measure that turns ABD
into an integer
46: {-@ measure toInt @-} 47: toInt :: ABC -> Int 48: x1:MeasuresAndCaseSplitting.ABC -> {VV : GHC.Types.Int | VV == MeasuresAndCaseSplitting.toInt x1}toInt A = 1 49: toInt B = 2 50: toInt C = 3
Though obvious to us, Liquid Haskell will fail to check
that toInt
of any ABC
argument
gives back a natural number.
Or, the following call leads to a refinement type error.
59: {-@ unsafe :: x:ABC -> {o:() | 0 <= toInt x } @-} 60: unsafe :: ABC -> () 61: x1:MeasuresAndCaseSplitting.ABC -> {o : () | 0 <= MeasuresAndCaseSplitting.toInt x1}unsafe MeasuresAndCaseSplitting.ABCx = ()
Why?
By turning toInt
into a measure, Liquid Haskell
gives precise information to each data constructor of ABC
.
Thus it knows that toInt
or A
, B
, and C
is respectively 1
, 2
, and 3
, by automatically
generating the following types:
72: A :: {v:ABC | toInt v == 1 } 73: B :: {v:ABC | toInt v == 2 } 74: C :: {v:ABC | toInt v == 3 }
Thus, to get the toInt
information one need to
explicitly perform case analysis on an ABC
argument.
The following code is safe
82: {-@ safe :: x:ABC -> {o:() | 0 <= toInt x} @-} 83: safe :: ABC -> () 84: x1:MeasuresAndCaseSplitting.ABC -> {o : () | 0 <= MeasuresAndCaseSplitting.toInt x1}safe A = () 85: safe B = () 86: safe C = ()
Liquid Haskell type check the above code because
in the first case the body is checked under the assumption
that the argument, call it x
, is an A
.
Under this assumption, toInt x
is indeed non negative.
Yet, this is the case for the rest two alternatives,
where x
is either B
or C
.
So, 0 <= toInt x
holds for all the alternatives,
because case analysis on x
automatically reasons about the
value of the measure toInt
.
Now, what if I match the argument x
only with A
and provide a default body for the rest?
104: {-@ safeBut :: x:ABC -> {o:() | 0 <= toInt x} @-} 105: safeBut :: ABC -> () 106: x1:MeasuresAndCaseSplitting.ABC -> {o : () | 0 <= MeasuresAndCaseSplitting.toInt x1}safeBut A = () 107: safeBut _ = ()
Liquid Haskell knows that if the argument x
is actually an A
,
then toInt x
is not negative, but does not know the value of toInt
for the default case.
But, by default Liquid Haskell will do the the case expansion
of the default case for you and rewrite your code to match _
with all the possible cases.
Thus, Liquid Haskell will internally rewrite safeBut
as
119: {-@ safeButLH :: x:ABC -> {o:() | 0 <= toInt x} @-} 120: safeButLH :: ABC -> () 121: x1:MeasuresAndCaseSplitting.ABC -> {o : () | 0 <= MeasuresAndCaseSplitting.toInt x1}safeButLH A = () 122: safeButLH B = () 123: safeButLH C = ()
With this rewrite Liquid Haskell gets precision!
Thus, it has all the information it needs to prove safeBut
as safe.
Yet, it repeats the code of the default case,
thus verification slows down.
In this example, we only have three case alternatives, so we only repeat the code two times with a minor slow down. In cases with many more alternatives repeating the code of the default case can kill the verification time.
For that reason, Liquid Haskell comes with the no-case-expand
flag that deactivates this expansion of the default cases.
With the no-case-expand
flag on, the safeBut
code will not type check
and to fix it the user needs to perform the case expansion manually.
In short, the no-case-expand
increases verification speed
but reduces precision. Then it is up to the user
to manually expand the default cases, as required,
to restore all the precision required for the code to type check.