#rust-lang

if you change to Some, can't anymore

const fn currently is opaque, so value is assumed to be the worst (e.g. Some)

changing const's value is already backwards-incompatible

the same thing would apply to #[exposed]

<eddyb>changing const's value is already backwards-incompatible -- how do you mean?

if you change None to Some in my example

you'll break someone doing &FOO

in a const context... right

yeah

eddyb, surely this would still allow for breaking changes in consumer libraries though?

Noldorin: hmm?

this is an opt-in for "changing the body is a breaking change"

my argument was and still is that we can't do that by default

with opt-in it might just be fine

eddyb, I mean, a library author could change the definition of an exposed function so that it now returns something non-const, and that could cause downstream code not to compile.

something non-const under different conditions *

Laters guys =)

bye centril

Noldorin: yupp

Noldorin: (just afking, not leaving the channel ^,- )

it's their responsibility not to mess with bodies of exposed functions

just like signatures of all functions

(well, all publicly exported functions)

eddyb, you consider this a significant advantage over not allowing all functions to be used in const exprs with no annotation?

Noldorin: well it doesn't break the default ignorance of semver towards function bodies

which was my main concern wrt "no explicit const fn"

but it also lets you use the body to decide whether CTFE is allowed, instead of just the bounds

which means you no longer need all-const-fn impls

and you can do it as much as you want

maybe we can apply it module-wide

you don't have to expose bodies in lock-step with compiler CTFE capabilities or anything like that

since it's an orthogonal mechanism

and it would also apply to any other kind of effect checking or whatever we might want to add later

Noldorin: it could even allow finer-grained borrowck or something but I wouldn't hold my breath :P

#[exposed] is prolly a bad way to do this but rn I'm out of ideas

eddyb, well, using the `const` keyword but with #[exposed] semantics might look nicer...

...if syntax is your concern

Noldorin: it wouldn't make sense though

why not?

because the body need not be CTFE-ready

hmm

eddyb, right, then an 'exposed' or 'ctfe' keyword maybe

or something like that

either way, a keyword sounds better than an attribute

sure

now that I understand this, I can definitely see the benefits.

will see what centril thinks, but perhaps he'll update the RFC along these lines... providing he doesn't find a blocker.

thanks for the explanation

bbiab

Noldorin: keep in mind we could apply it impl-wide or module-wide just as easily

writing the comment now

is `exposed` basically equivalent to putting it in a macro?

scottmcm3: very vaguely so. but keep in mind this can be a trait impl method

oh man, macros 3.0 that puts macros as trait items :P

(yes, I know that definitely isn't happening)

Noldorin, centril, scottmcm3: can I ask y'all to not refer to #[exposed] on the RFC thread, in case someone has a better idea :D?

`fn foo() -> T pub {...}` looks dumb though

eddyb: ok ;)

`-> pub T { ... }` also is not ideal

scottmcm3: macros 3.0 :/ how many more versions do we need?

then again, if you do it impl/mod-wide

centril: that was sarcasm :P

an attribute seems best

scottmcm3: Be careful - or someone will propose it ;) Like durka, he loves macros.

eddyb: roger wilco

[PR 2237] <open> RFC: const bounds and methods <https://github.com/rust-lang/rfcs/pull/2237>;

I'll edit it if it's too obtuse

or if someone makes a better syntax proposal

eddyb: That's fine i think

"transparent" is another word

22:55 <E7AA00~ eddyb> it's the difference between a crappy effect system and making the body transparent to effect systems

eddyb: what's the E7AA00 prefix there?

the what

idk IRCCloud copied including formatting

aha

could be some IRCv3 thing

which is apparently real and in use

centril, Noldorin: okay I admit having const fn mean "transparent body for the purposes of CTFE checks" *might* just work?

still checkable for backwards-compat breakage

eddyb: OTOH I don't like the thought of changing the body of an fn being a bc-break

const fn*

the alternative is ofc the conservative parametric const fn I previously advocated for

or something even stricter

"conservative parametric const fn" is what you proposed in the rfc?

centril: the thing where T: Trait means "const Trait when called at compiletime"

eddyb: right, I accepted that idea, just haven't changed the RFC yet

needs a bit of fleshing out

the transparent body approach, whether const fn or orthogonal, would also make derives much easily CTFE-compatible

*much more easily

brb, there are cookies @ kitchen that require eating.

centril: BTW, I think you'd really enjoy the 1ML effects paper

centril: I think it's the right template for (someday, in some language) being properly parametric over total/pure/mut/etc :D

eternaleye: =)

Also, they have an interesting notation for effectful functions

in -> effect/out

eternaleye: sounds like an indexed state monad i -> (o, a)

So you could have `pred : nat -> partial/nat`

eternaleye: what does ty / ty entail?

or eff/ty

centril: "invoking pred (potentially) releases the 'partial' effect, while producing a 'nat'"

centril: One thing that might be cool - if in a partial function you had to annotate the site of partiality (akin to writing in the partiality monad), then it might be possible to call a partial function from a total one iff it can be shown at compile time to avoid the trace that meets that site

eternaleye: that sounds very interesting indeed

This is basically eddyb's #[exposed], which I think makes much more sense for total/partial than for pure/impure :P

I guess I have to read the papers to fully grasp everything

centril: The special effects paper is short and sweet

eternaleye: Time for some video games. Thanks for the papers!

eternaleye: that also sounds hilarous :P

Bascally, it's 1.) sound effect polymorphism 2.) effect polymorphism at the type level is generativity polymorphism 3.) generativity polymorphism is super cool

eternaleye: btw... do you have any experience with erlang-style statem testing?

centril: I do feel that 1ML may be right up your alley - the core calculus of 1ML_ex is total, has effects (once you add in the special-effects paper), has parameterized modules, and they even plan to add dependent types :D

They add partiality at the term level with a "fix" primitive, and recursive types are also added in separately

eternaleye: It does sound very cool =)

And no, I've never touched erlang

eternaleye: or any other form of property based & randomized state machine testing

(I personally feel that 1ML, plus linear types, plus Rust-like references, might be very nearly ideal for me)

centril: Oh, I use property-based testing plenty

QuickCheck is bae

scottmcm3: The main loop doesn't need partiality, it just needs corecursion

eternaleye: Yeah, me too, but I have no experience with PBT + state machines

eternaleye: so I'm thinking of how it can be added to {!crate proptest}

proptest (0.3.3) - Hypothesis-like property-based testing and shrinking. -> https://crates.io/crates/proptest <https://docs.rs/proptest>;

scottmcm3: Also, https://personal.cis.strath.ac.uk/conor.mcbride... is a good read regarding what you can do in a total language. (Everything. The answer is 'everything'.)

McBride is a cool dude

scottmcm3: The gist is that there are actually _two_ meaningful notions of computation - "programs" (which, when total, have _termination_ guarantees) and "coprograms" (which, when total, have _productivity_ guarantees)

Programs use recursion on strictly-decreasing input, and so terminate

eternaleye: everything as in "nothing will actually ever need more than 2.pow(128) steps"?

ah, I see

Coprograms use corecursion on strictly-increasing output, and so make progress at every step