Some questions about using liquid haskell

[Alex Rozenshteyn]

I'm trying to get a working understanding of Liquid Haskell. In a "Dive into" approach, I'm trying to verify a leftist heap implementation (adapted from http://typeocaml.com/2015/03/12/heap-leftist-tree/).

I'm following the tutorial, paying close attention to the AVL tree chapter. I'm making progress, but I have a bunch of questions. I'm attaching my current draft; comments starting with "TODO" are my questions, and I'll replicate them here.

Is it possible to avoid record syntax when defining refined data types?
Is it ossible to avoid data refinement altogether, relying on smart constructors?
`OHeap` and `LHeap` are two refinements on `Heap`; how could they be changed so that they compose?
When is it appropriate to use a refinement which exposes some property (e.g. depth) in its type?
Why doesn't LH figure out that a `Leaf` has rank 0?

I want to figure this out mostly on my own, but I think that it's about time I stopped flailing and asked some questions, hopefully learning things in the process.

[Ranjit Jhala]

Hi Alex,

I have an edited version of your file at:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1455686166_1282.hs

Now all the specs are verified _except_ the call to `Branch` inside `merge` 

which currently in fact violates the specification.

Let me try to answer your great questions (which have also pointed out 

some nasty LH issues that we will fix!)

1. You need not have signatures in measure definitions, i.e. it should just be:

   {-@ measure rank @-} 

   not 

   {-@ measure rank :: Heap a -> Int @-}

   Writing the former _should_ return an error message, but it doesn't, 

   which is something we will fix!

2. When using Boolean measures, you need not write `Prop` i.e. instead of

< {-@ type LHeap a = {v:Heap a | Prop (isLeftist v)} @-}

< {-@ type OLHeap a X = {v:OHeap a X | Prop (isLeftist v)} @-}

   just write:

    

> {-@ type LHeap a = {v:Heap a | (isLeftist v)} @-}

> {-@ type OLHeap a X = {v:OHeap a X | (isLeftist v)} @-}

   Writing `Prop` _should_ return a nice error message but 

   unfortunately it doesn't which is clearly a bug in LH 

   that we should fix!

3. You cannot use arbitrary Haskell code in measures, e.g. 

   `min` in the definition of rank; they must be terms that 

   can be "lifted" into the refinement logic (i.e. belong in 

   the logic.) Thus, I have defined a `min` and used it here 

   instead. 

> {-@ inline min @-}

> min :: Int -> Int -> Int

> min x y = if x < y then x else y

   You can then use such functions via via the {-@ inline min @-} 

   pragma. (As described also in the AVL chapter.)

4. I think you missed a "1 +" in the rank for leaf (otherwise the 

   rank is always 0), so I did that:

<   Branch _ l r -> min (rank l) (rank r)

---

>   Branch _ l r -> 1 + min (rank l) (rank r)

​No​w turning to your questions:

 

Is it possible to avoid record syntax when defining refined data types?
Is it ossible to avoid data refinement altogether, relying on smart constructors?

​​

​5. Yes, in gene​val you need not have such constructors, but in 

   your specific case, where the types of one field *depend on* another 

   (here, l and r depend on elt) you have to refine the data type.

   For example, suppose you just want an ordered pair:

   {-@ data OP = OP {x :: Int, y :: {v : Int | x < v} } @-}

   

   you could imagine a smart constructor:

   op ::x:Int -> {v: Int | x < v} -> OP 

   but this is not enough when you *destruct* the pair e.g. 

   via pattern matching:

   case p of 

     OP a b -> assert (a < b)

   In theory you could solve this problem using "smart destructors" 

   instead of pattern matching, but it could get a bit tedious.

   The other benefit of refining the data type is that you "declaratively" 

   specify the invariants in exactly one place without having to worry 

   about "how" the values were created (e.g. what if you found some way 

   to build a tree without using a smart constructor?)

6.

`OHeap` and `LHeap` are two refinements on `Heap`; how could they be changed so that they compose?

​In this case, I would just eliminate LHeap and write OLHeap the way you have.

In principle we could imagine a mechanism like:

    {-@ type OLHeap a X = OHeap a X /\ LHeap a @-}

​but we ​haven't implemented such a thing yet.

​7.

​

When is it appropriate to use a refinement which exposes some property (e.g. depth) in its type?

​Hmm,​ thats a tricky one -- in general, I'd say whenever you need to reason 

about that property. (But perhaps I've misunderstood the question?)

​​

Why doesn't LH figure out that a `Leaf` has rank 0?

​Now it does!

 

I want to figure this out mostly on my own, but I think that it's about time I stopped flailing and asked some questions, hopefully learning things in the process.

Points 1-3 *should* have been reported as spec/syntax errors, which 

would probably have saved you a great deal of effort. Apologies for that

and thanks for pointing these out!

Let me know if you need any clarifications!

Best,

Ranjit.

[Alex Rozenshteyn]

On Wed, Feb 17, 2016 at 12:38 AM Ranjit Jhala <jh...@cs.ucsd.edu> wrote:

Hi Alex,

I have an edited version of your file at:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1455686166_1282.hs

 

Thank you!

Now all the specs are verified _except_ the call to `Branch` inside `merge` 

which currently in fact violates the specification.

Let me try to answer your great questions (which have also pointed out 

some nasty LH issues that we will fix!)

1. You need not have signatures in measure definitions, i.e. it should just be:

   {-@ measure rank @-} 

   not 

   {-@ measure rank :: Heap a -> Int @-}

   Writing the former _should_ return an error message, but it doesn't, 

   which is something we will fix!

Did you mean "the latter"? i.e. {-@ measure rank :: Heap a -> Int @-} should be an error?

I also noticed that when I removed the type signature, LH complained about `min` being unbound (before I added the inlined version), but not while the type signature was there.

I'm trying to figure out where I got the idea that measures needed signature... It must have been from a misreading of chapter 4 of the tutorial, where an example .spec file is given with a measure which has a signature; the first occurrence of {-@ measure ... @-} isn't until chapter 6, and I just didn't notice that it lacked a signature.

 

2. When using Boolean measures, you need not write `Prop` i.e. instead of

< {-@ type LHeap a = {v:Heap a | Prop (isLeftist v)} @-}

< {-@ type OLHeap a X = {v:OHeap a X | Prop (isLeftist v)} @-}

   just write:

    

> {-@ type LHeap a = {v:Heap a | (isLeftist v)} @-}

> {-@ type OLHeap a X = {v:OHeap a X | (isLeftist v)} @-}

   Writing `Prop` _should_ return a nice error message but 

   unfortunately it doesn't which is clearly a bug in LH 

   that we should fix!

How is that different from TRUE and FALSE in chapter two of the tutorial?

 

3. You cannot use arbitrary Haskell code in measures, e.g. 

   `min` in the definition of rank; they must be terms that 

   can be "lifted" into the refinement logic (i.e. belong in 

   the logic.) Thus, I have defined a `min` and used it here 

   instead. 

> {-@ inline min @-}

> min :: Int -> Int -> Int

> min x y = if x < y then x else y

   You can then use such functions via via the {-@ inline min @-} 

   pragma. (As described also in the AVL chapter.)

 

The AVL chapter uses the inline pragma, but it's explanation is a single footnote with a FIXME, so I wasn't quite sure when it was necessary (the fact that LH didn't object while I had the type signature in place didn't help).

I'm also a little fuzzy as to why `min` needs to be inlined; it makes sense for functions that aren't defined in the Haskell Prelude, but shouldn't the GHC/Classes.spec file have enough annotation that a user can just use `min`?

4. I think you missed a "1 +" in the rank for leaf (otherwise the 

   rank is always 0), so I did that:

<   Branch _ l r -> min (rank l) (rank r)

---

>   Branch _ l r -> 1 + min (rank l) (rank r)

​No​w turning to your questions:

 

Is it possible to avoid record syntax when defining refined data types?
Is it ossible to avoid data refinement altogether, relying on smart constructors?

​​

​5. Yes, in gene​val you need not have such constructors, but in 

   your specific case, where the types of one field *depend on* another 

   (here, l and r depend on elt) you have to refine the data type.

   For example, suppose you just want an ordered pair:

   {-@ data OP = OP {x :: Int, y :: {v : Int | x < v} } @-}

   

   you could imagine a smart constructor:

   op ::x:Int -> {v: Int | x < v} -> OP 

   but this is not enough when you *destruct* the pair e.g. 

   via pattern matching:

   case p of 

     OP a b -> assert (a < b)

   In theory you could solve this problem using "smart destructors" 

   instead of pattern matching, but it could get a bit tedious.

I'm afraid I can't imagine what such a "smart destructor" would look like; is there an example you could point me at? I personally would have appreciated an alternative presented in chapter 5 of the tutorial, when refined data types are introduced. It would have made them feel less like magic.

   The other benefit of refining the data type is that you "declaratively" 

   specify the invariants in exactly one place without having to worry 

   about "how" the values were created (e.g. what if you found some way 

   to build a tree without using a smart constructor?)

True, but the flip side of that is decreased reuse (possibly not in ways that matter, in the end); that is, I can't use the same Haskell data type for binary trees (no refinement), binary search trees (just ordering), and both AVL red-black trees (two different kinds of balancing).

 

6.

`OHeap` and `LHeap` are two refinements on `Heap`; how could they be changed so that they compose?

​In this case, I would just eliminate LHeap and write OLHeap the way you have.

In principle we could imagine a mechanism like:

    {-@ type OLHeap a X = OHeap a X /\ LHeap a @-}

​but we ​haven't implemented such a thing yet.

Would I have been able to write something like
{-@ type OThing a X T = T {a | a < X} @-}
{-@ type LHeap a = {v:Heap a | isLeftist v} @-}
{-@ type OLHeap a X = OThing a X LHeap @-}

 

I'm guessing not quite in that syntax.

​7.

​

When is it appropriate to use a refinement which exposes some property (e.g. depth) in its type?

​Hmm,​ thats a tricky one -- in general, I'd say whenever you need to reason 

about that property. (But perhaps I've misunderstood the question?)

​​

Why doesn't LH figure out that a `Leaf` has rank 0?

​Now it does!

 

I want to figure this out mostly on my own, but I think that it's about time I stopped flailing and asked some questions, hopefully learning things in the process.

Points 1-3 *should* have been reported as spec/syntax errors, which 

would probably have saved you a great deal of effort. Apologies for that

and thanks for pointing these out!

Let me know if you need any clarifications!

Best,

Ranjit.

Thanks again for taking the time!

[Ranjit Jhala]

Hi Alex,

Did you mean "the latter"? i.e. {-@ measure rank :: Heap a -> Int @-} should be an error?

​Yes,​ sorry I meant the latter.

 

I also noticed that when I removed the type signature, LH complained about `min` being unbound (before I added the inlined version), but not while the type signature was there.

I'm trying to figure out where I got the idea that measures needed signature... It must have been from a misreading of chapter 4 of the tutorial, where an example .spec file is given with a measure which has a signature; the first occurrence of {-@ measure ... @-} isn't until chapter 6, and I just didn't notice that it lacked a signature.

​If you find it let me know​ (this could be a recent change, and either way, LH should report a proper error, so thanks for pointing out!)

 

2. When using Boolean measures, you need not write `Prop` i.e. instead of

 

How is that different from TRUE and FALSE in chapter two of the tutorial?

​Very good point!​ With "raw" boolean values, we need a "Prop" but with measures 

of type `T -> Bool` we _don't_ need prop. This is an inconsistency that we need to fix! Sorry about that! (Again at the very least an error message would have helped.)

 

3. You cannot use arbitrary Haskell code in measures, e.g. 

   `min` in the definition of rank; they must be terms that 

 

The AVL chapter uses the inline pragma, but it's explanation is a single footnote with a FIXME, so I wasn't quite sure when it was necessary (the fact that LH didn't object while I had the type signature in place didn't help).

​Yes, this is an unfortunate consequence of the fact that this feature (using Haskell code in specs) was added *after* much of the tutorial was written. 

We will update the tutorial to say more on this up front!

I'm also a little fuzzy as to why `min` needs to be inlined; it makes sense for functions that aren't defined in the Haskell Prelude, but shouldn't the GHC/Classes.spec file have enough annotation that a user can just use `min`?

​The "inline"​ is just a keyword (we should probably pick a different one than is used by GHC!) In this case it is needed precisely because it is not in the LH Prelude. (But you are right, we could add it there...)

I'm afraid I can't imagine what such a "smart destructor" would look like; is there an example you could point me at? I personally would have appreciated an alternative presented in chapter 5 of the tutorial, when refined data types are introduced. It would have made them feel less like magic.

Hmm. Ill have to think about that. But yes, its because such a "smart destructor"

is tricky that we put some invariants inside the datatype.

True, but the flip side of that is decreased reuse (possibly not in ways that matter, in the end); that is, I can't use the same Haskell data type for binary trees (no refinement), binary search trees (just ordering), and both AVL red-black trees (two different kinds of balancing).

​Indeed! For this reason you _can_ decouple a "specific" invariant from the datatype. For example, in your Heap there are two properties:

{-@ data Heap a = Leaf 

                | Branch { elt :: a

                         , l   :: OLHeap a elt

                         , r   :: OLHeap a elt } 

  @-}

{-@ type OHeap a X = Heap {v:a | v < X} @-}

{-@ type LHeap a = {v:Heap a | (isLeftist v)} @-}

{-@ type OLHeap a X = {v:OHeap a X | (isLeftist v)} @-}

a. isLeftist

b. order

You can first "pull out" the isLeftist by making it recursive:

{-@ measure isLeftist  @-}

isLeftist = \case

  Leaf -> True

  Branch _ l r -> (rank l >= rank r) && isLeftist l && isLeftist r

and then changing the type to:

 data Heap a = Leaf 

             | Branch { elt :: a

                      , l   :: OHeap a elt

                      , r   :: OHeap a elt } 

and then:

 type LHeap a = {v:Heap a | isLeftist v}

Now we are not "baking" isLeftist into the data 

constructor. Next, we can "extract" the "order" 

property using "abstract refinements" (unfortunately 

no chapter in the tutorial yet, but see this:

http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/categories/abstract-refinements/

https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/BST.hs#L6

You can write:

{-@ data Heap a <p :: a -> a -> Prop> 

      = Leaf 

      | Branch { elt :: a

               , l   :: Heap (a<p elt>)

               , r   :: Heap (a<p elt>) 

               } 

  @-}

which says that each "a" is related to "elt" by an abstract predicate "p".

You can now "instantiate p to recover order, e.g.

{-@ type OHeap a = Heap <{\elt v -> v < elt }> a @-}

and finally recover both properties a, b as:

   {-@ type OLHeap a = {v: OHeap a | isLeftist v} @-}

 

without either of those actually being hardcoded into the data constructor.

So if you want unbalanced trees, where the root is actually the SMALLEST element,

it is just:

   {-@ type MinHeap a = Heap <{\elt v -> v > elt}> a @-}

and just an arbitrary unordered, unbalanced tree is just:

   {-@ type THeap a = Heap <{\elt v -> true}> a @-}

(which is just abbreviated to `Heap a`).

Does that make sense?

Thanks!

Ranjit.

[Alex Rozenshteyn]

Yes! It makes a lot of sense. I've been staying away from abstract refinements for now, but they don't look too complicated.

A few more questions I've come across:

• Where exactly are refined types permitted (I'm assuming that {v : SomeType | somePredicate v} should be called a "refined type"; if a different naming scheme is preferred, let me know)
  In particular, why is this rejected (parse error on "=")?
  
  data Q = Q Int
  {-@ data Q = Q {v:Nat | true} @-}
  
  But this is accepted:
  
  data Q = Q Int
  {-@ data Q = Q Nat @-}
• Is there some rule of thumb when to use "measure" as opposed to "inline"?
I think I may have run into something that I don't fully understand in that vein:
  
  {-@ inline refine @-}
  refine (Left x) = x < 0
  refine (Right x) = x > 0
  
  This is rejected because LH "cannot promote" the function, but if I use "measure", I won't be able to access the resulting refinement, will I (since it will be treated as an uninterpreted function symbol)?
• I'd like to understand the trick mentioned here in more detail, since it seems to be related to this "smart destructor" business; is there somewhere I can read about it?
  In that vein, this shouldn't pass, right?
  
  data Bar = Bar
  {-@ Bar :: {v:Bar | unboundSymbol v } @-}
  
  It seems that checking is deferred until use.
• Earlier in the thread, it's mentioned that LH can't prove something like the below (and needs an assume on the second refinement)
  
  newtype Foo = Foo {getFoo :: Either Int Int}
  {-@ Foo :: {v:Either Int Int | refine v} -> {v:Foo | refine (getFoo v)} @-}
  {-@ getFoo :: Foo -> {v:Either Int Int | refine v} @-}
  
  Why is that? Is it just an engineering task that's low priority? Or is the reason more fundamental?
• Will this work as expected?
  
  newtype Q = Q {q :: Int}
  {-@ data Q = Q {q :: {v:Nat | true}} @-}
  

In my heap code, as I understand it, LH is currently complaining about the `Branch` call in `merge` because it can't prove that `merged` is smaller than `x1`, and this is because the refinement of `merge` does not provide any connection between the output and the inputs; is this correct? One idea I had was to change the refinement type to {-@ merge :: OHeap t x -> OHeap t y -> OHeap t (min x y) @-}, which led to an interesting error message (in emacs):

Suspicious state from syntax checker haskell-stack-liquid: Checker haskell-stack-liquid returned non-zero exit code 1, but no errors from output: LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

liquid:
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
Unexpected expression parameter: min x y in /home/alex/Documents/Haskell/LiquidHaskellTest/src/flycheck_Heap.hs:62:40: Error: Malformed Type Alias Application
Type alias: OHeap
Defined at: /home/alex/Documents/Haskell/LiquidHaskellTest/src/flycheck_Heap.hs:21:10
Expects 2 arguments, but is given 2
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************


Checker definition probably flawed.

I tried to find some way to relate the output to the inputs, leading me to try to define this:

{-@ measure smaller @-}
smaller Leaf _ = True
smaller _ Leaf = False
smaller (Branch x1 _ _) (Branch x2 _ _) = x1 <= x2

which gives a "cannot be promoted" error; changing "measure" to "inline" doesn't help.

I don't think I understand why neither works, and I don't know how I should relate the output to the input. Would you give me a hint?

Thanks again for taking the time to answer my questions!