Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Draft] RFC: Generalized Type Ascription #8

Closed
wants to merge 32 commits into from

Conversation

Centril
Copy link
Owner

@Centril Centril commented Aug 7, 2018

This is a draft version of an RFC for you to review, before a formal proposal is made for consideration.

Summary

This RFC supersedes and subsumes RFC 803. We finalize a general notion of type ascription uniformly in patterns, expressions, let bindings, and fn definitions. You may now for example write:

let x = (0..10).collect() : Vec<_>;

do_stuff(try : Option<u8> { .. });

do_stuff(async : u8 { .. });

do_stuff(unsafe : u8 { .. });

do_stuff(loop : u8 { .. });

let alpha: u8 = expr;
    ^^^^^^^^^

let [x: u8, y, z] = stuff();
    ^^^^^^^^^^^^^

if let Some(beta: u8) = expr { .. }
            ^^^^^^^^

fn foo(Wrapping(alpha: usize)) {}
       ^^^^^^^^^^^^^^^^^^^^^^

Here, the underlined bits are patterns. Note however that this RFC does not introduce global type inference.

Finally, we lint (warn-by-default) when a user writes Foo { $field: $ident : $type } and the compiler instead suggests: Foo { $field: ($ident : $type) }.

and let's us easily constrain the type of `elems` in a syntactically
light-weight way in any case.

6. Type ascription is helpful when doing *type* driven development (TDD)
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: When I google "TDD" I get test driven development, as I expected, so I would discourage this abbreviation.

(that `expr : Option<?T>` for some `?T`).
Because the annotation is more local, we can employ more local reasoning.
This is particularly useful if the `enum` contains many variants in which
case the type ascription on `expr` may not be immediately visible.

This comment was marked as resolved.

This comment was marked as resolved.

This comment was marked as resolved.

```

This also gives the compiler an opportunity to tell you what the types are
if it so happens that you need this help.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this would be hard right now unless it's a trait impl, so you might want to have the code example explicitly be such, or change the error to just say that you need types, without suggesting them. (Especially since diagnostic quality is something that doesn't need RFCing -- people will just make it better even if the RFC doesn't say so, in the cases that are feasible.)

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nuanced the language a bit here to make it optional :)

Copy link

@nrc nrc left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Big 👍 from me!

It's probably worth discussing the implementation status of rust-lang#803 in more detail, iirc, non-coercing ascription is implemented, but coercions are not. (As an alternative design, it might be worth considering different ways that coercion and ascription interact. Some people have wanted to keep ascription meaning no coercion, and only coerce with as, however, this doesn't work for some coercions from fixed size to dynamically sized types).

6. Type ascription is helpful when doing *type* driven development (TDD)
and opens up more possibilities to move in the direction of
interactive development as is possible with [agda-mode] and [idris-mode].

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ANother benefit (which I don't think was ni 803) is that when you get a gnarly type error, type ascription can quickly help you understand and narrow down the error.


[RFC 1685]: https://github.com/rust-lang/rfcs/blob/master/text/1685-deprecate-anonymous-parameters.md

#### [RFC 1685] and deprecation schedule

This comment was marked as resolved.

This comment was marked as resolved.


# Possible future work
[possible future work]: #possible-future-work

This comment was marked as resolved.

This comment was marked as resolved.

match expr {
None => logic,
Some(vec: Vec<u8>) => logic,
}

This comment was marked as resolved.

This comment was marked as resolved.

This comment was marked as resolved.


Instead, we propose that whenever type ascription is followed by a
field projection or a method call, the projections or the call should apply
to the entire ascribed expression.

This comment was marked as resolved.

This comment was marked as resolved.

```

Do note however that in this case, you are annotating the inner type of the
resulting future and not the future itself. Thus, this is equivalent to:

This comment was marked as resolved.

This comment was marked as resolved.

This comment was marked as resolved.

### In macros

Just as we noted before that type ascription work in expression macros so may
you use type ascription in pattern macros. For example:

This comment was marked as resolved.

This comment was marked as resolved.

`ref (x : T)` instead of `(ref x) : T`. The same applies to `ref mut`, `&`,
and `&mut`.

The grammar of `let` bindings is changed from:

This comment was marked as resolved.

This comment was marked as resolved.


// A type variable is induced by `impl Display`
// and then `typeof(x)` is that variable.
// The type of `g3: for<T: Display> fn(Wrapping<T>) -> ()`.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The function names in the comments are all incorrect :)

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for spotting this! Fixed :)

@kennytm
Copy link

kennytm commented Aug 7, 2018

