"defined" vs "measure" - Githubissues

alanz commented 7 years ago

It seems that defined is parsed as a synonym for measure.

Is this intentional? Are both needed?

ranjitjhala commented 7 years ago

Didn't even know this existed -- @nikivazou what is defined about? Can we remove it?

ranjitjhala commented 7 years ago

Lets just remove it. The less stuff there is in the parser the better!

alanz commented 7 years ago

Likewise expression seems to be a lesser-used alias for predicate.

ranjitjhala commented 7 years ago

Wow, so much can go!

On Tue, Mar 21, 2017 at 7:49 AM Alan Zimmerman notifications@github.com wrote:

Likewise expression seems to be a lesser-used alias for predicate.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/972#issuecomment-288102466, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOHC6BX48-OjFxx_DwIRz41gClruPks5rn-OEgaJpZM4Mj2Ng .

ranjitjhala commented 7 years ago

Thanks!!

On Tue, Mar 21, 2017 at 7:50 AM Ranjit Jhala jhala@cs.ucsd.edu wrote:

Wow, so much can go!

On Tue, Mar 21, 2017 at 7:49 AM Alan Zimmerman notifications@github.com wrote:

Likewise expression seems to be a lesser-used alias for predicate.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/972#issuecomment-288102466, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOHC6BX48-OjFxx_DwIRz41gClruPks5rn-OEgaJpZM4Mj2Ng .

nikivazou commented 7 years ago

Define lets you define how Haskell functions behave into logic. For example look at this fine of built in defines

https://github.com/ucsd-progsys/liquidhaskell/blob/develop/include/CoreToLogic.lg

We need a way to encode this feature, but if you find a better keyword feel free to change it!

ranjitjhala commented 7 years ago

That particular use-case is probably one that will eventually be deprecated, but I guess we should hold on to it for now...

~~I suspect we could even achieve the same result using a #define CPP macro.~~

alanz commented 7 years ago

Just for clarity, there is define, measure and defined.

It is only the latter 2 that are parsed the same.

nikivazou commented 7 years ago

Oh I see.

You can delete the defined then. I initiated this defined because the measure command is SUPER overloaded. Specifically, it has 3 behaviors

defining measures, eg

{-@ measure len1 :: [a] -> Int 
len1 Nil = 0 
len1 (C x xs) = 1 + len1 xs 
@-}

defining UNINTERPRETED functions, eg
```
{-@ measure len2 :: [a] -> Int  @-}
```

lifting haskell functions into logic, eg

{-@ meausure len3 @-}
len3 N = 0 
len3 (C _ xs) = 1 + len3 xs

I dislike the usage of the keyword measure for the second case, because len2 is just not a measure., but just a (defined) unintepreted function.

alanz commented 7 years ago

If the distinction between the first and second is important, then there should be some kind of warning if they are used in the wrong sense.

Otherwise they are just synonyms which can cause confusion for new users (such as me).

ranjitjhala commented 7 years ago

Unlike @nikivazou, I don't think the difference between 1, 2 is so great.

On Tue, Mar 21, 2017 at 10:52 AM, Alan Zimmerman notifications@github.com wrote:

If the distinction between the first and second is important, then there should be some kind of warning if they are used in the wrong sense.

Otherwise they are just synonyms which can cause confusion for new users (such as me).

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

nikivazou commented 7 years ago

@ranjitjhala in the 2nd case we are not defining a measure

gridaphobe commented 7 years ago

I agree with @ranjitjhala, but perhaps we should let @alanz be the judge, as a new user :)

(1) and (2) both define new logical functions that can be used inside refinements. The difference is that (1) also provides an implementation that the logic can reason about, whereas (2) leaves the function as a black box so to speak. All we know in (2) is that the functions obey the axiom of congruence, i.e.

x == y ==> f x == f y

Obviously (1) is more powerful, but (2) is useful when you can't provide an implementation that the logic can reason about (there are many cases where this might appear since our logic is quite limited).

The important similarity between (1) and (2) to me is that once you've defined the functions, you use them in exactly the same way inside refinements. Thus I think they warrant the same name.

What do you think @alanz ?

alanz commented 7 years ago

I think the distinction is useful for someone like me, but only if I am helped with it.

So if I use measure and there is no underlying haskell function that can be reasoned about, then it should give a warning.

Likewise, if there IS a function for defined, that should warn.

nikivazou commented 7 years ago

That is a good point!

Now, the the following two codes have unexpectedly totally different semantics, without warning

a. real measure

{-@ meausure len3 @-}
len3 N = 0 
len3 (C _ xs) = 1 + len3 xs

b. uninterpreted function definition.

{-@ meausure len3 :: [a] -> Int @-}
len3 N = 0 
len3 (C _ xs) = 1 + len3 xs

My objections are two

I think the user expects the above two to behave the same; and
the b. defines an uninterpreted function that does not have to be restricted by the measure definition as defined in "measures are unary functions whose (1) domain is the data type, and (2) body is a single case-expression over the datatype \cite{Refinement Types for Haskell}"

alanz commented 7 years ago

So a warning if the measure conditions do not hold would be a good thing. And use defined for the other case.

