Allow refinements in the output type of measures

[gridaphobe]

Only base types are allowed to appear in the type of a measure, but this is less accurate than it could be, e.g. when dealing with measures that denote the size of a value.

measure len :: [a] -> Int
len []     = 0
len (x:xs) = 1 + len xs

Since the type only specifies that len returns an Int, we need to additionally define an invariant on Int.

invariant {v:[a] | (len v) >= 0}

This is a bit tedious when what we really want to write is just

measure len :: [a] -> Nat
len []     = 0
len (x:xs) = 1 + len xs

Perhaps there's a good reason to disallow refinements in the return type of a measure, but it isn't apparent to me.

[nikivazou]

I believe that the invariant is basically needed to get the qualifiers,
with the correct qualifiers liquidHaskell CAN infer that len v >=0 by lenis definition.

[ranjitjhala]

No it is not just for qualifiers.

The non negativity of Len can only be inferred for lists that are constructed from scratch.

Try to prove that haskell's 'drop' function returns a list with nonneg Len.
Now you will see you need that the INPUT also has non neg Len. It is to avoid writing such tedious things in the input that we need invariants.

At any rate @gridaphobe is right. It would be nice to put the fact right in the measure. Mind you we will still need the. Invariant mechanism for other things...

On Sep 25, 2013, at 8:15 AM, Niki Vazou [email protected] wrote:

I believe that the invariant is basically needed to get the qualifiers,
with the correct qualifiers liquidHaskell CAN infer that len v >=0 by lenis definition.

—
Reply to this email directly or view it on GitHub.

[ranjitjhala]

Btw, given @nikivazou's recent progress with promoting functions to measures, it would be nice to fix the above, thereby unifying measures and invariants.

So we should be able to write:

{-@ measure len @-}
{-@ len :: [a] -> Nat @-}
len :: [a] -> Int
len []     = 0
len (x:xs) = 1 + len xs

and from that, automatically derive

invariant {v: [a] | 0 <= len v}

How? Well, suppose you have a measure from some type T to a base type B with refinement p

meas :: T -> {v:B | p}

Then you have effectively specified (and verified)

invariant {v:T | p[(meas v) / v]}

[gridaphobe]

Yes, this sounds like a nice and simple approach.

I suppose in this approach, the measure-promotion would automatically refine the type of len-the-haskell-function to refer to len-the-measure? Or is @nikivazou already doing that?

Another question, should we allow promotion of functions with pre-conditions?

[nikivazou]

@ranjitjhala, this is a nice (and sound) suggestion. If we support this we can stop supporting invariants (that can lead to unsoundness).

@gridaphobe we should allows promotion of functions with preconditions, but we should translate the preconditions into the types of the data constructors. (I already relate the len-the-haskell-function with len-the-measure.)

Another suggestion: since we are already becoming a "lightweight" dependent type language, how about a flag "--autopromote" that automatically promotes to logic all the appropriate functions?

[ranjitjhala]

Hey, is this still open? I thought @nikivazou implemented it?

[nikivazou]

It is implemented for Haskell defined measures!

[gridaphobe]

@nikivazou what about for old-style measures? Not all measures can be defined in Haskell, e.g. uninterpreted measures.

[nikivazou]

Curently, there is no support for invariants over old style measures.

[ranjitjhala]

I think that's fine ... we would like to eventually deprecate old style measures anyway and just use the lifted style.

…

On Mon, Mar 20, 2017 at 7:48 AM Niki Vazou ***@***.***> wrote: Curently, there is no support for invariants over old style measures. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#126 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABkuOHdi0kmSYwmPV08njSHs-ylmeJ_Lks5rnpGegaJpZM4BCCvm> .

[gridaphobe]

But how would you define an uninterpreted measure in the lifted style? I suppose we could write a Haskell function that **actually** does the computation and change the annotation to `{-@ abstract measure @-}` or some such..

…

On Mon, Mar 20, 2017, at 09:09, Ranjit Jhala wrote: I think that's fine ... we would like to eventually deprecate old style measures anyway and just use the lifted style. On Mon, Mar 20, 2017 at 7:48 AM Niki Vazou ***@***.***> wrote: > Curently, there is no support for invariants over old style measures. > > — > You are receiving this because you were mentioned. > Reply to this email directly, view it on GitHub > <#126 (comment)>, > or mute the thread > <https://github.com/notifications/unsubscribe-auth/ABkuOHdi0kmSYwmPV08njSHs-ylmeJ_Lks5rnpGegaJpZM4BCCvm> > . > -- You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub: #126 (comment)

[nikivazou]

Agree, but abstract measure is just an uninterpreted function. Would need to clarify all these definitions.