From/TryFrom as in Rust

Stream: std4

[Hanting Zhang]

Hello!

Are there any thoughts on having stuff from Rust's std::convert? i.e. From, TryFrom, Into, etc. Is this a direction Std wants to move in? If not, what would be the alternative way of encoding conversions?

[Mario Carneiro]

hm that seems like more of a language design question, I would rather take it to the core team

[Mario Carneiro]

Right now conversions seem to be expressed either via typeclasses that fix one side like ToString, ToExpr, FromJson, or via intrinsic methods like UInt32.toUInt64

[Mario Carneiro]

there is also the coercion system of course, which we use a lot more expansively than rust

[Mario Carneiro]

it doesn't seem like a good idea to have fallible conversions as coercions to option/except though

[James Gallicchio]

There are the various String.toXXX? functions that go into Option, but I'm not sure how well those generalize. Are those typeclasses used in Rust in the way we use coercions?

[Hanting Zhang]

Ok, thanks. For #xy, the original problem is you want to write things like

class Field (F : Type _) where
  Repr : Type _
  asBytes : ToByteArray Repr  -- ideally this can be resolved as an instance when constructing Fields
  toRepr : F \to Repr

Here Field is to denote a large prime field for cryptographic computations. Ideally, we would want to have some representation of field elements as bytes -- but we also may want to represent them with something with more information than just ByteArray. Hence, we have the need to say instead "we have some Repr, and Repr can be converted to ByteArray."

I look at this code though, and I feel like there's something off.

[Hanting Zhang]

The rust code would look something like

pub trait Field {
  Repr : AsRef<u8> + AsMut<u8>
  fn to_repr(&self) -> Self::Repr;
}

[Mario Carneiro]

which, interestingly, does not use {Try}{From,Into}

[Mario Carneiro]

I don't think we really have any equivalent of AsRef, since that is making an assertion about the actual byte representation of the value

[Hanting Zhang]

Oh, yes :man_facepalming: I guess here the example is using AsRef.

[Hanting Zhang]

What would be the best way to replicate the Rust code in Lean?

[Mario Carneiro]

what do you want to do with the bytes?

[François G. Dorais]

An answer to Mario's question is what is needed. However, if I'm right about your use case, Leo's "views" idea is something to look into. See:
<https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Error.3A.20unknown.20free.20variable.20'_uniq.2E402'/near/275522380>

PS: I vaguely recall a better reference on Zulip but I couldn't find it and I might have dreamed it. In any case, the test that Leo links to in the thread above is useful to grasp the idea.

[Siddharth Bhat]

For reference, the idea of a view is from the paper "the view from the left" by Conor mc bride