Skip to content

Commit

Permalink
Shrink the scope of the associated const changes to RFC 195, and ment…
Browse files Browse the repository at this point in the history 
…ion trait objects.
  • Loading branch information
@quantheory
quantheory committed May 28, 2015
1 parent 1ad497d commit 992550b
Showing 1 changed file with 22 additions and 145 deletions.
167 changes: 22 additions & 145 deletions text/0195-associated-items.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -882,6 +882,7 @@ trait Foo<Input1, Input2> {
type Output1;
type Output2;
lifetime 'a;
const C: bool;
...
}
```
Expand All @@ -894,6 +895,7 @@ T: Foo<I1, I2, Output1 = O1>
T: Foo<I1, I2, Output2 = O2>
T: Foo<I1, I2, Output1 = O1, Output2 = O2>
T: Foo<I1, I2, Output1 = O1, 'a = 'b, Output2 = O2>
T: Foo<I1, I2, Output1 = O1, 'a = 'b, C = true, Output2 = O2>
```

The output constraints must come after all input arguments, but can appear in
Expand Down Expand Up @@ -954,20 +956,21 @@ trait Foo<Input1, Input2> {
type Output1;
type Output2;
lifetime 'a;
const C: bool;
...
}
```

Unlike the case for static trait bounds, which do not have to specify any of the
associated types or lifetimes (but do have to specify the input types), trait
object types must specify all of the types:
associated types, lifetimes, or consts, (but do have to specify the input types),
trait object types must specify all of the types:

```rust
fn consume_foo<T: Foo<I1, I2>>(t: T) // this is valid
fn consume_obj(t: Box<Foo<I1, I2>>) // this is NOT valid

