`with` bounds for pi types. #1932

ticki · 2017-02-26T15:24:12Z

This is one of 3 RFCs. The collection of the pi type RFCs is tracked by issue #1930.

Depends on #1931

TimNN · 2017-02-26T15:33:20Z

text/0000-with-bounds-in-pi-types.md

+    /// Note how this is not public. This is because we cannot, in the updated
+    /// version of the RFC, set constraints on compile time, so when created it
+    /// must either be dynamically ensured or an unsafe contract must be made
+    in order to satisfy the invariants.


This line is missing the ///

TimNN · 2017-02-26T15:41:53Z

text/0000-with-bounds-in-pi-types.md

+
+Often, it is wanted to have some statically checked clause satisfied by the
+constant parameters (e.g., for the sake of compile-time bound checking). To
+archive this, in a reasonable manner, we use constexprs, returning a boolean.


archive -> achieve

Ixrec · 2017-02-26T15:41:37Z

text/0000-with-bounds-in-pi-types.md

+
+my_func([1, 2, 3]);
+my_func([1, 2, 3, 4]);
+```


This example doesn't seem to require with clauses, only the "core pi types" RFC. Was it meant to go on that one instead?

Ixrec · 2017-02-26T15:41:47Z

text/0000-with-bounds-in-pi-types.md

+        // Clone it...
+    }
+}
+```


TimNN · 2017-02-26T15:47:43Z

text/0000-with-bounds-in-pi-types.md

+care about structural equality, not `Eq` or something else. This allows us to
+reason more rigorously about the behavior.
+
+Any non-identity-related term is threated as an unknown parameter, since reasoning about uniqueness of those is undecidable. For example,


threated -> treated

Ixrec · 2017-02-26T15:51:15Z

text/0000-with-bounds-in-pi-types.md

+We allow such constexprs in `with` clauses of functions. Whenever the
+function is invoked given constant parameters `<a, b...>`, the compiler
+evaluates this expression, and if it returns `false`, an aborting error is
+invoked.


Does "an aborting error is invoked" mean we give up on compilation entirely, or go back to checking for other impls a la SFINAE? This wording sounds like it'd be a compilation error, but I would've expected that we want to allow "impl Foo for 0<n<=2" to coexist alongside "impl Foo for n>2".

If I understood the later parts of the RFC correctly, we aren't going to allow with n=2 and with n>2 impls to coexist anyway, so I guess the answer is "yes it's a compilation error"?

How does that interact with specialization?

Ixrec · 2017-02-26T16:01:42Z

text/0000-with-bounds-in-pi-types.md

+Contradictive or unsatisfiable bounds (like `a < b, b < a`) cannot be detected,
+since such a thing would be undecidable.
+
+These bounds don't break anything, they are simply malformed and unreachable.


Maybe this is the same question as my last comment, but does this also mean "it's not a compiler error to declare such an item, that item would simply never get used because no call site could ever satisfy its bounds"?

Also, what happens if I create an item with a<b, b<a then create a pathological Ord impl where a<b && b<a is actually possible? Does it then get invoked "normally"?

that item would simply never get used because no call site could ever satisfy its bounds"?

That's how I understood it. It is like a special form of uninhabited type that we can't optimize.

create a pathological Ord impl where a<b && b<a is actually possible? Does it then get invoked "normally"?

You mean by overloading > and <? That's the only way this is possible I think. And you would need them to be const.

Assuming that you could create such a situation, I think yes, it would get used "normally".

comex · 2017-02-26T18:17:46Z

Having both with and where strikes me as confusing; they mean the same thing in English in this context, and they seem to do the same thing for value and type constraints, respectively. Why not just allow boolean constexprs to be written in where clauses using the same syntax as the previous RFC? e.g. where {a < b}

comex · 2017-02-26T18:57:18Z

Reply to self: I guess that'd make where Foo: Bar, { ambiguous, since where allows trailing commas. The const EXPR variant wouldn't have that problem but would be much more verbose. Sigh…. I still don't like with though.

where Foo: Bar, ({a < b}) would also be a possibility, but yikes.

Maybe we could just tell people to avoid less-than? where b > a is unambiguous, as is where a <= b + 1 and !!(a < b) and true == (a < b).

kennytm · 2017-02-26T19:14:23Z

text/0000-with-bounds-in-pi-types.md

