Stream: wg-traits

Topic: the meaning of not


nikomatsakis (Dec 24 2019 at 11:32, on Zulip):

@Jack Huey Let's discuss the meaning of not a bit. I've been pondering it indeed.

nikomatsakis (Dec 24 2019 at 11:33, on Zulip):

Aaron's blog post describes "modal logic":

Modal logic makes truth relative to a possible world, rather than being an absolute thing. In one world, the sky is blue; in another world, it’s red. That’s the story for “facts”. But the basic rules of logic apply no matter what world you’re talking about: 1+1 = 2 in every possible world.

nikomatsakis (Dec 24 2019 at 11:33, on Zulip):

In Rust terms, we have to ask ourselves in what "world" we are trying to prove things

nikomatsakis (Dec 24 2019 at 11:34, on Zulip):

In @Sunjay Varma's work on coherence, we introduced this idea of a "compatible" mode. It means basically "we're trying to prove whether this impl exists in any semver-compatible world". That turns out to be a much broader set of impls, of course, than the ones we can see. It includes downstream crates, for example.

nikomatsakis (Dec 24 2019 at 11:35, on Zulip):

We implement this in chalk via a special predicate (Compatible) that can ordinarily not be proven, but which can be inserted into the environment. So Compatible => G means "is G true for all semver-compatible worlds?"

nikomatsakis (Dec 24 2019 at 11:35, on Zulip):

Just proving G means "is G true in this world -- i.e., for the impls and assumptions we can see right now?"

nikomatsakis (Dec 24 2019 at 11:36, on Zulip):

Another good read is the "Negation as Failure" paper, though I can't find a free PDF of it (I think I bought it at some point)

nikomatsakis (Dec 24 2019 at 11:37, on Zulip):

Negation as failure means the idea of saying "if I can't find prove G, it must be false". This is the traditional Prolog form. It makes some sense because Prolog is complete -- i.e., if it can't prove something, there is no solution.

nikomatsakis (Dec 24 2019 at 11:39, on Zulip):

But chalk is a superset of prolog and indeed the interaction of negation-as-failure with forall feels kind of complex. For example, should forall<T> { not { T: Iterator } } be true? Seems like probably not -- we don't know that T: Iterator, but we also don't know that it doesn't.

But what about if there are no Iterator impls in the program at all?

nikomatsakis (Dec 24 2019 at 11:43, on Zulip):

I came up against this yeah because I've been pondering this test-case:

forall<T> {
    not { <T as Foo<i32>>::Bar = <T as Foo<u32>>::Bar }
}

right now this is provable, at least sometimes, which sort of seems wrong. But then, what if there are no impls of Foo at all? Or no impls where Bar is defined to be the same type?

nikomatsakis (Dec 24 2019 at 11:44, on Zulip):

And indeed I think if there is an impl where Bar overlaps, then we get it right.

nikomatsakis (Dec 24 2019 at 11:45, on Zulip):

So it seems like the question is, to some extent, in what "world" are we checking negation (or perhaps, checking generic functions). This then circles back a bit to "for what purpose are we using negation"?

nikomatsakis (Dec 24 2019 at 11:47, on Zulip):

(One problem we had early on was that forall<T, U> { not { T = U } } would be provable, which seems clearly wrong; we resolved this by the current method of replacing placeholders with inference variablles when negating, though we considered other approaches. I just had a branch where I was exploring the problem above and I was considering whether to revive some of the older approaches when I realized that it wasn't entirely clear to me what behavior I felt was "right")

nikomatsakis (Dec 24 2019 at 11:53, on Zulip):

I think the main uses we have for negation are:

Jack Huey (Dec 24 2019 at 17:01, on Zulip):

not has always thrown me for a loop

Jack Huey (Dec 24 2019 at 17:02, on Zulip):

especially when in the context of exists or forall

Jack Huey (Dec 24 2019 at 17:03, on Zulip):

This sort of train of thought reminds me of when you said something to the extent of "I would rather make all traits non-enumerable"

Jack Huey (Dec 24 2019 at 17:04, on Zulip):

In that, when we solve these goals, what are we considering? The current known world? Or the set of possible worlds?

Jack Huey (Dec 24 2019 at 17:05, on Zulip):

And, sure, Rust has a set of coherence rules that limit that set of possible worlds, but in the end, I think it would/should ultimately be the difference between a "suggestion" and a "unique answer"

Jack Huey (Dec 24 2019 at 17:05, on Zulip):

maybe?

Jack Huey (Dec 24 2019 at 17:06, on Zulip):

Anyways, bringing it back to not

Jack Huey (Dec 24 2019 at 17:08, on Zulip):

I might take a look at coherence rules a bit closer (more specifically, how they're written in Chalk) and Compatible

Jack Huey (Dec 24 2019 at 19:54, on Zulip):

But chalk is a superset of prolog and indeed the interaction of negation-as-failure with forall feels kind of complex. For example, should forall<T> { not { T: Iterator } } be true? Seems like probably not -- we don't know that T: Iterator, but we also don't know that it doesn't.

But what about if there are no Iterator impls in the program at all?

So, I've been thinking about this. Why aren't are Chalk goals and program "complete"? I would say that is the point of the Compatible predicate right? That we either enumerate all possible impls or we say "something impls Iterator, but we can't prove it"?

Charles Lew (Dec 25 2019 at 01:29, on Zulip):

I want to share my very naive view on this. (Ignore me if my theory goes too wrong). So we can see a Rust program as a series of "claim"s, the programmer thought they're facts, but maybe they're not, and it's the compiler's duty to find out. Two "claim"s may conflict with each other, and human may come up with a negative example for one "claim".

So in my mindset every query to chalk should be the form:

not (Contradiction) && { ConcreteType($TypeLevelExpr, ?Result) }

where Contradiction is a special predicate that when proved, it means that the "repo" itself is not in a consistent state, e.g. there're two claims in it that each conflicts with the other.

and about the "not" construct, i think it's composed with two smaller goals:
not A :- CannotProveUnderAssumption(True, A) && CannotProveUnderAssumption(A, Contradiction)

where CannotProveUnderAssumption is a special predicate that represents the capability of Chalk itself.

Last update: Jan 21 2020 at 09:05UTC