// but this IS valid:
fn consume_obj(t: Box<Foo<I1, I2, Output1 = O2, Output2 = O2, 'a = 'static>>)
fn consume_obj(t: Box<Foo<I1, I2, Output1 = O2, Output2 = O2, 'a = 'static, C = true>>)
```

With this design, it is clear that none of the non-`Self` types are erased as
Expand Down Expand Up @@ -1199,70 +1202,10 @@ clauses, it is probably too much of a hack to be viable for use in `libstd`.

### Associated consts in generic code

There are some restrictions on uses of associated consts in generic code. These
might be loosened or removed in the future (see the related sub-sections in
"Unresolved questions" below).

1. Values of constant expressions in match patterns cannot depend on a type
parameter (by extension, neither can the types of such expressions). This
restriction is necessary for exhaustiveness and reachability to be checked
in generic code.

Note that the dependence of a value on a type parameter may be indirect:

```rust
enum MyEnum {
Var1,
Var2,
}
trait HasVar {
const VAR: MyEnum;
}
fn do_something<T: HasVar>(x: MyEnum) {
const y: MyEnum = <T>::VAR;
// The following is forbidden because the value `y` depends on `T`.
match x {
y => { /* ... */ }
_ => { /* ... */ }
}
// However, this is OK because the guard is not a part of the pattern.
match x {
z if z == y => { /* ... */ }
_ => { /* ... */ }
}
}
```

2. Array sizes that depend on type parameters cannot be compared for equality
by type-checking, with one exception: if the expression for an array size
comprises only a single reference to a constant item (or associated item),
it will be considered equal to any other array size that refers to the same
item, even if that item itself depends on the type parameters.

For clarification, here are some examples. Assume that `T` is a type
parameter in the outer scope, and that it is known to have an associated
const `<T>::N` of type `usize`.

```rust
// This is OK (but there are limitations to how x can be used).
let x: [u8; <T>::N] = [0u8; <T>::N];
// Equivalent to the above.
let x = [0u8; <T>::N];
// Neither of the following are allowed (type checking shouldn't have to
// know anything about arithmetic).
let x: [u8; 2 * <T>::N] = [0u8; <T>::N + <T>::N];
let x: [u8; <T>::N + 1] = [0u8; 1 + <T>::N];
// Still not allowed.
let x: [u8; <T>::N + 1] = [0u8; <T>::N + 1];
// Workaround for the expression above.
const N_PLUS_1: usize = <T>::N + 1;
let x: [u8; N_PLUS_1] = [0u8; N_PLUS_1];
// Neither of the following are allowed.
const ALIAS_N_PLUS_1: usize = N_PLUS_1;
let x: [u8; N_PLUS_1] = [0u8; ALIAS_N_PLUS_1];
const ALIAS_N: usize = <T>::N;
let x: [u8; <T>::N] = [0u8; ALIAS_N];
```
If the value of an associated const depends on a type parameter (including
`Self`), it cannot be used in a constant expression. This restriction will
almost certainly be lifted in the future, but this raises questions outside the
scope of this RFC.

# Staging

Expand Down Expand Up @@ -1471,97 +1414,31 @@ on implementation concerns, which are not yet clear.
## Generic associated consts in match patterns

It seems desirable to allow constants that depend on type parameters in match
patterns, but it's not clear how to do so.

Looking at the `HasVar` example above, one possibility would be to simply treat
the first, forbidden match expression as syntactic sugar for the second, allowed
match expression that uses a pattern guard. This is simple to implement because
one can simply ignore the constant when performing exhaustiveness and
reachability checks. Unfortunately, this approach blurs the difference between
match patterns (which provide strict checks) and pattern guards (which are just
useful syntactic sugar), and it does not increase the expressiveness of the
language.

An alternative would be to allow `where` clauses to place constraints on
associated consts. If an associated const is known to be equal/unequal to some
other value (or in the case of integers, inside/outside a given range), this can
inform exhaustiveness and reachability checks. But this requires more design and
implementation work, and more syntax.
patterns, but it's not clear how to do so while still checking exhaustiveness
and reachability of the match arms. Most likely this requires new forms of
where clause, to constrain associated constant values.

For now, we simply defer the question.

## Generic associated consts in array sizes

The above solution for type-checking array sizes is somewhat unsatisfactory. In
particular, it is counter-intuitive that neither of the following will type
check:
It would be useful to be able to use trait-associated constants in generic code.

```rust
// Shouldn't this be OK?
const ALIAS_N: usize = <T>::N;
let x: [u8; <T>::N] = [0u8; ALIAS_N];
// This is likely to yield an embarrassing error message such as:
// "couldn't prove that `<T>::N + 1` is equal to `<T>::N + 1`"
let x: [u8; <T>::N + 1] = [0u8; <T>::N + 1];
```

A function like this is especially affected:

```rust
trait HasN {
const N: usize;
}
fn foo<T: HasN>() -> [u8; <T>::N + 1] {
// Can't be verified to be correct for the return type, and can't use the
// intermediate const workaround due to scoping issues.
[0u8; <T>::N + 1]
}
// Or...
let x: [u8; T::N + 1] = [0u8; T::N + 1];
```

This can be worked around with type-level naturals that use associated consts to
produce array sizes, but this is syntactically a bit inelegant.
However, this causes some problems. What should we do with the following case in
type checking, where we need to prove that a generic is valid for any `T`?

```rust
// Assume that `TypeAdd` and `One` are from a type-level naturals or similar
// library, and that `NAsTypeNatN` provides some way of translating the `N`
// on a `HasN` to a type compatible with that library.
trait HasN {
const N: usize;
type TypeNatN;
}
fn foo<T: HasN>() -> [u8; TypeAdd<<T>::TypeNatN, One>::AsUsize] {
// Because the type `TypeAdd<<T>::TypeNatN, One>` can be verified to be
// equal to itself in type checking, we know that the associated const
// `AsUsize` below must be the same item as the `AsUsize` mentioned in the
// return type above.
[0u8; TypeAdd<<T>::NAsTypeNat, One>::AsUsize]
}
let x: [u8; T::N + T::N] = [0u8; 2 * T::N];
```

There are a variety of possible ways to address the above issues, including:

- Implementing smarter handling of consts that are just aliases of other
constant items.
- Allowing `where` clauses to constrain some associated constants to be equal,
to other expressions, and using this information in type checking.
- Adding normalization with little or no awareness of arithmetic (e.g. allowing
expressions that are exactly the same to be considered equal, or using only
a very basic understanding of which operations are commutative and/or
associative).
- Adding new syntax and/or new capability to plugins to allow type-level
naturals to be used with more ergonomic and clear syntax.
- Implementing a dependent type system that provides built-in semantics for
integer arithmetic at the type level, rather than implementing this in an
external or standard library.
- Using a full-fledged SMT solver.
- Some other creative solutions not on this list.

While there are many ways to improve on the current design, and many of these
approaches are not mutually exclusive, much more work is needed to investigate
and implement a self-consistent, effective, and ideally intuitive set of
solutions.

Though admittedly not very satisfying at the moment, the current approach has
the advantage of being (arguably) a good minimalist design, allowing associated
consts to be used for array sizes in generic code now, but also allowing for any
of a number of improved systems to be implemented later.
We would like to handle at least some obvious cases (e.g. proving that
`T::N == T::N`), but without trying to prove arbitrary statements about
arithmetic. The question of how to do this is deferred.

0 comments on commit 992550b

Please sign in to comment.