ranjitjhala commented 7 years ago

@nikivazou -- I don't understand your example or the second objection.

The only difference between the two is the type signature? Other than that they should behave the same. Why don't they?

I'm willing to change the other thing to abstract measure (unless that is taken already)

On Tue, Mar 21, 2017 at 12:04 PM, Alan Zimmerman notifications@github.com wrote:

So a warning if the measure conditions do not hold would be a good thing. And use defined for the other case.

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

nikivazou commented 7 years ago

@ranjitjhala they definitely do not behave the same. b. defines an uninterpreted function that is unrelated with the Haskell len3 function.

To explain my second objection: How do you define a measure? (I do not know what is an abstract measure but in our bibliography we have formally defined what a measure is)

gridaphobe commented 7 years ago

When I say "abstract measure" I mean a plain old uninterpreted function.

My point is that the precise definition of "measure" as an inductive predicate that we use to strengthen the types of data constructors is not something that I want to worry about as a user.

What I want instead is a single concept of "logical function" that I can use in refinements. How does one produce such a thing? We currently have three ways that I'm aware of:

Write a measure, either by hand or lifted from an inductive Haskell function.
Write a predicate alias, or use the inline annotation to lift a non-inductive Haskell function.
Write an "abstract" measure, i.e. no implementation, just an uninterpreted function.

These three methods have different consequences under the hood, but the user-facing effect is the same: I get a new function to use in my refinement types. I'm willing to concede that there may be a user-visible difference between 1/2 and 3, in that replacing a logical function defined via 1 or 2 with one defined via 3 will cause programs to stop type-checking. But I think from a user's perspective, 1 and 2 are the same thing and 3 is at most an "abstract" version of whatever 1 and 2 are.

ranjitjhala commented 7 years ago

@nikivazou -- why do these two behave differently? Is it just the type sig [a] -> Int ? If so, that is a terrible bug that should be fixed.


{-@ measure lenA @-}
lenA N = 0
lenA (C _ xs) = 1 + lenA xs

{-@ measure lend :: [a] -> Int @-}

lenB N = 0
lenB (C _ xs) = 1 + lenB xs

In general, now that we have "lifting" we should assume (i.e. move towards a future where) ALL measures have matching haskell definitions (i.e. are lifted) and the "abstract" ones maybe get a definition like

{-@ measure foo @-}
foo :: Thing -> Int
foo = uninterpreted

where uninterpreted is just an alias for undefined or error or similar.

On Tue, Mar 21, 2017 at 1:51 PM, Eric Seidel notifications@github.com wrote:

When I say "abstract measure" I mean a plain old uninterpreted function.

My point is that the precise definition of "measure" as an inductive predicate that we use to strengthen the types of data constructors is not something that I want to worry about as a user.

What I want instead is a single concept of "logical function" that I can use in refinements. How does one produce such a thing? We currently have three ways that I'm aware of:

Write a measure, either by hand or lifted from an inductive Haskell function.

Write a predicate alias, or use the inline annotation to lift a non-inductive Haskell function.

Write an "abstract" measure, i.e. no implementation, just an uninterpreted function.

These three methods have different consequences under the hood, but the user-facing effect is the same: I get a new function to use in my refinement types. I'm willing to concede that there may be a user-visible difference between 1/2 and 3, in that replacing a logical function defined via 1 or 2 with one defined via 3 will cause programs to stop type-checking. But I think from a user's perspective, 1 and 2 are the same thing and 3 is at most an "abstract" version of whatever 1 and 2 are.

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

nikivazou commented 7 years ago

I agree that all uninterpreted functions should map to a corresponding Haskell function (which is not the case right now).

I disagree that calling the listing into logic measure thought. I suggest calling it reflect foo. Then if foo is actually a measure (ie defined on 1 ADT argument) we will treat it as a measure, if foo is not-recursive we can inline it, otherwise reflect the implementation of foo in the result type of the Haskell foo.

ranjitjhala commented 7 years ago

Sure, that's reasonable.

On Tue, Mar 21, 2017 at 6:31 PM Niki Vazou notifications@github.com wrote:

I agree that all uninterpreted functions should map to a corresponding Haskell function (which is not the case right now).

I disagree that calling the listing into logic measure thought. I suggest calling it reflect foo. Then if foo is actually a measure (ie defined on 1 ADT argument) we will treat it as a measure, if foo is not-recursive we can inline it, otherwise reflect the implementation of foo in the result type of the Haskell foo.

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/972#issuecomment-288271373, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOI-7fhCWFu9xmxj1-VoK_YByPaTgks5roHnHgaJpZM4Mj2Ng .

gridaphobe commented 7 years ago

Fine by me, I don't care too much what we call the user-facing thing as long as there's a single name for all three of the techniques I listed :)

alanz commented 7 years ago

Coming back to this, is there an agreed action to take for this issue?

From my perspective, this means clearing up

Just for clarity, there is define, measure and defined.

It is only the latter 2 that are parsed the same.

by removing the keyword defined.

nikivazou commented 7 years ago

We do not seem to agree on a major edit, so for now you can just remove the defined.

ucsd-progsys / liquidhaskell

"defined" vs "measure" #972