Unboxed `Partial`?

Stream: std4

[Mario Carneiro]

I don't really buy that we would save by factoring a.get! into a.get?.get!. Rust uses a[i] instead of a.get(i).unwrap() even though the latter functions are pretty much designed for the purpose and this is zero overhead

[Mario Carneiro]

These are just incredibly common functions, such that a shorthand is warranted

[Mario Carneiro]

(Even if we ignore the fact that a.get?.get! is not zero cost in lean)

[James Gallicchio]

RE: get/getD/get!/get? all over the standard collections APIs -- do we think it's possible to get a zero-cost implementation of Partial, where values are not boxed into a thunk? e.g. the runtime representation of Partial A h is the same as A if h is true, and undefined if h is not true

[James Gallicchio]

To me, (some operation).get.! reads just as fine as (some operation).get!, and cuts down on the size of the API that we need to maintain.

[Mario Carneiro]

The problem is that you would have to evaluate the expression to get something of type A

[Mario Carneiro]

but if it's undefined then this could cause UB

[Mario Carneiro]

so you have to leave it unevaluated, hence it's a thunk

[Mario Carneiro]

you can't evaluate it until you receive evidence that h is actually true

[James Gallicchio]

Yeah, I guess the compiler would have to inline whatever produces the Partial

[James Gallicchio]

in order to then optimize the box(0) application away

[James Gallicchio]

So I guess the question then is whether we could get compiler support for optimizing eliminators of Partial, which seems substantially less likely

[Mario Carneiro]

that almost certainly already exists, assuming Partial = Option

[Mario Carneiro]

you just have to inline enough stuff to make it possible to do

[James Gallicchio]

ah, hm

[James Gallicchio]

Let me see if I can get a Partial version of Array.get to produce identical bytecode

[James Gallicchio]

I guess it almost makes more sense to have an API for producing Fin ns by panicking on out of bounds :stuck_out_tongue:

[Mario Carneiro]

that's fine, although you can't define it for n = 0

[Mario Carneiro]

which makes it a lot less ergonomic than alternatives

[James Gallicchio]

that's an ergonomic issue of panic! generally, where there's no easy way to say that you want to escape to a farther out context which is Inhabited. the only solution I have to that ergonomics issue would be to start putting lots of stuff in an Except monad instead of panicking.

[James Gallicchio]

get! : [Inhabited A] -> Except E A -> A

[Mario Carneiro]

is that supposed to be returning something of type A?

[James Gallicchio]

maybe add a [ToString E] parameter to put in the panic message

[James Gallicchio]

maybe we have a ifOk : [IfOk E A B] -> A -> Except E B API for decidably failing coercions

[James Gallicchio]

get! <| do return A.get (←ifOk 0) does start to look absurd though :)

[Mario Carneiro]

yeah, I'm not seeing the ergonomic gain

[James Gallicchio]

I've definitely written code that would be cleaner with these abstractions, and not even niche code. But for small use cases it doesn't make sense.

[James Gallicchio]

Idk. I will push through the repetitive API for now

[James Gallicchio]

Honestly, textbook rust just opens Except String monad contexts everywhere and uses ? as a synonym for .←. I feel somewhat justified in doing the same in Lean.

[Mario Carneiro]

okay, but that's not the API in question

[Mario Carneiro]

Now is not a good time for redesigning Array. The API exists, we are just making the dependent version

[James Gallicchio]

:thumbs_up: will revisit this at some point

[François G. Dorais]

Sounds to me that the general end goal here is a more seamless interface for "safe laziness"? I've been wondering about that for a while too.

[James Gallicchio]

Not laziness but just better interfaces for handling quotients and partials

[Sebastian Ullrich]

I believe I had a proposal once for unified ?!D but I wouldn't know where to even start looking for it...