Introduce assumptions for PLE

[facundominguez]

Currently, the only way to feed equations to PLE is by reflecting functions.

This is a constraint that prevents entering equations from functions in dependencies unless these functions are reflected, which in turn requires to fork the dependencies to introduce the Liquid Haskell annotations that would have the functions reflected.

I would like a mechanism for assumptions to be introduced to PLE without changing dependencies, and I see three ways forward.

Impostor reflection

Let's say we would like to reflect Prelude.filter from base. Define a function

{-@ reflect myfilter @-}
myfilter p [] = []
myfilter p (x:xs) = if p x then x : myfilter p xs else myfilter p xs

Then tell somehow to LH to use the equations of myfilter every time it finds a call to Prelude.filter.

REST route

Introduce the assumed equations via REST rewrite rules. In this case we need to consider whether we can optimize REST so it is a practical substitute for regular PLE equations.

Type-scanning

Suppose we give the following specification to filter.

assume filter
  :: p:(a -> Bool)
  -> xs:[a]
  -> { v:[a] | v = if null xs then [] else if p (head xs) then head xs : filter p (tail xs) else filter p (tail xs) }

The type reveals how to unfold filter, but PLE is not looking for equations in the predicates of refinement types.
I'm guessing it wouldn't be difficult to have Liquid Haskell or Liquid Fixpoint to produce equations for PLE from this.

Moreover, it can be generalized one day, so PLE can do a bit more than unfolding eventually. e.g. given a definition like

gcd :: {x:Int | x>=0 } -> {y:Int | y>=0} -> { v:Int | mod x v = 0 && mod y v = 0 }
gcd x y = if x < y then gcd (y - x) x else if x > y then gcd y x else x

If PLE encounters gcd a b in a formula, it could add to the environment the fact that mod a (gcd a b) = 0 && mod b (gcd a b) = 0 before continuing with the unfolding of other terms.

---

I like impostor reflection the most because it saves the most typing. First, it gives the power of Haskell syntax to express the equations. And second, if filter depended on other functions, we could rely on LH to introduce the necessary uninterpreted symbols automatically.

type-scanning is interesting because it can generalize a bit what PLE does, but it does not offer as good an experience as impostor reflection for this use case.

REST route has the advantage to not require any new features. But we still need to mature the implementation, and similarly to type-scanning it offers not as good experience as impostor reflection.

[ranjitjhala]

I like this very much - I suggest using “type scanning” as a start , and later we can generalize it using “impostor”? Ie the implementation of impostor could essentially be type scanning + substituting names in the reflected refinement ?

…

On Wed, Dec 21, 2022 at 10:19 AM Facundo Domínguez ***@***.***> wrote: Currently, the only way to feed equations to PLE is by reflecting functions. This is a constraint that prevents entering equations from functions in dependencies unless these functions are reflected, which in turn requires to fork the dependencies to introduce the Liquid Haskell annotations that would have the functions reflected. I would like a mechanism for assumptions to be introduced to PLE without changing dependencies, and I see three ways forward. Impostor reflection Let's say we would like to reflect Prelude.filter from base. Define a function {-@ reflect myfilter @-} myfilter p [] = [] myfilter p (x:xs) = if p x then x : myfilter p xs else myfilter p xs Then tell somehow to LH to use the equations of myfilter every time it finds a call to Prelude.filter. Optimize REST Introduce the assumed equations via REST rewrite rules. In this case we need to consider whether we can optimize REST so it is a practical substitute for regular PLE equations. type-scanning for PLE Suppose we give the following specification to filter. assume filter :: p:(a -> Bool) -> xs:[a] -> { v:[a] | v = if null xs then [] else if p (head xs) then head xs : filter p (tail xs) else filter p (tail xs) } The type reveals how to unfold filter, but PLE is not looking for equations in the predicates of refinement types. I'm guessing it wouldn't be difficult to have Liquid Haskell or Liquid Fixpoint to produce equations for PLE from this. Moreover, it can be generalized one day, so PLE can do a bit more than unfolding eventually. e.g. given a definition like gcd :: {x:Int | x>=0 } -> {y:Int | y>=0} -> { v:Int | mod x v = 0 && mod y v = 0 } gcd x y = if x < y then gcd (y - x) x else if x > y then gcd y x else x If PLE encounters gcd a b in a formula, it could add to the environment the fact that mod a (gcd a b) = 0 && mod a (gcd a b) = 0 before continuing with the unfolding of other terms. ------------------------------ I like the *impostor reflection* the most because it saves the most typing. It gives you the power of Haskell syntax to express the function. Also, if filter depended on other functions, we could depend on LH to introduce the necessary uninterpreted symbols automatically. type-scanning is interesting because it can generalize a bit what PLE does, but it is not as good as *impostor reflection* for this use case. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2126__;!!Mih3wA!EzS0TQrJhFrUVAT_iCkjuYvqSZrUlzVFBLhvQoceNuESF-SUvUNPAmgFxxMYHNUn4bxaOShXMMTaJdjBfC9lfe9a$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OFWVRIZJNFNIFN3SNLWONC2PANCNFSM6AAAAAATF45R7Y__;!!Mih3wA!EzS0TQrJhFrUVAT_iCkjuYvqSZrUlzVFBLhvQoceNuESF-SUvUNPAmgFxxMYHNUn4bxaOShXMMTaJdjBfOB2TQ2f$> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[facundominguez]

impostor could essentially be type scanning + substituting names in the reflected refinement

I just realized that type scanning does indeed subsume impostor. It goes like this: define myfilter as above, reflect it as normal, then use type scanning on:

assume filter :: p:(a -> Bool) -> xs:[a] -> { v:[a] | v = myfilter p xs }

which should cause PLE to add equations filter a b = myfilter a b whenever a call to filter a b is encountered.

[ranjitjhala]

Ha! Very nice!!

On Wed, Mar 22, 2023 at 3:48 AM Facundo Domínguez ***@***.***> wrote: impostor could essentially be type scanning + substituting names in the reflected refinement I just realized that type scanning does indeed subsume impostor. It goes like this: define myfilter as above, reflect it as normal, then use type scanning on: assume filter :: p:(a -> Bool) -> xs:[a] -> { v:[a] | v = myfilter p xs } which should cause PLE to add equations filter a b = myfilter a b whenever a call to filter a b is encountered. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2126*issuecomment-1479322963__;Iw!!Mih3wA!GGWtyia32wgPreZVpexYFrwUQymPGl7QOXKxMpR1AAQFd3kYpQInzzpNY96QRD4x3ZT6sLxsK3jGgsAkPyAjR9y5$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OEK6UBIHAU3PNNC3KLW5LKITANCNFSM6AAAAAATF45R7Y__;!!Mih3wA!GGWtyia32wgPreZVpexYFrwUQymPGl7QOXKxMpR1AAQFd3kYpQInzzpNY96QRD4x3ZT6sLxsK3jGgsAkP-TrYi9l$> . You are receiving this because you commented.Message ID: ***@***.***>

-- - Ranjit.

[facundominguez]

Related to this, a safer alternative to assuming reflections would be to reflect the function definitions that are in interface files to use for inlining. This solution is only available for the smaller functions, but perhaps it is a very common case. Then we can reserve assuming reflections for the other functions.

[facundominguez]

The approach named here "impostor reflection" has been implemented in #2313.