Rust for non-Rustacean math-y types

# Rust for non-Rustacean math-y types *This hackmd is prepared for the purposes of discussion with folks familiar with PL/proof/logic/etc but not so much with Rust.* ## Overarching goals for today * We have some practical problems * Want to extend our semantics to be coinductive but not sure how to handle * How to best describe associated types ("beyond syntactic equality") * We have some more abstract problems * We want to map Rust's trait system to logical concepts so we can reason about it better * Building an (executable) model of the Rust type system to serve as a "spec" ([a-mir-formality](https://github.com/rust-lang/a-mir-formality)) ## Simple Rust program ```rust trait Clone { fn clone(&self) -> Self; } impl Clone for u32 { fn clone(&self) -> Self { *self } } impl<T> Clone for Option<T> where T: Clone, { fn clone(&self) { match self { Some(x) => x.clone(), None => (), } } } fn foo<T: Clone>(t: T) { t.clone(); } fn main() { foo(22); foo(Some(22)); } ``` ## Supertraits ```rust trait Eq: PartialEq {} // supertrait trait PartialEq { fn partial_eq(self, other: Self) -> bool; } fn foo<T: Eq>(a: T, b: T) { // ^^ a.partial_eq(b) } ``` ## Associated types ```rust trait Iterator { type Item: Clone; fn next(&mut self) -> Option<Self::Item>; } fn clone_all<I: Iterator>(i: I) { while let Some(elem) = i.next() { // elem has type `I::Item`... elem.clone(); // ...and we know that impl `Clone` } } ``` ## Rust 0 Grammar ``` Program := (TraitDefn | StructDefn | Implementation)* TraitDefn := trait Tr {} Ty := S < {Ty} > | X StructDefn := struct S < {X} > Implementation := impl<{X}> Tr for Ty where WC {} WC := (Ty : Tr) | WC, WC X := identifier of a generic parameter ``` ## Defining Rust trait solver So given a `Program`, when can we judge a given trait to be implemented? We'll define a judgment `WC_a |- WC_g`. This means that, given the assumptions `WC_a`, `WC_g` is provable. So far WC is just `(Ty: Tr)`, so e.g. `|- (u32: Clone)` says that `Clone` is implemented for `u32`. ``` substituted impl Tr for Ty_t where WC Ty_t = Ty_s A |- WC ------------------------------- impl A |- (Ty_s: Tr) ``` ``` impl<{X}> Tr for Ty_t where WC let S be some substitution for {X} S Ty_t = Ty_s A |- S WC ------------------------------- impl A |- (Ty_s: Tr) ``` ```rust impl Clone for u32 where true impl<T> Clone for Option<T> where T: Clone, ``` ``` impl<T> Clone for Option<T> where (T: Clone) S = { T => u32 } -- inferred by the compiler via unification S Option<T> = Option<u32> --after-substitution--> Option<u32> = Option<u32> A |- S (T: Clone) --after-substitution--> A |- (u32: Clone) ------------------------------- impl A |- (Option<u32>: Clone) ``` And we can define some basic connectives: ``` ------------------------------- environment ..., WC_i, ... |- WC_i ``` ``` A |- WC_0 A |- WC_1 ------------------------------- and A |- WC_0 && WC_1 ``` ...and some basic things like weakening, reordering, which I won't bother to list. ## Defining Rust trait solver Now we can use this to prove interesting things like `Option<u32>: Clone`: * `Option<u32>: Clone`, from `impl<T> Clone for Option<T> where T: Clone` with substitution `[u32 / T]` * `u32: Clone`, from `impl Clone for u32` ## Extending to higher-ranked stuff More interestingly, we can extend WC to include higher-ranked things and implications: ``` WC = (WC && WC) | (T: Trait) | forall<X> WC | (WC => WC) ``` with rules like ``` X not free in A, Program A |- WC ------------------------------- forall-introduction A |- forall<X> WC ``` and ``` (A, WC_0) |- WC_1 ------------------------------- implication-introduction A |- (WC_0 => WC_1) ``` and ``` A |- (forall<X> WC_0) ------------------------------- forall-elimination A |- { Ty / X } WC_0 ``` ``` A |- (WC_0 => WC_1) A |- WC_0 ------------------------------- implies-left A |- WC_1 ``` Why would we do this? As it happens, Rust includes "higher-ranked trait bounds", but we also need to be able to do forall and implication just to do basic type checking. For example, consider this function: ```rust fn clone_t<T>(t: T) where T: Clone, { let o: Option<T> = Some(t); o.clone(); // valid if `Option<T>: Clone` } ``` To prove that `o.clone()` is valid, the type-checker wants to judge that `Option<T>: Clone`. We can express that as ``` |- forall<T> ((T: Clone) => (Option<T>: Clone)) ``` and we can prove this via the above rules * `|- forall<T> ((T: Clone) => (Option<T>: Clone))`, then by rule "forall-introduction".. * `|- ((T: Clone) => (Option<T>: Clone))`, by rule "implication-introduction"... * `(T: Clone) |- (Option<T>: Clone)`, by rule "impl"... * `(T: Clone) |- (T: Clone)`, by rule environment. ### ill-typed program ```rust fn clone_t<T>(t: T) { let o: Option<T> = Some(t); o.clone(); // valid if `Option<T>: Clone` } ``` * `|- forall<T> (Option<T>: Clone)`, then by rule "forall-introduction".. * `|- (Option<T>: Clone)`, by rule "impl"... * `|- (T: Clone)` cannot be proven ### Supertrait declarations Extend grammar ``` TraitDefn = trait Tr: Tr {} ``` so that e.g. ```rust trait Eq: PartialEq {} // supertrait trait PartialEq {} ``` can be permitted by a rule ``` trait Trait2: Trait1 {} A |- (T: Trait2) ------------------------- supertrait v1 A |- (T: Trait1) ``` ## More ill-typed ```rust trait Clone { fn clone(&self) -> Self; } struct S { } fn main() { let s = S { }; s.clone(); // ERROR -- if this were to execute, we would have no method definition to use // "goes wrong" } ``` ## What does soundness mean? What does proving ``` |- WC ``` *mean*? We are trying to maintain an invariant here, that `WC` is *truly true*, meaning... * When `WC = (T: Trait)`, then * `T` is a struct in the program * and there exists a (substituted) impl such that `Self = T` and all WC are *truly true* * When `WC = forall<{X}> WC_0`, then * for any well-defined substitution `S` such that `S WC_0` is *truly true* * where well-defined means that it only refers to structs declared in the program * When `WC = WC_0 => WC_1`, then * if `WC_0` is *truly true*, then `WC_1` is *truly true* * (or *provable* implies *truly true*?) * When `WC = WC_0 && WC_1`, then * both `WC_0` and `WC_1` are *truly true* We would like to guarantee that * If `|- WC` then `WC` is *truly true*. The rule system we developed so far does not meet this property -- because of supertraits. ## But ```rust trait Eq where Self: PartialEq, { } trait PartialEq { fn partial_eq(&self); } impl Eq for u32 { } // This is missing: // // impl PartialEq for u32 { fn partial_eq(&self) { X } } fn main() { let t: u32 = 22; t.partial_eq(); // Provable, but should it be? } ``` * `|- (u32: PartialEq)`, via supertrait rule (which says that `Eq=>PartialEq`) * `|- (u32: Eq)`, via impl (`impl Eq for u32`) * ok! ## Possible solutions ### Validate the impl ``` trait Tr: Tr1 {} |- forall<{X}> (WC => Ty: Tr1) ---------------------------- |- impl<{X}> Tr for Ty where WC { } OK ``` But what about ```rust trait Clone { fn clone(&self) -> Self; } trait Magic: Clone impl<T: Magic> Magic for T { /* ok on its own */ } fn main() { let t: u32 = 22; t.clone() // "almost" provable, even though there is no `impl Clone for u32` } ``` * `|- u32: Clone`, via supertrait (MAgic => Clone) * `|- u32: Magic`, via impl * `|- u32: Magic`, via impl * `|- u32: Magic`, via impl * ...never get a finite proof tree... * today we are inductive, but we want to be coinductive This impl appears well-formed. Using it will cause an infinite proof, however (but see coinduction notes later). #### Forbid blanket impls like this? Also forbids useful patterns that we rely on everywhere, most obviously... ```rust trait Extension: BaseTrait { fn new_method(&self); } impl<T: BaseTrait> Extension for T { // ^^^^^^^^^^^^ "syntactically" the same fn new_method(&self) { /* just use methods from the base trait */ } } ``` ...in general enforcing ordering etc gets tricky. ### Check the assumptions when you use the impl Our solution: ``` impl<{X}> Tr for Ty_t where WC {} trait Tr: Tr1 {} // <-- changed let S be some substitution for {X} S Ty_t = Ty_s A |- S WC A |- (Ty_s: Tr1) // <-- changed ------------------------------- impl v2 A |- (Ty_s: Tr) ``` ## Desired change to Rust: coinductive semantics We allow people to write `#[derive(Clone)]`. This will autogenerate the code for cloning. Given a struct like this ```rust #[derive(Clone)] struct Tree<T> { data: T, children: Vec<Tree<T>>, } // impl<T> Clone for Vec<T> where T: Clone { .. } ``` it could for example generate ```rust impl<T> Clone for Tree<T> where T: Clone, Vec<Tree<T>>: Clone, { fn clone(&self) -> Self { Tree { data: self.data.clone(), children: self.children.clone(), } } } ``` OK, so far so good. But now you go to prove, say, that `Tree<u32>: Clone` and you get... * `Tree<u32>: Clone` if * `u32: Clone` -- true * `Vec<Tree<u32>>: Clone` if * `Tree<u32>: Clone` * cycle -- in an inductive semantics, this is an error We would like to shift to coinductive semantics. In fact, we already have it for some traits (e.g., `Send`, which indicates a thread-safe data structure). ### BUT: implications We can't just take the rules we've been using and interpret them coinductively. It will break with supertraits. ```rust trait Eq: PartialEq ``` then we had the equivalent of a rule like ``` A |- T: Eq ------------- A |- T: PartialEq ``` which is clearly not productive. This can be "weaponized": ```rust trait Haha: Clone { } impl<T: Haha> Haha for T { } ``` would result in ``` A |- T: Haha --------- "supertrait" A |- T: Clone ``` ``` A |- T: Haha --------- "impl" A |- T: Haha ``` given these traits and impls, you can prove `X: Clone` for any type `X` (not just those types that have impls). How? * `X: Clone`, using "supertrait" * `X: Haha`, using "impl" * ... (ad infinitum) * `X: Haha`, using "impl" ### How we are handling it in our model today Don't permit "general" coinduction. Instead, only allow coinductive reasoning when proving impl where clauses: ``` trait Tr: Tr1 {} impl<{X}> Tr for Ty_t where WC {} let S be some substitution for {X} S Ty_t = Ty_s A, (Ty_s: Tr) |- S WC // <-- changed // ~~~~~~~~~~ permit cycles A |- (Ty_s: Tr1) ------------------------------- impl v3 A |- (Ty_s: Tr) ``` Simplified ``` trait Trait: TrSuper {} substituted impl Trait for Ty_self where WC {} A, (Ty_self: Trait) |- WC // <-- coinductive A |- (Ty_self: TrSuper) ------------------------------- impl v3 A |- (Ty_self: Trait) ``` ``` trait Trait: TrSuper {} A, later (Ty_self: Trait) |- (Ty_self: Trait) implemented A, later (Ty_self: Trait) |- (Ty_self: TrSuper) ------------------------------- A |- (Ty_self: Trait) ``` ``` substituted impl Trait for Ty_self where WC {} A0, (Ty_self: Trait) |- WC ------------------------------- impl A0, later (Ty_self: Trait) |- (Ty_self: Trait) implemented ``` Now if we have a "cyclic" impl like so ```rust trait Magic: Clone { } impl<T: Magic> Magic for T { } ``` * `|- u32: Clone`, via supertrait rule * `|- u32: Magic`, via impl * `(u32: Magic) |- (u32: Magic)` (impl where clauses) -- OK! * via assumption * `|- u32: Clone` (because `trait Magic: Clone`) * cycle (rules are inductive --> error) you can still try to prove `T: Clone` by first proving `T: Magic` but then you just have to prove `T: Clone` again (without the benefit of the cyclic assumption). ## What does soundness mean... coinductively? Let's say a WC `WC` is *truly true* if * When `WC = (T: Trait)`, then there exists a (substituted) impl such that `Self = T` and all WC are *truly true* * When `WC = forall<{X}> WC_0`, then for any substitution `S` such that `S WC_0` is *truly true* * When `WC = WC_0 => WC_1`, then if `WC_0` is *truly true*, then `WC_1` is *truly true* * (or *provable* implies *truly true*?) * When `WC = WC_0, WC_1`, then both `WC_0` and `WC_1` are *truly true* We would like to guarantee that * If `|- WC` then `WC` is *truly true*. ## Challenges and questions so far * How do we define *soundness*? * We can show that whenever you can prove `|- Ty: Foo`, there wll always be an `impl` rather trivially by induction * But can we relate that to an approximation of an underlying "logic"? * e.g., translate `impl<T> Clone for Option<T> where T: Clone` to `(Option<T>: Clone) :- (T: Clone)` and interpret coinductively * show that our solver is an approximation of that * for example `impl<T> Trait for T where Option<T>: Trait` is coinductively true (infinite proof tree) but it is not provable in our system * but then what about `forall` and implication, and how do we take into account supertraits? * e.g. `forall<T> ((T: Eq) => (T: PartialEq))` should be a provable WC, but we can't translate `trait Eq: PartialEq` to `(T: PartialEq) :- (T: Eq)` and still interpret coinductively * what precedent is there here to look at? ### Sidenote: Elaborating assumptions? ``` (Ty: Eq) in A A, (Ty: PartialEq) |- WC ------------------------ "supertrait(Eq/PartialEq)" A |- WC ``` ## Associated types (or "aliases") Grammar ``` Program := (TraitDefn | StructDefn | Implementation)* TraitDefn := trait Tr where WC { AssocTypeDefn } // ~~~~~~~~~~~~~ new AssocTypeDefn := type Assoc : {Tr} // <-- new Ty := S < {Ty} > | X | Ty::Assoc // <-- new StructDefn := struct S < {X} > Implementation := impl<{X}> Tr for Ty where WC { AssocTypeValue } // ~~~~~~~~~~~~~~ new AssocTypeValue := type Assoc = Ty // <-- new WC := (Ty : Tr) | Ty: Tr<Assoc = Ty> // <-- new | WC, WC X := identifier of a generic parameter ``` ```rust! trait Clone { } impl Clone for u32 { } trait Iterator { type Item: Clone; // <-- associated type fn next(&mut self) -> Option<Self::Item>; } impl<T> Iterator for Vec<T> where T: Clone, { type Item = T; fn next(&mut self) -> Option<Self::Item> { .. } } fn foo(iter: &mut I) where I: Iterator, { let v: Option<I::Item> = iter.next(); v.clone(); } fn main() { let v: Vec<u32> = Vec::new(); let i: Option< u32 > = v.next(); let j: Option< <Vec<u32> as Iterator>::Item > = v.next(); } ``` ## What does soundness mean... for associated types Let's say a WC `WC` is *truly true* if * When `WC = Ty0: Tr<Assoc = Ty1>`, then * there exists exactly one (substituted) impl `I` such that * `Self = Ty0`, * all its WC are *truly true*, * `I` defines `Assoc` as `Ty1` (after subst). * (exactly one = job of coherence, out of scope?) and, as before, unchanged * When `WC = (T: Trait)`, then there exists a (substituted) impl such that `Self = T` and all WC are *truly true* * When `WC = forall<{X}> WC_0`, then for any substitution `S` such that `S WC_0` is *truly true* * When `WC = WC_0 => WC_1`, then if `WC_0` is *truly true*, then `WC_1` is *truly true* * (or *provable* implies *truly true*?) * When `WC = WC_0, WC_1`, then both `WC_0` and `WC_1` are *truly true* We would like to guarantee that * If `|- WC` then `WC` is *truly true*. ## * `Vec<X> = Vec<u32>` => `X = u32` * `X::Item = u32::Item` => ? * just as `f(x) = f(y)` does not tell me that `x = y` for an arbitrary function `f` ```rust fn foo<X: Iterator<Item = u32>>(x: X) { X::Item ==> u32 } ``` ```rust! fn foo<U, X: Iterator<Item = U>>(x: X) { X::Item ==> U } ``` ## ``` WC = T: Trait<Assoc = U> ``` ``` A |- U = T::Assoc ------------------------------- fallback A |- T: Trait<Assoc = U> ``` ``` substituted impl Tr for T where WC { type Assoc = S; } A, T: Trait<Assoc = S> |- WC ------------------------------- normalize-via-impl A, later(T: Trait<Assoc = S>) |- T: Trait<Assoc = S> ``` ``` trait Trait0 { type Assoc: Trait1 } ------------------------------- fallback A |- T::Assoc: Trait1 ``` ``` --------------------------- A |- T = T ``` ``` A |- T: Trait<Assoc = U1> A |- U1 = U2 --------------------------- A |- (T::Assoc) = U2 ``` ### cyclic normalization impl ```rust trait Trait { type Assoc; } impl Trait for i32 { type Assoc = <u32 as Trait>::Assoc; } impl Trait for u32 where i32: Trait<Assoc = ()>, { type Assoc = (); } ``` - `|- i32: Trait<Assoc = ()>` normalize via impl - (no where clause, output = `<u32 as Trait>::Assoc`) - `|- <u32 as Trait>::Assoc = ()` eq-via-normalize - `|- u32: Trait<Assoc = ()>` normalize via impl <-- productive - in where-clause `|- i32: Trait<Assoc = ()>` cycle - `|- () = ()`, ok because "duh" ```rust= trait OtherTrait { type OtherAssoc; } trait Trait { type Assoc; } impl<U: OtherTrait> Trait for i32 { type Assoc = <u32 as Trait>::Assoc; } impl<U: OtherTrait> Trait for u32 where i32: Trait<U, Assoc = U::OtherAssoc>, { type Assoc = U::OtherAssoc; } impl OtherTrait for i32 { type OtherAssoc = <i32 as Trait<i32>>::Assoc; } // forall<T> { i32: Trait<i32, Assoc = T> } ``` - `|- i32: Trait<U, Assoc = U::OtherAssoc>` normalize via impl - (no where clause, output = `<u32 as Trait>::Assoc`) - `|- <u32 as Trait>::Assoc = U::OtherAssoc` eq-via-normalize - `|- u32: Trait<U, Assoc = U::OtherAssoc>` normalize via impl - `|- i32: Trait<Assoc = U::OtherAssoc>` cycle - `|- i32: Trait<i32, Assoc = T>` normalize-via-impl - no where clauses - `|- <u32 as Trait<i32>>::Assoc == T` eq-via-norm - `|- u32: Trait<i32, Assoc = T>` normalize via impl - where-clause `|- i32: Trait<i32, Assoc = <i32 as OtherTrait>::OtherAssoc>`, normalize-via-impl - no where-clauses - `|- <u32 as Trait<i32>>::Assoc = <i32 as OtherTrait>::OtherAssoc`, eq-via-norm - `|- u32: Trait<i32, Assoc = <i32 as OtherTrait>::OtherAssoc>`, normalize-via-impl - `|- i32: Trait<i32, Assoc = ...>` - normalized type eq `|- <i32 as OtherTrait>::OtherAssoc = T` eq-via-nom - `|- i32: OtherTrait<OtherAssoc = T>` norm-via-impl - no where-clauses - `|- <i32 as Trait<i32>>::Assoc = T`, eq-via-norm - `|- i32: Trait<i32, Assoc = T>` -- cycle (at the top) ### failure mode 1: normalize to anything ```rust trait Trait { type Assoc; } impl Trait for u32 { type Assoc = u32::Assoc; } ``` With naive rules we can prove... * `|- forall<T> { u32::Assoc = T }`, via whatevr: * `|- u32::Assoc = T`, via alias-norm: * `|- u32: Trait<Assoc = u32::Assoc>`, via normalize-fallback * `|- u32::Assoc = T`, cycle (coinductively ok?) ...this seems bad. ### associated type bounds cyclic reasoning ```rust trait Trait { type Assoc: Copy; } impl<T: Trait> Trait for T { type Assoc = String; // <T as Trait>::Assoc: Copy } impl<T: Trait> Trait for T { type Assoc = String; // <T as Trait>::Assoc: Copy } fn foo<T: Trait>(y: T::Assoc) -> (T::Assoc, T::Assoc) { (y, y) } fn main() { foo::<u32>(String::from("hello, world")); // double free!! // (u32: Trait) but `(String: Copy)` doesn't hold. } ``` currently proves the following when checking that the impl is correct (proving that the impl is valid) - `|- forall<T> (T: Trait => T::Assoc: Copy)` - `|- T: Trait => T::Assoc: Copy` could this be - `|- forall<T> (T: Trait => String: Copy)` - TODO we also try to prove `T::Assoc: Copy` in `foo` we also prove `u32: Trait` when you call `foo` in `main` ``` trait Tr { type Assoc: Tr_a } substituted impl Tr for T where WC { type Assoc = U1; } A, (T: Trait<Assoc = U>) |- WC A |- U1 = U2 A |- (U1: Tr_a) ------------------------------- normalize-via-impl A |- T: Trait<Assoc = U2> ``` ## "implied bounds" ``` A |- (Ty : Tr_a) trait Tr_a { .. type Assoc : Tr .. } ------------------------------- A |- (Ty::Assoc: Tr) ``` ## "normalization" ``` trait Tr: Tr1 { .. type Assoc : {Tr_a} .. } impl<{X}> Tr for Ty_t where WC { .. type Assoc = Ty_i .. } let S be some substitution for {X} S Ty_t = Ty_s S Ty_i = Ty_a // <-- new A, (Ty_s: Tr) |- S WC A |- (Ty_s: Tr1) A |- (Ty_a: Tr_a) // <-- new ------------------------------- normalize-impl A |- (Ty_s: Tr<Assoc = Ty_a>) ``` ## "normalization fallback" ``` ------------------------------- normalize-fallback A |- (Ty: Tr<Assoc = Ty::Assoc>) ``` ## "equality" ### "reflexive" ``` A |- (Ty_1 = Ty_0) ------------------------------- fallback A |- (Ty_0 = Ty_1) ``` *this can't be interpreted coinductively...* ### "rigid equality" ``` {Ty_0} = {Ty_1} ------------------------------- rigid A |- (S<{Ty_0}> = S<{Ty_1}>) ``` ### "alias equality, base case" ``` A |- T_0 = T_1 ------------------------------- alias-opaque A |- (T_0::Assoc = T_1::Assoc) ``` ### "alias equality, normalized case" ``` A |- (T_0: Tr<Assoc = U0>) A |- U0 = U1 ------------------------------- alias-norm A |- (T_0::Assoc = U1) ``` ## some "fun" examples from [lcnr's notes](https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view) ### ex0 ```rust trait Trait { type Assoc; } impl Trait for () { type Assoc = <()>::Assoc; } ``` With naive rules we can prove... * `|- forall<T> { <u32>::Assoc = T }` * `|- u32::Assoc = T`, via alias-norm: * `|- u32: Trait<Assoc = u32::Assoc>`, via normalize-fallback * `|- u32::Assoc = T`, cycle (coinductively ok?) ...this seems bad. ## Random links * https://hackmd.io/cnX6oA28RwOPfRCTeyLw4Q?view * https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view #### stuff ```rust trait CloneIterator { type Item: Clone; } fn foo<T: CloneIterator<Item = U>, U>(u: U) { u.clone(); } ```

Syntax	Example	Reference
# Header	Header	基本排版
- Unordered List	Unordered List
1. Ordered List	Ordered List
- [ ] Todo List	Todo List
> Blockquote	Blockquote
Bold font	Bold font
Italics font	Italics font
~~Strikethrough~~	~~Strikethrough~~
19^th^	19^th
H~2~O	H₂O
++Inserted text++	Inserted text
==Marked text==	Marked text
[link text](https:// "title")	Link
![image alt](https:// "title")	Image
`Code`	`Code`	在筆記中貼入程式碼
```javascript var i = 0; ```	`var i = 0;`
:smile:		Emoji list
{%youtube youtube_id %}	Externals
$L^aT_eX$	L^aT_eX
:::info This is a alert area. :::	This is a alert area.