+/// A bounded integer.
+///
+/// This has two value parameter, respectively representing an upper and a lower bound.
+pub struct BoundedInt<const lower: usize, const upper: usize> {


Is there a missing with lower <= upper here? The rest of the code seemed to assume it.

gnzlbg · 2017-02-26T20:04:49Z

I think we should have a "How do we debug this" section in this RFC, at least as an unanswered question.

Some thoughts considering a situation, where two non-overlapping impls are at play, and the wrong one is chosen due to a bug in a with expression or const fn:

one cannot insert print statements all over the place, because that is not allowed in const fn.
the debugger pinpoints which function of which impl is being called, but not how did that impl got chosen (and all the const fn computations won't show in the debugger).
the C++ way to debug these issues is to "break the compiler in such a way that it spits the information you need", possibly multiple times at every step along the chain.

It might be that "how to debug these things" is still an open research problem without a solution, but we should at least give it some thought before hand.

withoutboats · 2017-02-26T20:22:28Z

Thanks for splitting #1657 ticki. I just want to give you the heads up that we'll probably postpone this and #1933 during triage (next triage is March 9th), on the same grounds as #1657.

I definitely see why having all of these open is useful from your perspective, but from ours, as of this writing we have 49 lang RFCs. This number has consistently been more than half the open RFCs, and despite our best efforts to resolve RFCs it continues to grow. In order both to track progress more effectively and give contributors some sense of confidence their RFCs are being worked on, we're trying to keep open only those RFCs making immediate progress. In this case, that's #1931.

Ixrec · 2017-02-26T20:37:24Z

I had already assumed both of these would be "de facto postponed" until #1931 got at least accepted, if not implemented and stabilized, so making that status explicit sounds fine to me.

tmccrmck · 2017-02-27T02:24:43Z

Would the Experimental extensions open to discussion section make more sense in #1933?

fitzgen · 2017-02-27T15:49:22Z

Having both with and where strikes me as confusing;

I agree.

I didn't follow the original ambiguities with re-using "where", could someone point me to relevant discussion?

Would qualifying const type parameters' bounds with "const" provide disambiguation? For example:

impl<const a: usize, const b: usize> Divides<b> for Num<a>
    where const b % a == 0 {}

0x7CFE · 2017-02-27T17:01:37Z

text/0000-with-bounds-in-pi-types.md

+    DistributiveMultiplicationLhs:
+      c(a + b) ↦ ca + cb
+    DistributiveMultiplicationRhs:
+      (a + b)c ↦ ca + cb


Should it be (a + b)c ↦ ac + bc?

I think this would require a commutativity rule, which is not reductive, IIUC.

Hm… Isn't it the original version that requires commutativity rule? Right multiplication is applied, but result term have c to the left. Or am I missing something?

Assuming that I know what I'm talking about, what matters is that both rules produce the same form. Otherwise, one will need an extra step to be able to simplify further (a step which is problematic because it is not reductive).

Oh, now I see. So that was intentional. Thank you.

P.S.: IIUC, that means that multiplication itself is implicitly commutative, so the user should be ready for it. But what if actual operands are not commutative? Say, a b and c are matrices. In such a case we may not distribute the multiplication that way.

@dkashitsyn I don't think these rules apply to custom types or even floating-point types, they should be just be treated as a.mul(b).

I was actually just thinking about the same problem since you can arbitrarily overload * with Mul... however, it might still work because overloading Mul is not const, right?

@mark-i-m Yeah... E0379.

pkou · 2017-03-01T14:54:47Z

Alternate syntax to consider: Using if <condition> as a part of where clause, e.g. where ... [if <condition>]

fn copy1<T, const N: usize, const K: usize>(target: &mut [T; N], source: &[T; K])
    where T: Copy if N <= K
{
    ...
}

fn copy2<const N: usize, const K: usize>(target: &mut [u8; N], source: &[u8, K])
    where if N <= K
{
   ...
}

mark-i-m · 2017-03-01T17:09:54Z

I am still unsure of why it is ambiguous to use where...

aturon · 2017-03-10T00:25:15Z

Thanks @ticki.

The lang team discussed this RFC a bit during the triage meeting today, and consensus continues to be as laid out in the comment on the previous RFC, namely that this extension is getting quite a bit far ahead of things, and we should focus for now solely on a minimal const generics proposal, and the implementation foundation to support it.

While it's certainly fine to discuss the topic, we'd prefer discussion to happen on https://internals.rust-lang.org/ for the time being, in the interest of keeping the RFC PR list pruned to proposals under consideration in the relatively near term. This is a topic worth revisiting after the core has stabilized.

@rfcbot fcp postpone

rfcbot · 2017-03-10T00:25:16Z

Team member @aturon has proposed to postpone this. The next step is review by the rest of the tagged teams:

No concerns currently listed.

Once these reviewers reach consensus, this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

rfcbot · 2017-04-03T20:41:20Z

🔔 This is now entering its final comment period, as per the review above. 🔔

rfcbot · 2017-04-13T20:51:01Z

The final comment period is now complete.

aturon · 2017-04-13T22:26:37Z

Closing as postponed, per the summary above.

FWIW, the lang team spent much of today's meeting discussing const generics and some of the subtle semantic issues involved. The good news is that there seems to be a pretty straightforward story, and the needed implementation work isn't too far off. @withoutboats should have more on that in other threads.

xiaoniu-578fa6bff964d005 · 2018-10-19T07:40:32Z

text/0000-with-bounds-in-pi-types.md

+            n: from.n,
+        }
+    }
+}


