Goal 0.1: insert + parallel map on a set

[rrnewton]

Parallel map on a set may not initially seem like it needs total Ord, but in LVish, it does. For instance, if you look at how the traverseSet function works, it must:

• divide and conquer the input set
• asynchronously insert into the output set

The assumption that inserts safely commute requires total Ord, as we've been discussing.

This goal is met when we have some kind of traverseSet operation that takes a proof of Ord totality (three proofs actually). This should in turn be based on an insert function that takes those same proofs.

[Note: for this prototype, because of problems with (1) type classes and (2) passing proofs in product types, we will pass proofs as separate function arguments.]

[rrnewton]

This should probably just be a branch of LVish with the fancier types. Please branch off of something that is passing unit tests.

[vikraman]

I'm wondering if turning on the LiquidHaskell --totality flag will be enough to ensure that compare :: a -> a -> Ordering is total, so we just need proofs of antisymmetry and transitivity.

[vikraman]

Ok, it's not enough, we still need the total order proof.

[rrnewton]

Could you post whatever counterexample convinced you?

As far as I can see, in a higher order case like this... I'm not sure how we can state that the totality check was applied to the function passed in. That is, can't I just put the function in another module, check it without --totality and then fool your function?

[nikivazou]

I too doubt that the totality check can be of any use to a polymorphic function compare :: a -> a -> Ordering. I cannot see how a polymorphic function can be partially defined, since you cannot do case analysis on its inputs.

[rrnewton]

I guess the idea was if you guarantee that all call sites for Set.insert are checked with liquid haskell, and that the code for the concrete (monorphic) compare functions are likewise checked.... then --totality would cover it?

I'm a bit confused about how we would assert totality in a refinement anyway. Wouldn't it be covered by whatever other refinements we have? I.e. any references to the compare operation in the refinements (e.g. antisymmetry/transitivity) mean it has been axiomatized and therefore is total?

[vikraman]

I was confusing the two notions of totality. For example, this is a total function, but it fails the totality requirement of a total order.

leqInt :: Int -> Int -> Bool
leqInt x y = False

So, instead of Ord a =>, we need to pass in:

   (leq : a -> a -> Bool) 
-> (x:a -> y:a -> { leq x y || leq y x })
-> (x:a -> y:a -> { leq x y && leq y x => x == y }) 
-> (x:a -> y:a -> z:a -> { leq x y && leq y z ==> leq x z })

[rrnewton]

I see... does that differ a bit with the a -> a -> Ordering signature? Wouldn't the latter mean that --totality is enough to force compare to meet the a <= b || b <= a requirement of the total order?

[rrnewton]

Oh, but I just realized that writing down that signature you pasted gets very very ugly using compare directly.

[rrnewton]

Here's an ugly and direct expansion to use compare:

   (cmpr : a -> a -> Ordering) 
-> (x:a -> y:a -> z:a -> { cmpr x y == LT && cmpr y z == LT ==> cmpr x z == LT})
-> (x:a -> y:a -> z:a -> { cmpr x y == LT && cmpr y z == EQ ==> cmpr x z == LT})
-> (x:a -> y:a -> z:a -> { cmpr x y == EQ && cmpr y z == LT ==> cmpr x z == LT})
-> (x:a -> y:a -> z:a -> { cmpr x y == EQ && cmpr y z == EQ ==> cmpr x z == EQ}) 
-> (x:a -> y:a -> { cmpr x y == LT ==> cmpr y x == GT })
-> (x:a -> y:a -> { cmpr x y == EQ ==> cmpr y x == EQ })

[nikivazou]

Well, you can use macros

type ComProp X Y Z = (x:a -> y:a -> z:a -> { cmpr x y == X && cmpr y z == Y ==> cmpr x z == Z})

type LTCom =  ComProp LT LT LT 

     (cmpr : a -> a -> Ordering) 
-> LTCom
-> (x:a -> y:a -> z:a -> { cmpr x y == LT && cmpr y z == EQ ==> cmpr x z == LT})
-> (x:a -> y:a -> z:a -> { cmpr x y == EQ && cmpr y z == LT ==> cmpr x z == LT})
-> (x:a -> y:a -> z:a -> { cmpr x y == EQ && cmpr y z == EQ ==> cmpr x z == EQ}) 
-> (x:a -> y:a -> { cmpr x y == LT ==> cmpr y x == GT })
-> (x:a -> y:a -> { cmpr x y == EQ ==> cmpr y x == EQ })

[rrnewton]

That's a macro at the type level; would it also be possible to just define leq as a utility function at the value level and then axiomatize?

-- Axiomatize and use as an abbreviation:
leq cmpr x y = cmpr x y == EQ || cmpr x y == LT 

insert :: x -> Set x ->  (c : a -> a -> Ordering) 
-> (x:a -> y:a -> { leq c x y || leq c y x })
-> (x:a -> y:a -> { leq c x y && leq c y x => x == y }) 
-> (x:a -> y:a -> z:a -> { leq c x y && leq c y z ==> leq c x z })
-> Par _ s ()

Anyway, I guess it comes down to whatever makes it easiest for the clients to do their proofs.

I think we should do a simple Set Int to kick off this 0.1 goal and make sure everything is hooked up and working. After that we were planning on checking off tuples and other simple examples.

[rrnewton]

By the way, just to document it:

The thing blocking us from putting these 3 proofs in a product type for convenience is this issue, I believe. @vikraman, have we confirmed that all available product types fail? I.e. a tuple of proofs doesn't work any better than a datatype of proofs?

[nikivazou]

It is possible @rrnewton! If you are an inline annotation {-@ inline leq @-}, leq will just be inlined in the logic

[rrnewton]

Ah, nice. I wasn't aware of that inline annotation.

(FYI, it turns out that I missed some cases, and totality on compare doesn't seem to help anything. Please ignore the compare-based spec above.)

Note that @vikraman's current approach actually gets around having a separate argument for each theorem. Instead he can create an abstract datatype for VerifiedOrd which does not store the proofs, and this works in the current Liquid Haskell.

This should support a smooth refactoring path to add the fields as proofs (when we can do refinements inside fields of a product type). That will be necessary for reuse when constructing proofs for compound values like pairs.

Actually, we can probably start mocking up a class-based version as well, again, not providing the proofs as methods, but rather a method that returns a VerifiedOrd value.