#rust-lang

scottmcm3: (let Some(x) = 5); wouldn't typeck tho (a later stage, but still)

Havvy: o.O I didn't know you could use + that way

playbot-mini: fn main () { +2; }

You can't.

k great, the world is sane again

scottmcm3: Assuming I'm a parser, I start parsing 'let ' and then I start parsing <PATTERN> (metavar) then '=' and then <EXPR> - if I now see a ';' it is a statement. Otherwise, either an operator follows (like &&) and I parse another <EXPR>.. If ; never follows, it is an expr. I can't see how this requires infinite lookahead tho, but makes parsing a bit complicated.

Havvy: ^

Havvy: That is fair - I only want to show at this stage that it is possible to have general bool-typed let expressions

not to add them to the RFC now

I want to show forward-compatibility with that idea and then move on and ask people to write a separate RFC

about that...

I would like to have refutable let statements that panic though.

Havvy: then you have questions about unwinding and aborts ... :/

It'd be opt in, e.g. `let ref Some(x) = my_option_I_know_is_Some;` (but `ref` wouldn't work because it's already got meaning in patterns)

Havvy: right, but opt into what sort of panic?

`let or unwind Some(x) = my_opt;`

`let or abort Some(x) = my_opt;`

`unwind or let Some(x) = my_opt;`

centril: That's set by the panic=unwind|abort setting.

Havvy: ah, then `panic or let Some(x) = my_opt;`

but I want to reduce the number of panics in Rust code - so idk if I'm very happy about this

It'd be entirely opt-in, so :shrug:

Havvy: what does :shrug: mean? 1. sigh, 2. idk, 3. ?

As in, I don't see it as a problem to have opt-in panicking operations.

Idk... I think it is probably too easy to .unwrap() today

centril: would the easiness of unwrap be mitigated if we had total fns?

garagedragon: elaborate?

You can't have an unwrap() call hiding inside a total function

the better way to describe that is "never panics"

eddyb: it's a total function, not "it never panics"

total as in: termination is guaranteed

eddyb: A total function is also not allowed to do things like infinite loops

yes I'm just saying total functions are overkill for that

also not really doable for systems which are meant to never terminate under normal function :P

garagedragon: If there was a badge-of-honour like culture to have total wherever possible, then .unwrap()s might be reduced

eddyb: sure, but you might still want to prove totality for a part of the program

total requires never-panics which implies never-panics is easier to prove

centril: shame we can't borrow MS Research's time machine and make totalness the default :D

garagedragon: they have a time machine now? Cool.

I don't think totality checking is nearly as tractable as never-panicking

eddyb: granted, but still nice

centril: It's a running joke on Old New Thing because he gets so many suggestions about, "why not solve X problem with [feature that didn't exist when X first came about]?"

I have my doubts for anything with I/O

(i.e. not pure computation)

things like "keep reading until you've finished"

I think totality in the face of IO is difficult because of the FFI involved more than anytihng to do with IO in particular

"Keep reading until you're finished" obviously wouldn't be total, but individual read calls could be

eddyb: my thinking is: unsafe blocks <: total fn <: no_panic fn <: const fn <: fn <: unsafe fn

eh

unsafe blocks acting as a "I postulate that this is total, trust me"

wat

OTOH

unsafe{} doesn't impl total.

that seems both pointless and problematic

Speaking of unsafe, what _syntax_ does unsafe code allow that safe code doesn't? Is it only pointer deref?

garagedragon: no new syntax

yeah, that's a bad phrasing. I mean more, "fundamental operations"

Havvy: probably some other word then

Derefencing of raw pointers, reading union fields, calling unsafe fns.

garagedragon: accessing a static mut, dereferencing a raw pointer, calling unsafe functions

oh right union fields too

eddyb: why is it pointless and problematic?

centril: because a loop inside unsafe {} might not have anything to do with the unsafe {} itself

i.e. you seem to be conflating things

unsafe{} is distinct from total{}ness.

You would want a new untotal{} keyword.

lmao

eddyb: right right - postulate { /* i have checked myself that this is total */ }

or what Havvy said

centril: in the context of a total fn, you mean?

garagedragon: yea

I can see how that'd be useful, but I also kinda feel that totalness should be provable from first principles and not rely on *any* code being "bug free?"

garagedragon: not even Agda adheres to that principle

Agda has postulate , which is "ok; this is an axiom I can make whatever shit up I like here"