The issue currently blocking type ascription (rust-lang/rust#23416) is soundness issue when coercion happens:

Ensure soundness with respect to ref positions:

  • let ref x = <expr> / let mut ref = <expr>
  • match <expr>: Type { ref x => ... }
  • (<expr>: Type).method_with_ref_self()

The issue is elaborated in rust-lang#803 (comment) and rust-lang/rust#23416 (comment). It seems this RFC did not address this issue (can't find the word "sound" and this RFC does support coercion).

Thus, we believe it is reasonable to expedite the schedule.

# Prior art
[prior-art]: #prior-art

This comment was marked as resolved.

This comment was marked as resolved.


This entails for example that a Rust compiler will interpret `ref x : T` as
`ref (x : T)` instead of `(ref x) : T`. The same applies to `ref mut`, `&`,
and `&mut`.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are you certain it's the same between ref and &? In

let &x : &i32 = &0;

the x is an i32, so I think the parse is let (&x) : &i32, not let &(x: &i32).

fn display_all(elems: impl Iterator<Item: Display>) { ... }
```

As of today (2018-08-06), it is not possible to use turbofish at all
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Still true as of 2018-08-07 😁

.into() : Rc<[_]>;
```

To that end, `foo : bar.quux()` and `foo : bar.quux` should unambiguously be

This comment was marked as resolved.

This comment was marked as resolved.

.into() : Rc<[_]>;
```

We suggest instead that you should be able to write:

This comment was marked as resolved.

This comment was marked as resolved.

```rust
fn foo<T>(Wrapping(value: T)) -> usize { ... }

fn bar(Wrapping(value: usize)) -> usize { ... }
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While I really like this feature, it might be worth scoping it down initially to avoid needing to specify all the details. For example, there are no examples of lifetimes, thus far. (And I think it'd work fine, but there are a bunch of questions around things like lifetime elision if you have Foo { x: x: &i32, y: y: &i32 } and it's Foo<'_>.)

Maybe start with just the "no generics" case? (Like Quux below.)

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

...or you could just define the full unification algorithm 🤣

Type ascription is useful. A motivation for the feature is noted in the merged,
but thus far not stabilized, [RFC 803][RFC_803_motivation] which introduces
type ascription in expression contexts as `expr : T`. We reinforce that RFC
with more motivation:

This comment was marked as resolved.


However, if you write this on a single line, or simply consider `x : T.foo()`
a user might parse this as `x : (T.foo())` instead.
While Rust does not have any "type level methods", and wherefore this parse
Copy link

@varkor varkor Aug 7, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"wherefore" isn't quite right here ("therefore" is closer, but still awkward). Maybe rephrase to something like: "While at this stage Rust does not support type-level methods (meaning this parse currently makes no sense), a user may nonetheless make this mistake."

// c) this entails that `'?c = 'a` and so `'?c` is substituted for `'a`.
//
// 4) Thus, `good_11 : for<'a> fn(Wibble<'a>) -> ()`.
fn good_11(Wibble(x: &i32, y: Bar<'_>)) {}
Copy link

@scottmcm scottmcm Aug 8, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wow, this section is awesome!

I think I agree with all of them except for good_11: I would expect that

fn good_11(Wibble(x: &i32, y: Bar<'_>)) {}

is equivalent to

fn good_11(Wibble(x: &'_ i32, y: Bar<'_>)) {}

is equivalent to

fn good_11<'a, 'b>(Wibble(x: &'a i32, y: Bar<'b>)) {}

Which is illegal since it, unlike Wibble, doesn't require that 'a == 'b.

That's because the version not wrapped in Wibble:

fn rutabaga(x: &i32, y: Bar<'_>) {}

would have two lifetimes, so I think the wrapped version should too.

This helps local reasoning, as you don't need to look at the declaration of Wibble to know whether the two lifetimes are the same or different (since Product and Wibble cases look the same in the function header).

--

So maybe then there's

fn good_11<'a>(Wibble(x: &'a i32, y: Bar<'a>)) {}

and

fn bad_4(Wibble(x: &i32, y: Bar<'_>)) {} //~ ERROR insufficiently constrained

Copy link
Owner Author

@Centril Centril Aug 8, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Glad you think so :)

I agree that good_11 is the tricky one. The rule you imposed certainly does improve local reasoning and the expectation induced by rutabaga does seem like it would happen to folks sometimes.

However, I do wonder if people care and think so much about lifetime parameters (if you are dealing with unsafe code where this is important you should quantify explicitly) that it matters in practice. I mostly don't think about them that much personally.

  • At the call site good_11 won't be callable with something where given &'a i32 and Bar<'b> you have that 'a != 'b because you won't be able to construct such a Wibble<'?> in the first place.

  • What remains is then confusion at the definition site of good_11 where the user may think that 'a != 'b. However, when the user actually tries to make use of this mistaken belief, the compiler should be able to give the user the actual signature of the function and/or say that the lifetimes are really the same. Thus, the user can therefore "learn on the job".

In any case, it is also true that your proposed rule allows strictly less than my rule so if we use your rule and then change our minds we can switch. So we are forward compatible.

Finally and as an aside, there are two ways to make your changed good_11 shorter:

// in-band lifetimes (assuming we don't ditch it)
fn good_11(Wibble(x: &'a i32, y: Bar<'a>)) {}

// The types are fully determined by `Wibble<'_>` itself.
fn good_11(Wibble(x, y)) {}

EDIT: Perhaps the last one is so ergonomic that fn good_11(Wibble(x: &i32, y: Bar<'_>)) simply doesn't occur for it to matter?

I'll go and add an unresolved question for now; I think this is something which is subtle and where we'll want to weigh the trade-offs and discuss them on the RFC. :)

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that

fn good_11(Wibble(x, y)) {}

should be rejected for the same reason that we now require -> Foo<'_> instead of just -> Foo: the existence of a lifetime should be visible in the function header.

So I still think the answer is that elision fills in lifetimes before the unification algorithm runs. and then the fn arugula(Wibble(x, y)) {} example an error because the unification algorithm doesn't find anything for the lifetime variables to unify with, and thus the signature is under-constrained.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

...and I thought of more stuff for these examples: match ergonomics.

I think the following would work?

fn good_13(Foo(x): &_) {}

Giving a type of for<'a> fn(&'a Foo) and, in the body, x: &'a usize.

One of the rules we've imposed is that each lifetime position mentioned
in a type fragment of some pattern in a function parameter introduces
a distinct lifetime. However, this means that type inference may sometimes
introduce two many lifetimes for one type and therefore reject the definition.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

*too many

@Centril
Copy link
Owner Author

Centril commented Aug 10, 2018

Thanks all for chipping in! Time to publish :)

@Centril Centril closed this Aug 10, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants