Stream: wg-traits

Topic: Question


gnzlbg (Dec 05 2019 at 12:54, on Zulip):

Is it possible to express the following trait system query under chalk?

compatible(T, U) is "satisfied" if there exists a type sequence [U_0, U_1, ..., U_N] such that for i in range [1, N) the query compatible(U_{i}, U_{i+1}) is satisfied and such that compatible(U_N, U)is also satisfied

?

gnzlbg (Dec 05 2019 at 17:18, on Zulip):

Context: https://gist.github.com/gnzlbg/4ee5a49cc3053d8d20fddb04bc546000#reference-level-explanation (in particular, the last paragraph of that section).

nikomatsakis (Dec 06 2019 at 23:56, on Zulip):

@gnzlbg ..maybe?

nikomatsakis (Dec 06 2019 at 23:56, on Zulip):

/me reads context

nikomatsakis (Dec 06 2019 at 23:56, on Zulip):

Yeah I'm going with "maybe" :)

nikomatsakis (Dec 06 2019 at 23:57, on Zulip):

it certainly seems expressible but also seems fairly dissimilar from other things in Rust

nikomatsakis (Dec 06 2019 at 23:57, on Zulip):

that said, chalk can certainly express things like the "at least one" solution (via exists<T> { ... } goals). I'm not sure about the open-ended nature of the length of the sequence though.

gnzlbg (Dec 11 2019 at 16:37, on Zulip):

thanks, I'll try to get chalk running and see if I can find a way to express the query

lqd (Dec 11 2019 at 17:00, on Zulip):

(this explanation might be clearer expressed as the compatible transitive closure in datalog: compatible(T, U) :- compatible(T, X), compatible(X, U).)

gnzlbg (Dec 13 2019 at 13:42, on Zulip):

@rkruppe ^^^

Last update: Jun 07 2020 at 10:15UTC