if lower_b <= lower_a && upper_b >= upper_a hold true, then [lower_b, upper_b] actually contains [lower_a, upper_a]. So if you cast one number from BoundedInt<lower_b, upper_b> to BoundedInt<lower_a, upper_a>, you actually "shrink" the bound rather than extend it.

with bounds for pi types.

df76a8e

This was referenced Feb 26, 2017

Fully dependent pi types. #1933

Closed

The pi type trilogy #1930

Closed

TimNN reviewed Feb 26, 2017

View reviewed changes

Ixrec reviewed Feb 26, 2017

View reviewed changes

TimNN reviewed Feb 26, 2017

View reviewed changes

Ixrec reviewed Feb 26, 2017

View reviewed changes

kennytm reviewed Feb 26, 2017

View reviewed changes

withoutboats added the T-lang Relevant to the language team, which will review and decide on the RFC. label Feb 26, 2017

mark-i-m mentioned this pull request Feb 26, 2017

RFC: Constant generics (restricted Π types) for Rust, core RFC (v2) #1931

Closed

0x7CFE reviewed Feb 27, 2017

View reviewed changes

aturon self-assigned this Mar 9, 2017

rfcbot added the final-comment-period Will be merged/postponed/closed in ~10 calendar days unless new substational objections are raised. label Apr 3, 2017

aturon closed this Apr 13, 2017

kennytm mentioned this pull request Aug 24, 2017

Const generics #2000

Merged

kennytm mentioned this pull request Nov 18, 2017

Tracking issue for RFC 1861: Extern types rust-lang/rust#43467

Open

3 tasks

hdevalence mentioned this pull request May 19, 2017

Fix overflow bug in Decaf Elligator code dalek-cryptography/curve25519-dalek#54

Merged

xiaoniu-578fa6bff964d005 reviewed Oct 19, 2018

View reviewed changes

kennytm mentioned this pull request May 12, 2020

Add more functionality to where clause #2715

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`with` bounds for pi types. #1932

`with` bounds for pi types. #1932

ticki commented Feb 26, 2017 •

edited

Loading

TimNN Feb 26, 2017

TimNN Feb 26, 2017

Ixrec Feb 26, 2017

Ixrec Feb 26, 2017

TimNN Feb 26, 2017

Ixrec Feb 26, 2017 •

edited

Loading

Ixrec Feb 26, 2017

eternaleye Feb 27, 2017

Ixrec Feb 26, 2017

mark-i-m Feb 28, 2017

comex commented Feb 26, 2017

comex commented Feb 26, 2017 •

edited

Loading

kennytm Feb 26, 2017

gnzlbg commented Feb 26, 2017

withoutboats commented Feb 26, 2017 •

edited

Loading

Ixrec commented Feb 26, 2017

tmccrmck commented Feb 27, 2017

fitzgen commented Feb 27, 2017

0x7CFE Feb 27, 2017 •

edited

Loading

mark-i-m Feb 28, 2017

0x7CFE Mar 1, 2017 •

edited

Loading

mark-i-m Mar 1, 2017

dkashitsyn Mar 1, 2017

kennytm Mar 1, 2017

mark-i-m Mar 1, 2017

kennytm Mar 1, 2017

pkou commented Mar 1, 2017

mark-i-m commented Mar 1, 2017

aturon commented Mar 10, 2017

rfcbot commented Mar 10, 2017 •

edited by nikomatsakis

Loading

rfcbot commented Apr 3, 2017

rfcbot commented Apr 13, 2017

aturon commented Apr 13, 2017

xiaoniu-578fa6bff964d005 Oct 19, 2018

with bounds for pi types. #1932

with bounds for pi types. #1932

Conversation

ticki commented Feb 26, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Ixrec Feb 26, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

comex commented Feb 26, 2017

comex commented Feb 26, 2017 • edited Loading

Choose a reason for hiding this comment

gnzlbg commented Feb 26, 2017

withoutboats commented Feb 26, 2017 • edited Loading

Ixrec commented Feb 26, 2017

tmccrmck commented Feb 27, 2017

fitzgen commented Feb 27, 2017

0x7CFE Feb 27, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

0x7CFE Mar 1, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pkou commented Mar 1, 2017

mark-i-m commented Mar 1, 2017

aturon commented Mar 10, 2017

rfcbot commented Mar 10, 2017 • edited by nikomatsakis Loading

rfcbot commented Apr 3, 2017

rfcbot commented Apr 13, 2017

aturon commented Apr 13, 2017

Choose a reason for hiding this comment

`with` bounds for pi types. #1932

`with` bounds for pi types. #1932

ticki commented Feb 26, 2017 •

edited

Loading

Ixrec Feb 26, 2017 •

edited

Loading

comex commented Feb 26, 2017 •

edited

Loading

withoutboats commented Feb 26, 2017 •

edited

Loading

0x7CFE Feb 27, 2017 •

edited

Loading

0x7CFE Mar 1, 2017 •

edited

Loading

rfcbot commented Mar 10, 2017 •

edited by nikomatsakis

Loading