Allow reflected functions to use non-reflected functions

[facundominguez]

In stitch I was trying at some point to reflect the stitch type checker. However, the type checker uses Data.Map.lookup to find globally defined symbols.

Now, Liquid Haskell would insist that Data.Map.lookup needs to be reflected in order to reflect the type checker, when all it actually needs is a function in the logic to stand for it. I'm not interested in reflecting Data.Map.lookup since it is rather non-trivial and I'm happy to introduce assumptions about its behavior as necessary.

My workaround here implements a lookup function that doesn't terminate, but nonetheless can be reflected. And then I use rewrite rules to convince GHC to replace the non-terminating function with the actual lookup function from Data.Map.

This is a horrible hack as far as hacks go. Could we instead just tell LH to put in the logic an uninterpreted function

{-@ opaque-reflect Data.Map.lookup :: k -> Map k v -> Maybe v @-}

? Now when LH finds that the stitch type-checker uses Data.Map.lookup, it uses the uninterpreted function without further ado.

One other use case for a feature like this is in the length function of lists and bytestrings, and many other functions. liquid-base defines a measure

instance measure len :: forall a. [a] -> GHC.Types.Int
  len []     = 0
  len (y:ys) = 1 + len ys

Then length is defined as

{-@ length :: xs:[a] -> {v: GHC.Types.Int | v = len(xs)} @-}

This still doesn't allow to reflect functions that call to length despite of being a perfectly usable len function in the logic. Moreover, it requires the user to translate between the two names when crossing from code to specification.

Why not just name the measure the same as the function? And then let LH translate between the two when reflecting.

[ranjitjhala]

Yes this is an excellent idea - in fact opaque-measures can be useful just to write specs.

[facundominguez]

It struck me last weekend that perhaps opaque reflect should rather be the default. If a function is not available in the logic when reflecting some other function, have LH reflect it opaquely.

[nikivazou]

I agree, and actually do that a lot, manually. If I want to reflect foo that calls bar and cannot reflect bar, then the hack around it is:

foo = .... bar 

{-@ measure  bar :: a -> b @-}
{-@ assume bar :: x:a -> {v:b |  v = bar x } @-}
bar = unreflected 

[ranjitjhala]

The benefit of @facundo’s proposal is we could do this also for imported functions (eg in the prelude) without having to redefine them…

On Mon, Nov 15, 2021 at 7:36 AM Niki Vazou @.***> wrote:

I agree, and actually do that a lot, manually. If I want to reflect foo that calls bar and cannot reflect bar, then the hack around it is:

foo = .... bar

{-@ measure bar :: a -> b @-} {-@ assume bar :: x:a -> {v:b | v = bar x } @-} bar = unreflected

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1892-23issuecomment-2D969032284&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=MDIqtYn8FfygjMjuqo6Yz5ztFaTtDjudkABQDZsV4ATbo92pg8QtVS75Qp1AGEc8&s=t1WN5HYytwRgM9urO1_t8MlHm-bsUsoOFnLfBa-bk2o&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OCW5BX5RWYG3SZXUW3UMESJDANCNFSM5G7LRFRQ&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=MDIqtYn8FfygjMjuqo6Yz5ztFaTtDjudkABQDZsV4ATbo92pg8QtVS75Qp1AGEc8&s=3dA5eLzjltS3kOBxhDwWdHTHYMboouP6_n_JuBI2p0w&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=MDIqtYn8FfygjMjuqo6Yz5ztFaTtDjudkABQDZsV4ATbo92pg8QtVS75Qp1AGEc8&s=f7yBRsaojbHhGPGB1fQvAKhji7aZ2S6ikROIRV6O5u0&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=MDIqtYn8FfygjMjuqo6Yz5ztFaTtDjudkABQDZsV4ATbo92pg8QtVS75Qp1AGEc8&s=O9-MtRoOb5FSMa5Fz60syqXXYUsdwYyTxDIDtg76lVA&e=.