Logical Constraints

[nikivazou]

See tests/pos/Constraints.hs

Logical Constraints are of the form

{x1:a1 | r1} -> ... -> {xn:an | rn} -> {v:b | p} -> {v:b | q} (1)

and produce the formula

r1 /\ ... /\ rn => (p => q) (2)

Meaning if the constraint (1) appears in the type of a function f, then the formula (2) is

• assumed when the body of f is checked
• checked to hold when f is called

[ranjitjhala]

Can we discuss this in person tomorrow?

[nikivazou]

Sure!

[gridaphobe]

I won't be in today, but I'll leave a few thoughts.

1. I like this better than the existential, whose implementation I never understood :)
2. The constraints in your example are not well-scoped, as they refer to the output of the function. I would suggest moving them past the / that we use for termination exprs.
3. Please update the README and CHANGELOG before merging :)

[nikivazou]

Thanks @gridaphobe.
I guess I agree about the scope, and I will update the README, but before that to make constraints usable we need a better syntax. Now their meaning is not clear. But I want to test them before I write a constraint parser.

So, this is much more expressive than existential types.
(1) Note how in function composition we can give to function arguments preconditions!
(2) Also, with this we can verify stateful computations, see tests/pos/StateConstraints.hs

[gridaphobe]

Perhaps we should use => in constraints to mirror Haskell's constraint syntax?

[gridaphobe]

Nice, it also handles a proper state monad and bind. Now we just need some notion of intersection types so we can assign these types to the actual >>= and >> operators :)

[nikivazou]

What do you mean by "proper state monad and bind"?

I feel we can use dictionaries and do something smarter than intersection types, but it is not clear in my mind yet.

Anyways, we are getting closer:)

[gridaphobe]

The usual definition with

data ST s a = ST (s -> (a,s))

There's no real reason to expect LH to fail with the usual definition, but it gives me some extra peace of mind having tried it :)

Working directly with the dictionaries would be nice too, but it might require implementing the .lhi file stuff to support instances defined in other modules.

[ranjitjhala]

@nikivazou, hahahahahah! check out:

https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/filterAbs.hs

(and for sanity)

https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/neg/filterAbs.hs

On Mon, Dec 22, 2014 at 3:14 PM, Eric Seidel [email protected]
wrote:

The usual definition with

data ST s a = ST (s -> (a,s))

There's no real reason to expect LH to fail with the usual definition, but
it gives me some extra peace of mind having tried it :)

Working directly with the dictionaries would be nice too, but it might
require implementing the .lhi file stuff to support instances defined in
other modules.

Reply to this email directly or view it on GitHub
#289 (comment)
.

Ranjit.

[nikivazou]

This is cool! And quite clean!

These logical constraints are very powerful, it seems....

See this https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/StateConstraints.hs

[ranjitjhala]

Btw, the more I think about it the syntax needs to be changed.

This is because if you just write:

x:A -> y:B -> z:C -> D

then any user will think that it is equivalent to write:

x:A -> z:C -> y:B -> D

or for that matter,

z:C -> x:A -> y:B -> D

but in fact the semantics are totally different, because
really the last two things are special, and there is a
subtyping between them.

In particular the v in C and D refer to the same
value while the other v do not. Hence, I think we
should just use our regular constraint syntax

x:A, y:B |- C <: D

or find some other way to highlight that the last two
things are subtypes. This is pretty essential...

On Mon, Dec 22, 2014 at 4:57 PM, Niki Vazou [email protected]
wrote:

This is cool! And quite clean!

These logical constraints are very powerful, it seems....

See this
https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/StateConstraints.hs

Reply to this email directly or view it on GitHub
#289 (comment)
.

Ranjit.

[nikivazou]

@ranjitjhala I agree, but I suggest logical implication over subtyping, something like

y:a, x: {v:Bool | Prop v}, v:a |- v = y => p v

[ranjitjhala]

Why? In reality it is sub typing no?

On Dec 22, 2014, at 9:57 PM, Niki Vazou [email protected] wrote:

@ranjitjhala I agree, but I suggest logical implication over subtyping, something like

y:a, x: {v:Bool | Prop v}, v:a |- v = y => p v

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

[nikivazou]

It is subtyping. But sub typing is equivalent to logical implication.

I preferred implication because I call these constraints logical constraints, but if you see it as bounded quantification subtyping makes more sense. So, I also like the subtyping suggestion.