measure vs. reflect

[nikivazou]

How about we merge these two into just reflect foo and then LH can decide if foo is actually a measure?

From user perspective it will be convenient because the user does not need to know the difference. But, if the user does not know the difference then how do they know that "reasoning about measures happen automatically, while for reflected functions the user needs to do the unfoldings".

Thoughts?

[ranjitjhala]

This would be great! @gridaphobe has been asking for this forever.

[Also, include inline] but somehow, I think, it will be tricky...

On Wed, Apr 4, 2018 at 10:59 AM, Niki Vazou notifications@github.com wrote:

How about we merge these two into just reflect foo and then LH can decide if foo is actually a measure?

From user perspective it will be convenient because the user does not need to know the difference. But, if the user does not know the difference then how do they know that "reasoning about measures happen automatically, while for reflected functions the user needs to do the unfoldings".

Thoughts?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1285, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOLesBkNn1JVrV72A0htKzehsK2Knks5tlQnngaJpZM4THPUV .

[ranjitjhala]

Perhaps we can start by trying to make precise exactly the rules/conditions under which a function will be treated as (1) inline (2) measure (3) reflect ?

On Wed, Apr 4, 2018 at 11:13 AM, Ranjit Jhala jhala@cs.ucsd.edu wrote:

This would be great! @gridaphobe has been asking for this forever.

[Also, include inline] but somehow, I think, it will be tricky...

On Wed, Apr 4, 2018 at 10:59 AM, Niki Vazou notifications@github.com wrote:

How about we merge these two into just reflect foo and then LH can decide if foo is actually a measure?

From user perspective it will be convenient because the user does not need to know the difference. But, if the user does not know the difference then how do they know that "reasoning about measures happen automatically, while for reflected functions the user needs to do the unfoldings".

Thoughts?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1285, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOLesBkNn1JVrV72A0htKzehsK2Knks5tlQnngaJpZM4THPUV .

[nikivazou]

We have the rules, they are syntactic. This is not the problem.

My concern is, they how do we explain to the user that

reasoning (unfolding) about length happens automatically but about reverse the user needs to do the unfolding.

[ranjitjhala]

I don't know the rules, can we enumerate them precisely over here?

On Wed, Apr 4, 2018 at 11:16 AM, Niki Vazou notifications@github.com wrote:

We have the rules, they are syntactic. This is not the problem.

My concern is, they how do we explain to the user that

reasoning (unfolding) about length happens automatically but about reverse the user needs to do the unfolding.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1285#issuecomment-378695895, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOE1BnpVZB1F4417Vg7WQN4iFZgkVks5tlQ4LgaJpZM4THPUV .

[ranjitjhala]

Btw, to me the "user explanation" is this:

• inlines [non-recursive]
• measures [recursive-but-over-single-ADT]

are always unfolded, but,

• reflects [recursive] are never unfolded (except with PLE)

?

[atondwal]

Are we going to keep {-@ measure f @-} to define uninterpreted functions? It's quite useful.