@@ -8,21 +8,21 @@ Cleanup the trait, method, and operator semantics so that they are
8
8
well-defined and cover more use cases. A high-level summary of the
9
9
changes is as follows:
10
10
11
- 1 . Full support for proper generic traits ("multiparameter type classes"),
12
- including a simplified version of functional dependencies that may
13
- evolve into associated types in the future.
14
- 2 . Generalize explicit self types beyond ` &self ` and ` &mut self ` etc,
11
+ 1 . Generalize explicit self types beyond ` &self ` and ` &mut self ` etc,
15
12
so that self-type declarations like ` self: Rc<Self> ` become possible.
16
- 3 . Expand coherence rules to operate recursively and distinguish
13
+ 2 . Expand coherence rules to operate recursively and distinguish
17
14
orphans more carefully.
18
- 4 . Revise vtable resolution algorithm to be gradual.
19
- 5 . Revise method resolution algorithm in terms of vtable resolution.
15
+ 3 . Revise vtable resolution algorithm to be gradual.
16
+ 4 . Revise method resolution algorithm in terms of vtable resolution.
17
+
18
+ This RFC excludes discussion of associated types and multidimensional
19
+ type classes, which will be the subject of a follow-up RFC.
20
20
21
21
# Motivation
22
22
23
23
The current trait system is ill-specified and inadequate. Its
24
- implementation dates from a rather different language. I want to clean
25
- it up and put it on a surer footing.
24
+ implementation dates from a rather different language. It should be
25
+ put onto a surer footing.
26
26
27
27
## Use cases
28
28
@@ -190,73 +190,6 @@ property. And the popularity and usefulness of blanket impls cannot
190
190
be denied. Therefore, I think this property ("always being able to
191
191
add impls") is not especially useful or important.
192
192
193
- ### Overloadable operators
194
-
195
- * Addressed by:* Proper generic traits.
196
-
197
- Our current rules around operator overloading are too limiting.
198
- Consider the case of defining a mathematical library for modeling
199
- vectors. I might like to overload the ` + ` operator. Following mathematical
200
- convention, I'd like to say that:
201
-
202
- 1 . Vector + vector yields a vector.
203
- 2 . Vector + scalar yields a vector.
204
- 3 . Scalar + vector yields a vector.
205
-
206
- Given that the trait for addition looks like:
207
-
208
- ```
209
- trait Add<RHS,SUM> { ... }
210
- ```
211
-
212
- where ` RHS ` is the type of the right-hand-side argument and ` SUM ` is
213
- the type of their sum. One might then imagine translating the three
214
- kinds of addition for vectors into impls like so (note that the type
215
- after the ` for ` is the left-hand-side of the addition):
216
-
217
- ```
218
- impl Add<Vector, Vector> for Vector { ... }
219
- impl Add<Scalar, Vector> for Vector { ... }
220
- impl Add<Vector, Vector> for Scalar { ... }
221
- ```
222
-
223
- Of course, if you do this, you'll get...well, it won't work. You'll
224
- get some coherence failures, I think, but in addition the algorithms
225
- and trait matching are just not up to the task of resolving these
226
- sorts of traits (see "Insufficient implementation").
227
-
228
- I think however that this sort of impl * should* work, though not
229
- necessarily for * every* trait. Basically, trait type parameters can be
230
- divided into two groups: inputs and ouputs. An * input* type parameter
231
- is one that is used to decide what impl applies. An * output* type
232
- parameter is one that is determined by the impl. In the case of the
233
- ` Add ` trait, the * inputs* would be the implicit type parameter ` Self `
234
- as well as ` RHS ` . The * output* would be the type ` SUM ` .
235
-
236
- In Haskell, the distinction between * input* and * output* type
237
- parameters can be expressed in two mostly equivalent ways. One is
238
- * functional dependencies* , in which one declares an expression like `A
239
- B -> C D` , which means that the type parameters ` A` and ` B` uniquely
240
- determine ` C ` and ` D ` . In other words, ` A ` and ` B ` are inputs, and ` C `
241
- and ` D ` are outputs. (Functional dependencies are more general than
242
- this, though I know of no actual use case for their full generality.)
243
- * Asssociated types* are another means of drawing this distinction:
244
- here the * associated types* are outputs.
245
-
246
- In this proposal, I specify that the implicit type parameter ` Self `
247
- is, by default, the only input type parameters. All explicit type
248
- parameters on a trait default to * output* unless prefixed by the ` in `
249
- keyword. This means that, e.g., the trait ` Add ` should be defined as:
250
-
251
- ```
252
- trait Add<in RHS, SUM> { ... }
253
- ```
254
-
255
- The decision to make * output* be the default is data-driven: a quick
256
- look over existing traits, as well as existing practice from Haskell,
257
- shows that output type parameters are * much* more common. I have
258
- further discussion on the interaction with * associated types* below.
259
-
260
193
### Hokey implementation <a name =hokey >
261
194
262
195
* Addressed by:* Gradual vtable resolution algorithm
@@ -296,11 +229,10 @@ some other reason.
296
229
297
230
Note that there is some interaction with the distinction between input
298
231
and output type parameters discussed in the previous
299
- example. Specifically, we must never * infer* the value of an input
232
+ example. Specifically, we must never * infer* the value of the ` Self `
300
233
type parameter based on the impls in scope. This is because it would
301
234
cause * crate concatentation* to potentially lead to compilation errors
302
- in the form of inference failure. (I am not 100% convinced this is a
303
- big deal, though, see the * Alternatives* section for more details.)
235
+ in the form of inference failure.
304
236
305
237
## Properties
306
238
@@ -338,17 +270,6 @@ like to write out a declarative and non-algorithmic specification for
338
270
the rules too, but that is work in progress and beyond the scope of
339
271
this RFC. Instead, I'll try to explain in "plain English".
340
272
341
- ## Trait syntax
342
-
343
- Use the ` in ` keyword to designate * input* type parameters \[ [ 1] ( #1 )] :
344
-
345
- trait Add<in RHS, SUM> { ... }
346
-
347
- The implicit ` Self ` type parameter is * always* considered an input.
348
- All explicit type parameters are considered outputs unless declared as
349
- inputs. Input type parameters must come * before* explicit type
350
- parameters. \[ [ 3] ( #3 )]
351
-
352
273
## Method self-type syntax
353
274
354
275
Currently methods must be declared using the explicit-self shorthands:
@@ -383,9 +304,8 @@ and the *overlapping implementations* restriction.
383
304
the following conditions:
384
305
385
306
1 . The trait being implemented (if any) must be defined in the current crate.
386
- 2 . At least one of the input type parameters (including but not
387
- necessarily ` Self ` ) must meet the following grammar, where ` C `
388
- is a struct or enum defined within the current crate:
307
+ 2 . The ` Self ` type parameter must meet the following grammar, where
308
+ ` C ` is a struct or enum defined within the current crate:
389
309
390
310
T = C
391
311
| [T]
@@ -396,12 +316,13 @@ the following conditions:
396
316
| (..., T, ...)
397
317
| X<..., T, ...> where X is not bivariant with respect to T
398
318
399
- * Overlapping instances* : No two implementations can be instantiable
400
- with the same set of types for the input type parameters. For this
401
- purpose, we will also recursively check bounds. This check is
402
- ultimately defined in terms of the * RESOLVE* algorithm discussed in
403
- the implementation section below: it must be able to conclude that the
404
- requirements of one impl are incompatible with the other.
319
+ * Overlapping instances* : No two implementations of the same trait can
320
+ be defined for the same type (note that it is only the ` Self ` type
321
+ that matters). For this purpose of this check, we will also
322
+ recursively check bounds. This check is ultimately defined in terms of
323
+ the * RESOLVE* algorithm discussed in the implementation section below:
324
+ it must be able to conclude that the requirements of one impl are
325
+ incompatible with the other.
405
326
406
327
Here is a simple example that is OK:
407
328
@@ -413,17 +334,6 @@ The first impl implements `Show for int` and the case implements
413
334
` Show for uint ` . This is ok because the type ` int ` cannot be unified
414
335
with ` uint ` .
415
336
416
- Here is another example that is OK under these rules:
417
-
418
- trait Add<in RHS, SUM> { ... }
419
- impl Add<int, int> for int { ... }
420
- impl Add<Vector, Vector> for int { ... }
421
-
422
- It might seem surprising that these two impls are ok, because both
423
- implement ` Add ` for ` int ` . However, the type ` RHS ` is different in
424
- each case, and ` RHS ` is an input type parameter.
425
-
426
- Note that it is crucial for ` RHS ` to be an input type parameter.
427
337
The following example is * NOT OK* :
428
338
429
339
trait Iterator<E> { ... }
@@ -448,10 +358,20 @@ might add an implementation of `Copy` for `~B`.)
448
358
449
359
Since trait resolution is not fully decidable, it is possible to
450
360
concoct scenarios in which coherence can neither confirm nor deny the
451
- possibility that two impls are overlapping. I know of no examples that
452
- do not involve infinite recursion between impls. For example, in the
453
- following scenario, the coherence checked would be unable to decide if
454
- the following impls overlap:
361
+ possibility that two impls are overlapping. One way for this to happen
362
+ is when there are two traits which the user knows are mutually
363
+ exclusive; mutual exclusion is not currently expressible in the type
364
+ system \[ [ 7] ( #7 ) \] however, and hence the coherence check will report
365
+ errors. For example:
366
+
367
+ trait Even { } // Naturally can't be Even and Odd at once!
368
+ trait Odd { }
369
+ impl<T:Even> Foo for T { }
370
+ impl<T:Odd> Foo for T { }
371
+
372
+ Another possible scenario is infinite recursion between impls. For
373
+ example, in the following scenario, the coherence checked would be
374
+ unable to decide if the following impls overlap:
455
375
456
376
impl<A:Foo> Bar for A { ... }
457
377
impl<A:Bar> Foo for A { ... }
@@ -676,14 +596,17 @@ resolution. If, after type checking the function in its entirety,
676
596
there are * still* obligations that cannot be definitely resolved,
677
597
that's an error.
678
598
679
- ## Ensuring crate concatenation through functional dependencies
599
+ ## Ensuring crate concatenation
600
+
601
+ To ensure * crate concentanability* , we must only consider the ` Self `
602
+ type parameter when deciding when a trait has been implemented (more
603
+ generally, we must know the precise set of * input* type parameters; I
604
+ will cover an expanded set of rules for this in a subsequent RFC).
680
605
681
- It depends. The distinction between * input* and * output* type
682
- parameters is necessary to ensure that inference is stable even if
683
- crates are concatenated. That is, imagine a scenario like this one:
606
+ To see why this matters, imagine a scenario like this one:
684
607
685
608
trait Produce<R> {
686
- fn produce(self: Self) -> R;
609
+ fn produce(& self: Self) -> R;
687
610
}
688
611
689
612
Now imagine I have two crates, C and D. Crate C defines two types,
@@ -694,19 +617,28 @@ Now imagine I have two crates, C and D. Crate C defines two types,
694
617
695
618
Now imagine crate C has some code like:
696
619
697
- fn foo(v: Vector) {
698
- let x = v.produce();
699
- ...
620
+ fn foo() {
621
+ let mut v = None;
622
+ loop {
623
+ if v.is_some() {
624
+ let x = v.get().produce(); // (*)
625
+ ...
626
+ } else {
627
+ v = Some(Vector);
628
+ }
629
+ }
700
630
}
701
631
702
- At this point we don't know the type of ` x ` . But the inferencer might
703
- conclude that, since it can only see one ` impl ` of ` Produce ` for
704
- ` Vector ` , ` x ` must have the type ` int ` .
632
+ At the point ` (*) ` of the call to ` produce() ` we do not yet know the
633
+ type of the receiver. But the inferencer might conclude that, since it
634
+ can only see one ` impl ` of ` Produce ` for ` Vector ` , ` v ` must have type
635
+ ` Vector ` and hence ` x ` must have the type ` int ` .
705
636
706
637
However, then we might find another crate D that adds a new impl:
707
638
639
+ struct Other;
708
640
struct Real;
709
- impl Combine<Real> for Vector { ... }
641
+ impl Combine<Real> for Other { ... }
710
642
711
643
This definition passes the orphan check because * at least one* of the
712
644
types (` Real ` , in this case) in the impl is local to the current
@@ -743,11 +675,11 @@ is four sets:
743
675
recursion.
744
676
745
677
In general, if we ever encounter a NO-IMPL or UNDECIDABLE, it's
746
- probably an error. DEFERRED obligations are ok until we reach the end
678
+ probably an error. DEFERRED obligations are ok until we reach the end
747
679
of the function. For details, please refer to the
748
680
[ prototype] [ prototype ] .
749
681
750
- # Alternatives <a name =alternatives >
682
+ # Alternatives and downsides <a name =alternatives >
751
683
752
684
## Autoderef and ambiguity <a name =ambig >
753
685
@@ -773,77 +705,6 @@ that are not smart pointers.
773
705
This idea appeals to me but I think belongs in a separate RFC. It
774
706
needs to be evaluated.
775
707
776
- ## What are the downsides to fundeps? <a=fundepdownsides>
777
-
778
- There is one place where a strict concern about fundeps will limit
779
- inference. One scenario I am envisioning is the following:
780
-
781
- struct MyIterator<E> {
782
- }
783
-
784
- impl<E:Copy> Iterator<E> for MyIterator<E> {
785
- fn next(&self) -> Option<E> { ... }
786
- }
787
-
788
- ...
789
-
790
- let i: MyIterator<_> = ...;
791
- i.next();
792
-
793
- Note that I wrote ` MyIterator<_> ` for the type of ` i ` -- let's say
794
- that the type inference hasn't yet settled on what type we are
795
- iterating over, and hence (from it's point of view) the type of ` i ` is
796
- ` MyIterator<$0> ` , where ` $0 ` represents an inference variable. In that
797
- case, we won't be able to decide whether ` MyIterator<$0> ` implements
798
- ` Iterator ` because we don't know whether ` $0 ` implements ` Copy ` .
799
-
800
- One way to address this would be by allowing the definition of
801
- ` MyIterator ` to declare bounds of its own:
802
-
803
- struct MyIterator<E:Copy> { ... }
804
-
805
- Then we might adjust the algorithm to understand that we can match the
806
- impl, since if there is a value of type ` MyIterator<$0> ` , then ` $0 `
807
- must be ` Copy ` . This basically relies on some other pull requests that
808
- are in the pipeline.
809
-
810
- ## How do functional dependencies and associated types relate? <a name =assoc >
811
-
812
- An * associated type* is basically an "output" functional dependency. I
813
- expect we will eventually add some sort of syntax for associated
814
- types. Associated types have a lot of advantages over fundeps, but I
815
- do have some concrete concerns too. I think we may want both in the
816
- end.
817
-
818
- My usual example for where a fundep may be more appropriate
819
- is the ` Iterator ` trait:
820
-
821
- trait Iterator<E> { ... }
822
-
823
- It is common to want to write a function that takes an iterator of
824
- some specific type, e.g. char. With a fundep-style approach, this can
825
- easily be expressed:
826
-
827
- fn foo<I:Iterator<Char>>(...) { ... }
828
-
829
- If using associated types, the equivalent would require some sort
830
- of ` where ` clause:
831
-
832
- trait Iterator { type E; }
833
- fn foo<I:Iterator>(...) where I::E == Char { ... }
834
-
835
- Past experience also suggests that it's harder to figure out how to
836
- integrate this substitution into the type system rules themselves.
837
-
838
- Moreover, it's not clear how associated types integrate with object
839
- types. For example, an object type like ` &Iterator<char> ` works fine,
840
- but for traits using associated types that doesn't work at all.
841
-
842
- ## Why functional dependencies and not traits implemented over tuples? <a name =tuples >
843
-
844
- All things being equal, I might prefer to say that only the ` Self `
845
- type of a trait is
846
-
847
708
# Footnotes
848
709
849
710
<a name =1 >
@@ -885,4 +746,9 @@ to this rule.
885
746
discuss alternate rules that might allow us to lift the requirement
886
747
that the receiver be named ` self ` .
887
748
749
+ <a name =7 >
750
+
751
+ ** Note 7:** I am considering introducing mechanisms in a subsequent
752
+ RFC that could be used to express mutual exclusion of traits.
753
+
888
754
[ prototype ] : https://github.com/nikomatsakis/trait-matching-algorithm
0 commit comments