I'm guessing that that somehow helps prove totality in cases where the compiler's too dumb?

garagedragon: well you can postulate things like function extensionality or the univalence axiom

perhaps it helps prove totality in some cases

it may also be that you don't have time to make a machine checkable proof for some thing that was proven ages ago on paper, so just postulate it

I.e: you want to show that your conjecture flows from other lemmas and theorems, but you don't have time to encode those

that's true

I'm not really familiar with programming in terms of logical proofs

garagedragon: maybe more a mathematicians toolbox than a programmers

but the intersection is interesting

centril: I suppose the original I was getting at was that if you allow non-total code inside unsafe blocks, then a buggy unsafe block can lead to a "total" function failing to halt or panicking, which blunts the point of having the marker at all

garagedragon: Not sure I understand the 'setup' you are referring to - we have a total fn which has an unsafe block inside?

Yeah

if you have something like:

garagedragon: I think that argument is the same one as "why have safe fns at all when you can have unsafe blocks inside"

yeah, so it doesn't entirely make the marker useless, just less strong than it looks

and my reply is that the keyword gives you easy grepability and the blame is evident from the source code

sure, I think it's a pragmatic trade-off

If you have total fn count_something_finite() { unsafe { iterator_I_promise_is_finite().count() } }, and you're wrong about the iterator being finite, then your code hangs in a "total" function

garagedragon: right

or just untotal { iterator.. } for simplicity

Made an issue about untotal {..} on git, so dump ideas there too =)

"centril> scottmcm3: (let Some(x) = 5); wouldn't typeck tho (a later stage, but still)"

^ why not? `true;` typecks

scottmcm3: 5 is not Option<X>

oh, right. `let Some(5) = x` then

:P

scottmcm3: So I've asked on the RFC about a demonstration showing that `EXPR is PAT` is better than `let PAT = EXPR` wrt. parsing perf, etc.

s/about/for

well, what's the proposed fallible expression? just add `let PAT = EXPR` to the expression grammar, returning bool?

scottmcm3: yes

(more or less, exact grammar has to be worked out ofc)

that has the problem I'm mentioning, then.

and saying "well, if that's the only expression treat it like the old statement" doesn't go well because macro

My main interest at this stage is ensuring that let pat = expr would work as a bool-typed expression, then we can move on from that question and not deal with it in this RFC

macros :/

scottmcm3: well it was more like "when you find ; you know it's a statement"

but expression followed by ; is also a legal statement

scottmcm3: example?

hmm. is there currently any way to make something conditionally const, depending on a cfg feature?

something... a function

centril: `foo();`

scottmcm3: ends with a ; so we know it's a statement

right, but a let statement and a expr-statement-containing-a-let do different things

despite being the same token sequence

so I don't think it can work

and I don't think it should, even if it can, since it makes something so similar do something so different

scottmcm3: right, so 'let foo = 1;' is both "an stmt to assign 1 to foo" and "a statement that pattern matches and yields a bool but throws the bool away"

the latter seems useless

what's the argument against special casing this?

probably things like that it's really weird for `{let Some(5) = x}` and `{let Some(5) = x;}` to be so different, since it's not just a type change like `;` normally is

scottmcm3: how is it not just a type change?

BTW, officialy, are types like const *! or &! inhabitable...?

centril: because one is fallible

garagedragon: the former definitely is, with null

garagedragon: otoh: there's no way to construct &! with a valid value, but *const ! can have a value (an adress pointing to nonsense)

the latter is an open question, though I suspect it'll be uninhabited at least from a match perspective

scottmcm3: my intuition about it is that it is UB the second you deref

garagedragon: there's an RFC open about it

!rfc 1872

[PR 1872] <open> Fix the handling of uninhabited types in pattern matching. <https://github.com/rust-lang/rfcs/pull/1872>;

centril: a friend made the point that &! can't be inhabited because derefing it is safe, and since you can never have a ! to reference, there can be no valid &!, even if there are usable pointers under the hood

scottmcm3: 'let Some(5) = x' eq '{let Some(5) = x}' and 'let Some(5) = x;' eq '{let Some(5) = x;}' idk how it's weird...?

garagedragon: I think that is exactly right, the program will panic before you ever get to make a &!

the former two work, the latter two are "must be irrefutable pattern" errors, centril

garagedragon: see the RFC. the complicated question is around unsafe and uninitialized values and such

scottmcm3: ooooh, now I see it

dummy me