Lifetime puzzler: How to bypass a generic lifetime?

help
1

I have the following code which insulted my mind:

trait Has<T> {
    fn has(&self, item: &T) -> bool;
}

struct One;
struct Two;
struct Three<'a>(&'a bool);


struct Variants { }

impl Has<One> for Variants {
    fn has(&self, _: &One) -> bool { true }
}

impl Has<Two> for Variants {
    fn has(&self, _: &Two) -> bool { false }
}

impl<'a> Has<Three<'a>> for Variants {
    fn has(&self, &Three(item): &Three) -> bool { *item }
}

struct Checker { }

impl Checker {
    fn check<'a, T: Has<Three<'a>>>(&self, t: &T) -> bool {
        let item = true;
        let three = Three(&item);
        let result = t.has(&three);
        result
    }
}

fn main() {
    let variants = Variants { };
    println!("Has One? {}", variants.has(&One));
    println!("Has Two? {}", variants.has(&Two));
    let item = true;
    println!("Has Three? {}", variants.has(&Three(&item)));
}

The question is: How to implement Checker?

I'll get over it if impossible, friends! But why not? )

1 Like
2

Will this work?

impl Checker {
    fn check<T: for<'a> Has<Three<'a>>>(&self, t: &T) -> bool {
        let item = true;
        let three = Three(&item);
        let result = t.has(&three);
        result
    }
}
2 Likes
3

Excellent! I owe you a beer when I'am in Spb! :beer:

1 Like
4

To explain why this works -

This feature is little documented, but is called "higher ranked lifetimes" or "higher ranked trait bounds." The issue is that when you declare check<'a, T>, that means that the caller of check should be able to insert any lifetime, even 'static for example. This is similar to the issue you may have seen where you want to return an iterator, and you try foo<T: Iterator>() -> T - you can't do this because this says the caller can decide which iterator you return (which is why Rust will soon have the impl Trait feature).

The higher ranked lifetime means that Has<Three<'a>> has to be able to accept any lifetime, but check itself will supply the lifetime to that trait, rather than the caller of check.

If you're interested in reading more about the type theory behind this, both for<'a> and impl Trait are forms of existential type parameters, whereas the lifetime and type parameters introduces in the <...> after a function name are universal type parameters.

5 Likes
5

Thank you for a good explanation! It was a dark corner of my Rust understanding!
It's really poorly documented.

6

When I discovered that, I was a bit disappointed it concerned lifetimes only. In Haskell, that’s called existential quantification and it’s very useful :).

7

TIL that

trait S {}
trait X: S {}

fn foo<T>() where for<> for<> X: S {}

Is apparently a valid Rust. And those fors mean different things!

1 Like
8

Are you sure? I think the normal introduction of a lifetime in Rust is parametric (different from universal because it can be monomorphised, and universally quantified types cannot due to polymorphic recursion), and 'for' introduces a universally quantified lifetime (each instantiation of the function can be passed a different lifetime). Existential quantification would require there is a lifetime but you cannot know what it is. As far a I can tell a Box functions as Rusts equivalent of an existential type.

9

I think you are just using this terminology more precisely (and correctly) than I was. The key distinction is between type parameters which are "input" (determined by the caller) and "output" (determined by this function).

I think this is true, but it has become more common to refer to the impl Trait feature as Rust's 'existential type.' ("Box functions" are called "trait objects" by the way, and don't necessarily need to be boxed (or functions)).

10

There is something odd about Rust syntax, in that lifetimes are type level objects (like "int32" is a type level object, similar to concepts like type level names, there is an infinite supply of fresh ones and they are locally scoped) and are not variables, yet they get introduced along with type-variables. Really 'forall' is the wrong notation because you are not introducing a variable. Really instead of 'forall' it should simply be introducing a parametric lifetime variable.

11

No, 'a is a lifetime variable, and is a type parameter of the kind lifetime. Its somewhat confusing because the few concrete lifetimes that can be named are named using the same syntactic appearance (exmaples of concrete lifetimes are 'static and the lifetimes that can be applied to loops). But fn foo<'a> is parameteric over all lifetimes, and each instantiation will apply it to a concrete lifetime.

for is used to introduce a higher rank parameter, its incidental that you can only introduce higher rank lifetimes right now and not type parameters.

12

That makes sense, there is something odd about the syntax, but it wasn't what I thought :slight_smile: I still find Haskell's type notation cleaner, but I realise the syntax is designed to appeal to C++ and Java programmers.

13

I have to ask what does that mean?

14

I have do admit that I know the difference only on the syntactic level :slight_smile:

Syntactically, you can specify a where bound for any type, like where TYPE: BOUNDS. You can also specify an for bound (which I guess roughly means an infinite number of bounds), like where for<lifetimes> TYPE: BOUNDS. And the type itself can be a for-type. So in where for<> X: S the for is a part of the where clause and in where (for<> X): S the for is a part of type.

I do not know what is the difference between two cases though (perhaps they are equvalent? Then maybe we don't need one of them?), would be glad to learn it!

And if you actually try to specify lifetimes in fors in both positions, you would get an error. Here's the relevant comment in the compiler source code: https://github.com/rust-lang/rust/commit/8122ce81d0909bed39c6df3e47bc751851bded84#diff-9694c2dab1b4140752e569e4b1ba58c4R57

15

Thanks. So it seems that rust allows to include universal like quantifier anywhere in the whereclause and that is kind of effectively creating a new type on the fly and the rest of whereclause bounds/reasoning is applied to that new type. However the new type has to be related to some known type parameter. And as of now the quantifier only supports lifetimes as a parameter.
Thanks again.