Traits: compute explicit implementation expressions

[W95Psp]

Consider the following code:

trait Show {
    fn show(self) -> String;
}
// Let's name this impl. `ShowStr`
impl Show for &str {
    fn show(self) -> String {
        self.to_string()
    }
}
// Let's name this impl. `ShowU8`
impl Show for u8 {
    fn show(self) -> String {
        format!("{}", self)
    }
}
// Let's name this impl. `ShowVec`
impl<T: Show, U: Show> Show for (T, U) {
    fn show(self) -> String {
        format!("({}, {})", self.0.show(), self.1.show())
    }
}

The expression (1, "a").show() is for now translated as a call to the method show of the typeclass/trait Show with argument (1, "a"). Some backends might have no typeclasses or traits, and some (like F*) have typeclasses mechanisms whose inference mechanism is not great.

Thus, we need the frontend to derive the implementation expressions (i.e. ShowVec ShowU8 ShowStr for (1, "a").show()).

---

Edit: we've got another constraint.
In the engine, we often transform some patterns (i.e. mutation, loops) into function calls that are trait methods. Thus, maybe we should not do impl resolution in Rust, but on the OCaml side. Or do both: we should anyway export as much info in the frontend, but we'll need to do some impl resolution in the engine.

---

Status: @sonmarcho has some great prototype for that :tada:

---

Status (2023-12-21): this was done by #249 on the frontend side, and will be completed in the engine by #372

[spitters]

Is there a good comparison between the type class implementations in F*, Coq and lean? https://www.fstar-lang.org/tutorial/book/part3/part3_typeclasses.html

On Wed, Apr 12, 2023 at 8:42 AM Lucas Franceschino @.***> wrote:

Consider the following code:

trait Show { fn show(self) -> String;}// Let's name this impl. ShowStrimpl Show for &str { fn show(self) -> String { self.to_string() }}// Let's name this impl. ShowU8impl Show for u8 { fn show(self) -> String { format!("{}", self) }}// Let's name this impl. ShowVecimpl<T: Show, U: Show> Show for (T, U) { fn show(self) -> String { format!("({}, {})", self.0.show(), self.1.show()) }}

The expression (1, "a").show() is for now translated as a call to the method show of the typeclass/trait Show with argument (1, "a"). Some backends might have no typeclasses or traits, and some (like F*) have typeclasses mechanisms whose inference mechanism is not great.

Thus, we need the frontend to derive the implementation expressions (i.e. ShowVec ShowU8 ShowStr for (1, "a").show()).

— Reply to this email directly, view it on GitHub https://github.com/hacspec/hacspec-v2/issues/20, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTTZVGIUC7TG7SM5VBLXAZFFNANCNFSM6AAAAAAW3HQ2B4 . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[spitters]

I believe there is some work on adding type classes to Easycrypt. Do you happen to know more?

On Wed, Apr 12, 2023 at 8:51 AM Bas Spitters @.***> wrote:

Is there a good comparison between the type class implementations in F*, Coq and lean? https://www.fstar-lang.org/tutorial/book/part3/part3_typeclasses.html

On Wed, Apr 12, 2023 at 8:42 AM Lucas Franceschino < @.***> wrote:

Consider the following code:

trait Show { fn show(self) -> String;}// Let's name this impl. ShowStrimpl Show for &str { fn show(self) -> String { self.to_string() }}// Let's name this impl. ShowU8impl Show for u8 { fn show(self) -> String { format!("{}", self) }}// Let's name this impl. ShowVecimpl<T: Show, U: Show> Show for (T, U) { fn show(self) -> String { format!("({}, {})", self.0.show(), self.1.show()) }}

The expression (1, "a").show() is for now translated as a call to the method show of the typeclass/trait Show with argument (1, "a"). Some backends might have no typeclasses or traits, and some (like F*) have typeclasses mechanisms whose inference mechanism is not great.

Thus, we need the frontend to derive the implementation expressions (i.e. ShowVec ShowU8 ShowStr for (1, "a").show()).

— Reply to this email directly, view it on GitHub https://github.com/hacspec/hacspec-v2/issues/20, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTTZVGIUC7TG7SM5VBLXAZFFNANCNFSM6AAAAAAW3HQ2B4 . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[W95Psp]

Mmh, so I have no idea whether there exist some comparisons, but in F* (and Coq I believe) typeclasses resolve to dependent records + special inference mechanism. Yes, Easycrypt is about to get typeclasses (but I don't exactly know when!)

[spitters]

The F* documentation hints that they got that from Coq (dep records + eauto proof search).

On Wed, Apr 12, 2023 at 9:01 AM Lucas Franceschino @.***> wrote:

Mmh, so I have no idea whether there exist some comparisons, but in F* (and Coq I believe) typeclasses resolve to dependent records + special inference mechanism. Yes, Easycrypt is about to get typeclasses (but I don't exactly know when!)

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you commented.Message ID: @.***>

[W95Psp]

Oh, right, that makes sense then!

[W95Psp]

The extraction of impl expression from Rustc was done in the backend by #249

This information is used for associated types in Hax's AST, but not yet for other associated items (e.g. method calls).