Partial negative reasoning via a False trait

language design
1

I have been reading about negative bounds and I think it is possible to get some of its potential without its many complications by just having a special trait. If we declare a trait, let us call it False, so that having a type implementing False is considered an error by the compiler, then we can state that a trait is the negation of another by

impl<T:MyTrait+NotMyTrait> False for T {}

Note that this would not satisfy the excluded middle axiom, this is, adding

impl<T:MyTrait> Foo for T {}
impl<T:NotMyTrait> Foo for T {}

would not implement Foo for every type, but just for the ones that have including one of them. Then, if some crate needs Foo for some type, they should decide if implementing either MyTrait or NotMyTrait. This should be more robust than the typical !MyTrait meaning having not known implementation of MyTrait, where it can change from one implementation to another if some other crate implements the trait. Although it is not evident wether the compiler could detect this is not a case of conflicting implementation.

This also could help to prevent some of the issues found at Unsoundness in `Pin` by adding

impl<'a,T> False for &'a T where &'a T:DerefMut {}
impl<'a,T> False for &'a mut T where &'a mut T:Clone {}

I know that negative bounds and traits have been thought a lot already, and this proposal probably has problems from which I am just unaware, but I have not seen it elsewhere.

2 Likes
2

I'm not particularly clear on rules supporting these kinds of tests but can something like the following be adapted to work for Pin or other cases? Here I've adapted something from static_asserts to test that a particular type Foo is !Send and !Sync.

    // Adapted from static_asserts 1.1.0 `assert_not_impl_any` macro
    // MIT/Apache licensed

    trait AmbiguousIfImpl<A> {
        fn some_f() -> bool { true }
    }
    impl<T: ?Sized> AmbiguousIfImpl<()> for T {}

    #[allow(unused)] struct NotSync;
    impl<T: ?Sized + Sync> AmbiguousIfImpl<NotSync> for T {}

    #[allow(unused)] struct NotSend;
    impl<T: ?Sized + Send> AmbiguousIfImpl<NotSend> for T {}

    #[test]
    fn test_not_send_nor_sync() {
        assert!(<Foo as AmbiguousIfImpl<_>>::some_f());
    }
1 Like
3

Yes it can, but you need to actively inspect the Dubious reference type as assert!(<&dyn Dubious as AmbiguousIfImpl<_>>::some_f()); and it gives the error "cannot infer type" which is not the desired one.

Here is a playground with one of @comex's examples:

Given this, my proposal of a False trait becomes just a trait that should be implicitly checked for all the types, since the check is already possible to do for specific types.

4

Did anyone actually see any problem with this idea? Perhaps @nikomatsakis?

Apparently it seems easy to include it as some axiom in chalk. Reading @aturon's post http://aturon.github.io/blog/2017/04/24/negative-chalk/ I think such axiom would be written forall<T> { compat { not {T:False} } } or compat { not { exists<T> { T: False } } }. Thus, False would be an exception to some coherence rules, but it should not break anything, since we have seen we can force a similar check for any particular type.

5

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.