# 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<I>(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<U>; }
A, T: Trait<Assoc = S<U>> |- WC
------------------------------- normalize-via-impl
A, later(T: Trait<Assoc = S<U>>) |- T: Trait<Assoc = S<U>>
```
```
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<U> {
type Assoc;
}
impl<U: OtherTrait> Trait<U> for i32 {
type Assoc = <u32 as Trait<U>>::Assoc;
}
impl<U: OtherTrait> Trait<U> 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<U>>::Assoc`)
- `|- <u32 as Trait<U>>::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();
}
```
Sign in with Wallet
Connect another wallet