ucsd-progsys/liquidhaskell

Allow refinements in the output type of measures

gridaphobe opened this issue · 12 comments

gridaphobe commented

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 commented

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 commented

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 notifications@github.com 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 commented

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 commented

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 commented

@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 commented

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

nikivazou commented

It is implemented for Haskell defined measures!

gridaphobe commented

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

nikivazou commented

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

ranjitjhala commented
gridaphobe commented
nikivazou commented

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