Stream: t-compiler/const-eval

Topic: using const-qualif for const-checking


RalfJ (Jun 03 2019 at 16:59, on Zulip):

@eddyb about my proposal to basically implement const-checking as "qualif everything and make sure nothing complains", to hopefully reduce duplication:

there are side-effects that don't produce a value

well but "qualif" also checks whether functions are const fn, even if they return (). so clearly they already are about side-effects, not just about the value produced.

eddyb (Jun 03 2019 at 17:00, on Zulip):

yes because it doesn't know it can synthesize a () out of thin air

eddyb (Jun 03 2019 at 17:00, on Zulip):

eventually we might do just that :P

eddyb (Jun 03 2019 at 17:00, on Zulip):

in fact, the old AST-based promoter had some special-cases for various "obviously ZST constructor"s

RalfJ (Jun 03 2019 at 17:00, on Zulip):

wait so &foo() should just become &() during implicit promotion??

eddyb (Jun 03 2019 at 17:01, on Zulip):

no

eddyb (Jun 03 2019 at 17:01, on Zulip):

the call isn't promoted away

eddyb (Jun 03 2019 at 17:01, on Zulip):

it'd become { foo(); &() }

RalfJ (Jun 03 2019 at 17:01, on Zulip):

but that's what I am saying -- promotion is not just about values, it's also about effects... wait what?^^

eddyb (Jun 03 2019 at 17:01, on Zulip):

no! it's about, at most, the effects needed to obtain that value!

RalfJ (Jun 03 2019 at 17:02, on Zulip):

"the effects needed to run that computation"

eddyb (Jun 03 2019 at 17:02, on Zulip):

it's about the computational needs

RalfJ (Jun 03 2019 at 17:02, on Zulip):

the same value, 42, can be obtained without effects

eddyb (Jun 03 2019 at 17:02, on Zulip):

yes but how do you know it's 42?

eddyb (Jun 03 2019 at 17:02, on Zulip):

at compile-time

RalfJ (Jun 03 2019 at 17:02, on Zulip):

(replace () by i32 in my example above, my argument stands and now you cannot synthesize)

RalfJ (Jun 03 2019 at 17:03, on Zulip):

all I am saying is we are not talking about properties of a value here, but abourt properties of a computation

eddyb (Jun 03 2019 at 17:03, on Zulip):

yes, computation for the "future runtime value"

RalfJ (Jun 03 2019 at 17:03, on Zulip):

and so I dont see why we cannot cast the question "may this const body computation occur at compile-time" in the same framework as the question "may this temporary be promoted implicitly"

eddyb (Jun 03 2019 at 17:04, on Zulip):

the final value may not depend on the side-effects

RalfJ (Jun 03 2019 at 17:04, on Zulip):

where currently we have qualifs for the latter but a visitor for the former

RalfJ (Jun 03 2019 at 17:04, on Zulip):

the final value may not depend on the side-effects

so? that's the case either way?

eddyb (Jun 03 2019 at 17:04, on Zulip):

heck, I think we promote &{ println!("foo"); 5 } today, let me check

RalfJ (Jun 03 2019 at 17:05, on Zulip):

even if we do, not sure how that changes anything. that's just a weird notion of "subterm".

eddyb (Jun 03 2019 at 17:05, on Zulip):

I'm saying that checking whether the computation that ends up in the return slot is promotable, doesn't tell you whether you can execute the entire body

eddyb (Jun 03 2019 at 17:06, on Zulip):

because there is no reification of the "worldstate" on exit

eddyb (Jun 03 2019 at 17:06, on Zulip):

if we had VSDG, this would be a much more different discussion

eddyb (Jun 03 2019 at 17:06, on Zulip):

then, yes, you could qualify everything with dataflow

eddyb (Jun 03 2019 at 17:06, on Zulip):

same thing for lambda calculus

eddyb (Jun 03 2019 at 17:06, on Zulip):

still, the checker has very fine-grained messages. qualification loses that detail

RalfJ (Jun 03 2019 at 17:07, on Zulip):

same thing for lambda calculus

now you lost me entirely^^

eddyb (Jun 03 2019 at 17:07, on Zulip):

I meant pure functional code

eddyb (Jun 03 2019 at 17:07, on Zulip):

side-effects are encoded in dataflow

RalfJ (Jun 03 2019 at 17:07, on Zulip):

still, the checker has very fine-grained messages. qualification loses that detail

right I understand that. I hate it when diagnostics makes the important code more ugly :(

eddyb (Jun 03 2019 at 17:07, on Zulip):

VSDG is just first-order functional calculus w/ linear types

RalfJ (Jun 03 2019 at 17:07, on Zulip):

but I wanted to understand if diagnostics is the only reason

eddyb (Jun 03 2019 at 17:08, on Zulip):

diagnostics are the main reason

eddyb (Jun 03 2019 at 17:08, on Zulip):

you'd still need a visitor for side-effects that don't (always) affect values

eddyb (Jun 03 2019 at 17:09, on Zulip):

https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=50042f128ce6e1d1be43b495e5f1ef1e

RalfJ (Jun 03 2019 at 17:09, on Zulip):

I'm saying that checking whether the computation that ends up in the return slot is promotable, doesn't tell you whether you can execute the entire body

sure, that has no bearing on my question though I don't think. once we cannot "peak" the computation any more because it's a const fn we still fall back to checking computation, and more importantly, relying only on the type here would be unsound -- which demonstrates that this is not an analysis of the value V, but of the computation M V living in some monad and eventually producing the value.

Last update: Nov 15 2019 at 20:25UTC