From 27c33a354e42172918e9b19e78dd30a8e109433c Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 13:40:16 +0200 Subject: [PATCH 01/34] =?UTF-8?q?rfc:=20=CE=A0-types?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- text/0000-pi-types.md | 182 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 182 insertions(+) create mode 100644 text/0000-pi-types.md diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md new file mode 100644 index 00000000000..f145147d381 --- /dev/null +++ b/text/0000-pi-types.md @@ -0,0 +1,182 @@ +- Feature Name: pi-types +- Start Date: 2016-06-22 +- RFC PR: (leave this empty) +- Rust Issue: (leave this empty) + +# Summary +[summary]: #summary + +We propose a simple, yet sufficiently expressive, addition of dependent-types +(also known as, Π-types and value-types). + +Type checking remains decidable. + +# Motivation +[motivation]: #motivation + +An often requested feature is the "type-level numerals", which enables generic +length arrays. The current proposals are often limited to integers or even lack +of value maps, and other critical features. + +There is a whole lot of other usecases as well. These allows certain often +requested features to live in standalone libraries (e.g., bounded-integers, +type level arithmetics, lattice types). + +# Detailed design +[design]: #detailed-design + +## The new value-type construct, `const` + +The first construct, we will introduce is `ε → τ` constructor, `const`. All this +does is taking a const-expr (struct construction, arithmetic expression, and so +on) and constructs a _type-level version_ of this. + +In particular, we extend the type grammar with an additional `const C`, a type +whose semantics can be described as follows, + + ValueTypeRepresentation: + Π ⊢ x: const c + -------------- + Π ⊢ x = c + +In other words, if `x` has type `const c`, its value _is_ `c`. That is, any +constexpr, `c`, will either be of its underlying type or of the type, `const +c`. + +It is important to understand that values of `const c` are constexprs, and +follows their rules. + +## `const fn`s as Π-constructors + +We are interested in value dependency, but at the same time, we want to avoid +complications such as SMT-solvers and so on. + +Thus, we follow a purely constructible model, by using `const fn`s. + +Let `f` be a `const fn` function. From the rules of `const fn`s and constexprs, +we can derive the rule, + + PiConstructorInference: + Π ⊢ x: const c + Π ⊢ f(c): τ + -------------- + Π ⊢ f(x): const τ + +This allows one to take some const parameter and map it by some arbitrary, pure +function. + +## Type inference + +Since we are able to evaluate the function on compile time, we can easily infer +const types, by adding an unification relation, from the rule above. + +The relational edge between two const types is simple a const fn, which is +resolved under unification. + +## `where` clauses + +Often, it is wanted to have some statically checked clause satisfied by the +constant parameters. To archive this, in a reasonable manner, we use const +exprs, returning a boolean. + +We allow such constexprs in `where` clauses of functions. Whenever the +function is invoked given constant parameters ``, the compiler +evaluates this expression, and if it returns `false`, an aborting error is +invoked. + +## The type grammar + +These extensions expand the type grammar to: + + T = scalar (i32, u32, ...) // Scalars + | X // Type variable + | Id // Nominal type (struct, enum) + | &r T // Reference (mut doesn't matter here) + | O0..On+r // Object type + | [T] // Slice type + | for fn(T1..Tn) -> T0 // Function pointer + | >::Id // Projection + | C // const types + F = c // const fn name + C = E // Pi constructed const type + P = r // Region name + | T // Type + O = for TraitId // Object type fragment + r = 'x // Region name + E = F(E) // Constant function application. + | p // const type parameter + | [...] // etc. + +Note that the `const` prefix is only used when declaring the parameter. + +## An example + +This is the proposed syntax: + +```rust +use std::{mem, ptr}; + +// We start by declaring a struct which is value dependent. +struct Array { + // `n` is a constexpr, sharing similar behavior with `const`s, thus this + // is possible. + content: [T; n], +} + +// We are interested in exploring the `where` clauses and Π-constructors: +impl Array { + // This is simple statically checked indexing. + fn const_index(&self) -> &T where i < n { + // note that this is constexpr ^^^^^ + unsafe { self.content.unchecked_index(i) } + } + + // "Push" a new element, incrementing its length **statically**. + fn push(self, elem: T) -> Array { + let mut new: [T; n + 1] = mem::uninitialized(); + // ^^^^^ constexpr + unsafe { + ptr::copy(self.content.as_ptr(), new.as_mut_ptr(), n); + ptr::write(new.as_mut_ptr().offset(n), elem); + } + + // Don't call destructors. + mem::forget(self.content); + + // So, the compiler knows the type of `new`. Thus, it can easily check + // if the return type is matching. By siply evaluation `n + 1`, then + // comparing against the given return type. + Array { content: new } + } +} + +fn main() { + let array: Array<2, u32> = Array { content: [1, 2] }; + + assert_eq!(array.const_index::<0>(), 1); + assert_eq!(array.const_index::<1>(), 2); + assert_eq!(array.push(3).const_index::<2>(), 3); +} +``` + +# Drawbacks +[drawbacks]: #drawbacks + +If we want to have type-level Turing completeness, the halting problem is +inevitable. One could "fix" this by adding timeouts, like the current recursion +bounds. + +Another draw back is the lack of implication proves. + +# Alternatives +[alternatives]: #alternatives + +Use full SMT-based dependent types. These are more expressive, but severely +more complex as well. + +# Unresolved questions +[unresolved]: #unresolved-questions + +What syntax is preferred? How does this play together with HKP? Can we improve +the converse type inference? What should be the naming conventions? Should we +segregate the value parameters and type parameters by `;`? From e4446c58a0acf6feb84a5c4eea17e027b89b5f89 Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 14:17:54 +0200 Subject: [PATCH 02/34] Expand the `overview` section --- text/0000-pi-types.md | 36 +++++++++++++++++++++++++++++++++--- 1 file changed, 33 insertions(+), 3 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index f145147d381..503f5b2ee9e 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -9,7 +9,36 @@ We propose a simple, yet sufficiently expressive, addition of dependent-types (also known as, Π-types and value-types). -Type checking remains decidable. +Type checking will not require SMT-solvers or other forms of theorem provers. + +## Generic value parameters + +A `const` type parameter acts like a generic parameter, containing a constant +expression. Declaring a generic parameter `a: const usize`, creates a constant +variable `a` of type `usize`. + +One can create implementations, structs, enums, and traits, abstracting over +this generic value parameter. + +We use the syntax `a: const value` to denote the constant type parameter, `a`, +of constant value, `value`. This can be used at both type-level (as parameter) +and value-level (as expression). + +## Compile time calculations on constant parameters + +Since it is simply consisting of constexprs, one can apply constant functions +(`const fn`) to the parameter, to perform compile time, type level calculations +on the parameter. This allows for great expressiveness as `const fn` improves. + +## Expression `where` bounds + +The second construct added is the constant expression in `where` bounds. These +contains statements about the constant parameters, which are checked at compile +time. + +## Type checking + +Type checking is done eagerly by evaluating the bounds and constexprs. # Motivation [motivation]: #motivation @@ -67,7 +96,7 @@ function. ## Type inference -Since we are able to evaluate the function on compile time, we can easily infer +Since we are able to evaluate the function at compile time, we can easily infer const types, by adding an unification relation, from the rule above. The relational edge between two const types is simple a const fn, which is @@ -179,4 +208,5 @@ more complex as well. What syntax is preferred? How does this play together with HKP? Can we improve the converse type inference? What should be the naming conventions? Should we -segregate the value parameters and type parameters by `;`? +segregate the value parameters and type parameters by `;`? Disjoint +implementations satisfying some bound? From eb60cd3b9e1cea0f81df8a0d580e98067f0eb07b Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 15:27:11 +0200 Subject: [PATCH 03/34] Propose alternative syntaxes --- text/0000-pi-types.md | 37 ++++++++++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 503f5b2ee9e..579bc07bc70 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -156,7 +156,7 @@ struct Array { impl Array { // This is simple statically checked indexing. fn const_index(&self) -> &T where i < n { - // note that this is constexpr ^^^^^ + // note that this is constexpr ^^^^^ unsafe { self.content.unchecked_index(i) } } @@ -203,6 +203,41 @@ Another draw back is the lack of implication proves. Use full SMT-based dependent types. These are more expressive, but severely more complex as well. +## Alternative syntax + +The syntax is described above is, in fact, ambiguous, and multiple other better or worse +candidates exists: + +### Blending the value parameters into the arguments + +This one is an interesting one. It allows for defining functions with constant +_arguments_ instead of constant _parameters_. This allows for bounds on e.g. +`atomic::Ordering`. + +```rust +fn do_something(const x: u32) -> u32 where x < 5 { x } +``` + +### Angle brackets + +Use angle brackets for dependent parameters: + +```rust +fn do_something[x: u32]() -> u32 where x < 5 { x } + +do_something::[2](); +``` + +### `const` _before_ the parameter + +Use the proposed syntax in similar manner to constant definitions: + +```rust +fn do_something() -> u32 where x < 5 { x } + +do_something::<2>(); +``` + # Unresolved questions [unresolved]: #unresolved-questions From 71f2d8bf288bb568131a22a76442a4c7153be35c Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 16:42:41 +0200 Subject: [PATCH 04/34] Improve type inference with a new rule allowing direct substitution --- text/0000-pi-types.md | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 579bc07bc70..c596d695378 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -88,7 +88,7 @@ we can derive the rule, PiConstructorInference: Π ⊢ x: const c Π ⊢ f(c): τ - -------------- + ----------------- Π ⊢ f(x): const τ This allows one to take some const parameter and map it by some arbitrary, pure @@ -102,6 +102,29 @@ const types, by adding an unification relation, from the rule above. The relational edge between two const types is simple a const fn, which is resolved under unification. +We add an extra rule to improve inference: + + PiDependencyInference: + Γ ⊢ T: A → 𝓤 + Γ ⊢ a: T + Γ ⊢ a: T + -------------- + Γ ⊢ x: const c + +This allows us infer: + +```rust +// [T; N] is a constructor, T → usize → 𝓤 (parameterize over T and you get A → 𝓤). +fn foo() -> [u32; n] { + // ^ note how l depends on n. + l +} + +// We know n from the length of the array. +let l = baz::<_, [1, 2, 3, 4, 5, 6]>(); +// ^ ^^^^^^^^^^^^^^^^ +``` + ## `where` clauses Often, it is wanted to have some statically checked clause satisfied by the From b3558113d4e74d33fe9e8c4da58807fe8cf0b3f4 Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 18:12:22 +0200 Subject: [PATCH 05/34] Add section on impl unification --- text/0000-pi-types.md | 67 +++++++++++++++++++++++++++++-------------- 1 file changed, 46 insertions(+), 21 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index c596d695378..3e82eb64679 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -38,7 +38,7 @@ time. ## Type checking -Type checking is done eagerly by evaluating the bounds and constexprs. +Type checking is done lazily by evaluating the bounds and constexprs. # Motivation [motivation]: #motivation @@ -136,31 +136,51 @@ function is invoked given constant parameters ``, the compiler evaluates this expression, and if it returns `false`, an aborting error is invoked. +To sum up, the check happens at monomorphization, thus a function can type +check until it is called (note that this is already possible in present day +Rust, through `where` bounds). + ## The type grammar These extensions expand the type grammar to: - T = scalar (i32, u32, ...) // Scalars - | X // Type variable - | Id // Nominal type (struct, enum) - | &r T // Reference (mut doesn't matter here) - | O0..On+r // Object type - | [T] // Slice type - | for fn(T1..Tn) -> T0 // Function pointer - | >::Id // Projection - | C // const types - F = c // const fn name - C = E // Pi constructed const type - P = r // Region name - | T // Type - O = for TraitId // Object type fragment - r = 'x // Region name - E = F(E) // Constant function application. - | p // const type parameter - | [...] // etc. + T = scalar (i32, u32, ...) // Scalars + | X // Type variable + | Id // Nominal type (struct, enum) + | &r T // Reference (mut doesn't matter here) + | O0..On+r // Object type + | [T] // Slice type + | for fn(T1..Tn) -> T0 // Function pointer + | >::Id // Projection + + | C // const types + + F = c // const fn name + + C = E // Pi constructed const type + P = r // Region name + | T // Type + O = for TraitId // Object type fragment + r = 'x // Region name + + E = F(E) // Constant function application. + + | p // const type parameter + + | [...] // etc. Note that the `const` prefix is only used when declaring the parameter. +## `impl` unification + +Only one `where` bound can be specified on each disjoint implementations (for +possible extensions, see below). + +To find the right implementation, we use the data from the type inference (see +the inference rules above). Since the parameters are, in fact, not much +semantically different from normal generic parameters, we can resolve it is a +normal manner. + +Likewise are disjointness checks based on structural equality. + +Since not all parameters' edges are necessarily the identity function, +dispatching these would be undecidable. A way to solve this problem is to +introduce some syntax allowing to specify the `impl` parameters. + ## An example This is the proposed syntax: @@ -241,9 +261,9 @@ _arguments_ instead of constant _parameters_. This allows for bounds on e.g. fn do_something(const x: u32) -> u32 where x < 5 { x } ``` -### Angle brackets +### Square brackets -Use angle brackets for dependent parameters: +Use square brackets for dependent parameters: ```rust fn do_something[x: u32]() -> u32 where x < 5 { x } @@ -261,6 +281,11 @@ fn do_something() -> u32 where x < 5 { x } do_something::<2>(); ``` +### Allow multiple implementation bounds + +Allow overlapping implementations carrying bounds, such that only one of the +conditions may be true under monomorphization. + # Unresolved questions [unresolved]: #unresolved-questions From a70553246a72dc30f4a70f0d603a04c19a624855 Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 18:17:38 +0200 Subject: [PATCH 06/34] Add transitivity suggestion --- text/0000-pi-types.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 3e82eb64679..a27272e125b 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -140,6 +140,15 @@ To sum up, the check happens at monomorphization, thus a function can type check until it is called (note that this is already possible in present day Rust, through `where` bounds). +### (Optional extension:) Transitivity of bounds. + +An optional extension is to require a bound of a function to imply the bounds +of the functions it calls, through a simple unification + alpha-substitution +algorithm. + +The compiler would then enforce that if `f` calls `g`, `unify(bound(g)) ⊆ +unify(bound(f))` (by structural equality). + ## The type grammar These extensions expand the type grammar to: From 946aa558682873fc6b1bea8f49c27f7d837971a2 Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 20:56:01 +0200 Subject: [PATCH 07/34] Change syntax, add transitivity rule --- text/0000-pi-types.md | 139 ++++++++++++++++++++++++------------------ 1 file changed, 81 insertions(+), 58 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index a27272e125b..61f4748335b 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -14,15 +14,15 @@ Type checking will not require SMT-solvers or other forms of theorem provers. ## Generic value parameters A `const` type parameter acts like a generic parameter, containing a constant -expression. Declaring a generic parameter `a: const usize`, creates a constant +expression. Declaring a generic parameter `const a: usize`, declares a constant variable `a` of type `usize`. One can create implementations, structs, enums, and traits, abstracting over this generic value parameter. -We use the syntax `a: const value` to denote the constant type parameter, `a`, -of constant value, `value`. This can be used at both type-level (as parameter) -and value-level (as expression). +Such a parameter acts type-like in the context of types, generics, and +polymorphism, and value-like in the context of expressions, function bodies, +and applications. ## Compile time calculations on constant parameters @@ -38,7 +38,8 @@ time. ## Type checking -Type checking is done lazily by evaluating the bounds and constexprs. +Type checking is done by using a transitive rule, such that `where` bounds must +be implied by the caller. # Motivation [motivation]: #motivation @@ -56,24 +57,25 @@ type level arithmetics, lattice types). ## The new value-type construct, `const` -The first construct, we will introduce is `ε → τ` constructor, `const`. All this -does is taking a const-expr (struct construction, arithmetic expression, and so -on) and constructs a _type-level version_ of this. +The first construct, we will introduce one allowing us to declare `ε → τ` +constructors (value dependent types). -In particular, we extend the type grammar with an additional `const C`, a type -whose semantics can be described as follows, +In a sense, `const` "bridges" between types and values. - ValueTypeRepresentation: - Π ⊢ x: const c - -------------- - Π ⊢ x = c +Declaring a parameter `const x: T` allows use in both expression context (as a +value of type `T`) and type context (as a type parameter). + +Such a parameter is declared, like type parameters, in angle brackets. -In other words, if `x` has type `const c`, its value _is_ `c`. That is, any -constexpr, `c`, will either be of its underlying type or of the type, `const -c`. +The expr behavior is described as: -It is important to understand that values of `const c` are constexprs, and -follows their rules. + ValueParameterDeclaration: + Π ⊢ const x: T + -------------- + Π ⊢ x: T + +On the type level, we use the very same semantics as the ones generic +parameters currently follows. ## `const fn`s as Π-constructors @@ -82,34 +84,36 @@ complications such as SMT-solvers and so on. Thus, we follow a purely constructible model, by using `const fn`s. -Let `f` be a `const fn` function. From the rules of `const fn`s and constexprs, -we can derive the rule, - - PiConstructorInference: - Π ⊢ x: const c - Π ⊢ f(c): τ - ----------------- - Π ⊢ f(x): const τ - This allows one to take some const parameter and map it by some arbitrary, pure -function. +function, following the rules described in [RFC 0911](https://github.com/rust-lang/rfcs/blob/master/text/0911-const-fn.md#detailed-design). ## Type inference Since we are able to evaluate the function at compile time, we can easily infer -const types, by adding an unification relation, from the rule above. +const parameters, by adding an unification relation, simply + + PiRelationInference + Γ ⊢ y = f(x) + Γ ⊢ T: U + -------------- + Γ ⊢ T: U -The relational edge between two const types is simple a const fn, which is +The relational edge between two const parameters is simple a const fn, which is resolved under unification. We add an extra rule to improve inference: - PiDependencyInference: + DownLiftEquality: Γ ⊢ T: A → 𝓤 + Γ ⊢ c: A + Γ ⊢ x: A Γ ⊢ a: T Γ ⊢ a: T -------------- - Γ ⊢ x: const c + Γ ⊢ c = x + +So, if two types share constructor by some Π-constructor, share a value, their +value parameter is equal. This allows us infer: @@ -136,20 +140,21 @@ function is invoked given constant parameters ``, the compiler evaluates this expression, and if it returns `false`, an aborting error is invoked. -To sum up, the check happens at monomorphization, thus a function can type -check until it is called (note that this is already possible in present day -Rust, through `where` bounds). +To sum up, the check happens at monomorphization. The callers bounds must imply +the invoked functions' bounds: -### (Optional extension:) Transitivity of bounds. +### Transitivity of bounds. -An optional extension is to require a bound of a function to imply the bounds -of the functions it calls, through a simple unification + alpha-substitution -algorithm. +We require a bound of a function to imply the bounds of the functions it calls, +through a simple unification + alpha-substitution algorithm. The compiler would then enforce that if `f` calls `g`, `unify(bound(g)) ⊆ unify(bound(f))` (by structural equality). -## The type grammar +This is done under type unification. Thus, we only need to check the bounds at +the top level. + +## The grammar These extensions expand the type grammar to: @@ -172,7 +177,7 @@ These extensions expand the type grammar to: + | p // const type parameter + | [...] // etc. -Note that the `const` prefix is only used when declaring the parameter. +Note that the `const` syntax is only used when declaring the parameter. ## `impl` unification @@ -198,17 +203,17 @@ This is the proposed syntax: use std::{mem, ptr}; // We start by declaring a struct which is value dependent. -struct Array { +struct Array { // `n` is a constexpr, sharing similar behavior with `const`s, thus this // is possible. content: [T; n], } // We are interested in exploring the `where` clauses and Π-constructors: -impl Array { +impl Array { // This is simple statically checked indexing. - fn const_index(&self) -> &T where i < n { - // note that this is constexpr ^^^^^ + fn checked_index(&self) -> &T where i < n { + // note that this is constexpr ^^^^^ unsafe { self.content.unchecked_index(i) } } @@ -234,9 +239,9 @@ impl Array { fn main() { let array: Array<2, u32> = Array { content: [1, 2] }; - assert_eq!(array.const_index::<0>(), 1); - assert_eq!(array.const_index::<1>(), 2); - assert_eq!(array.push(3).const_index::<2>(), 3); + assert_eq!(array.checked_index::<0>(), 1); + assert_eq!(array.checked_index::<1>(), 2); + assert_eq!(array.push(3).checked_index::<2>(), 3); } ``` @@ -247,7 +252,7 @@ If we want to have type-level Turing completeness, the halting problem is inevitable. One could "fix" this by adding timeouts, like the current recursion bounds. -Another draw back is the lack of implication proves. +Another drawback is the lack of implication proves. # Alternatives [alternatives]: #alternatives @@ -257,8 +262,8 @@ more complex as well. ## Alternative syntax -The syntax is described above is, in fact, ambiguous, and multiple other better or worse -candidates exists: +The syntax is described above is, in fact, ambiguous, and multiple other better +or worse candidates exists: ### Blending the value parameters into the arguments @@ -270,6 +275,8 @@ _arguments_ instead of constant _parameters_. This allows for bounds on e.g. fn do_something(const x: u32) -> u32 where x < 5 { x } ``` +From the callers perspective, this one is especially nice to work with. + ### Square brackets Use square brackets for dependent parameters: @@ -280,16 +287,25 @@ fn do_something[x: u32]() -> u32 where x < 5 { x } do_something::[2](); ``` -### `const` _before_ the parameter +### `const` as an value-type constructor Use the proposed syntax in similar manner to constant definitions: ```rust -fn do_something() -> u32 where x < 5 { x } +fn do_something() -> u32 where x < 5 { x } do_something::<2>(); ``` +### `with` instead of `where` + +Some have raised concerns of mixing things up there. Thus one can use the +syntax `with` to denote bounds instead. + +### Lazily type check without transitivity rule + +Simply evaluate the bounds when calling. Remove the requirement of implication. + ### Allow multiple implementation bounds Allow overlapping implementations carrying bounds, such that only one of the @@ -298,7 +314,14 @@ conditions may be true under monomorphization. # Unresolved questions [unresolved]: #unresolved-questions -What syntax is preferred? How does this play together with HKP? Can we improve -the converse type inference? What should be the naming conventions? Should we -segregate the value parameters and type parameters by `;`? Disjoint -implementations satisfying some bound? +What syntax is preferred? + +How does this play together with HKP? + +What should be the naming conventions? + +Should we segregate the value parameters and type parameters by `;`? + +Should disjoint implementations satisfying some bound be allowed? + +Should there be a way to parameterize functions dynamically? From d52e7289a041c16596a07433b86fc73c90a08ecb Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 21:13:51 +0200 Subject: [PATCH 08/34] Add 'How we teach this' --- text/0000-pi-types.md | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 61f4748335b..be6a25ec7b7 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -52,6 +52,8 @@ There is a whole lot of other usecases as well. These allows certain often requested features to live in standalone libraries (e.g., bounded-integers, type level arithmetics, lattice types). +It allows for creating powerful abstractions without type-level hackery. + # Detailed design [design]: #detailed-design @@ -245,6 +247,34 @@ fn main() { } ``` +# How we teach this + +This RFC aims to keep a "symmetric" syntax to the current construct, giving an +intuitive behavior, however there are multiple things that are worth explaining +and/or clearing up: + +1. What are Π-types? How are they different from those from other languages? + +2. One will have to understand what `const fn`s are and how they are linked to + Π-types. + +3. What are the usecases? + +4. What are the edge cases, and how can one work around those (e.g. failed + unification)? + +5. How can I use this to create powerful abstractions? + +6. Extensive examples. + +Moreover, we need to "informalize" the rules defined in this RFC. + +I believe this subject is complex enough to have its own chapter in The Holy +Book, answering these questions in detail. + +Lastly, the FAQ will need to be updated to answer various questions related to +this. + # Drawbacks [drawbacks]: #drawbacks @@ -325,3 +355,5 @@ Should we segregate the value parameters and type parameters by `;`? Should disjoint implementations satisfying some bound be allowed? Should there be a way to parameterize functions dynamically? + +What API would need to be rewritten to take advantage of Π-types? From 551688c207c21a203e85d8b2687000fdaff851b0 Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 21:16:15 +0200 Subject: [PATCH 09/34] Fix the code example --- text/0000-pi-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index be6a25ec7b7..7c677870ad4 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -121,7 +121,7 @@ This allows us infer: ```rust // [T; N] is a constructor, T → usize → 𝓤 (parameterize over T and you get A → 𝓤). -fn foo() -> [u32; n] { +fn foo() -> [u32; n] { // ^ note how l depends on n. l } From ea92a57cc46cad69273ed74f2ed4f03b873572dc Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 21:28:48 +0200 Subject: [PATCH 10/34] Add optional extension --- text/0000-pi-types.md | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 7c677870ad4..e707e3998d4 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -319,7 +319,7 @@ do_something::[2](); ### `const` as an value-type constructor -Use the proposed syntax in similar manner to constant definitions: +Create a keyword, `const`: ```rust fn do_something() -> u32 where x < 5 { x } @@ -327,6 +327,26 @@ fn do_something() -> u32 where x < 5 { x } do_something::<2>(); ``` +### An extension: A constexpr type constructor + +Add some language item type constructor, `Const`, allowing for constructing +a constexpr-only types. + +`x: T` can coerce into `Const` if `x` is constexpr. Likewise, can `Const` +coerce into `T`. + +```rust +fn do_something(x: Const) -> u32 { x } + +struct Abc { + constfield: Const, +} +``` + +It is unclear how it plays together with `where` bounds. + +The pro is that it adds ability to implement e.g. constant indexing, `Index>`. + ### `with` instead of `where` Some have raised concerns of mixing things up there. Thus one can use the From 1d8813baa91f61527815b06139bc7b2dee497911 Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 21:30:35 +0200 Subject: [PATCH 11/34] s/baz/foo --- text/0000-pi-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index e707e3998d4..962f434c481 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -127,7 +127,7 @@ fn foo() -> [u32; n] { } // We know n from the length of the array. -let l = baz::<_, [1, 2, 3, 4, 5, 6]>(); +let l = foo::<_, [1, 2, 3, 4, 5, 6]>(); // ^ ^^^^^^^^^^^^^^^^ ``` From d6a9b05cda706e2ae5c0ab787c1439537f010517 Mon Sep 17 00:00:00 2001 From: ticki Date: Wed, 22 Jun 2016 22:10:51 +0200 Subject: [PATCH 12/34] Use unicode for the lines --- text/0000-pi-types.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 962f434c481..10fc9aade95 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -73,7 +73,7 @@ The expr behavior is described as: ValueParameterDeclaration: Π ⊢ const x: T - -------------- + ────────────── Π ⊢ x: T On the type level, we use the very same semantics as the ones generic @@ -97,7 +97,7 @@ const parameters, by adding an unification relation, simply PiRelationInference Γ ⊢ y = f(x) Γ ⊢ T: U - -------------- + ────────────── Γ ⊢ T: U The relational edge between two const parameters is simple a const fn, which is @@ -111,7 +111,7 @@ We add an extra rule to improve inference: Γ ⊢ x: A Γ ⊢ a: T Γ ⊢ a: T - -------------- + ────────────── Γ ⊢ c = x So, if two types share constructor by some Π-constructor, share a value, their From 99b200512c0c5949723085d59e2891c575494106 Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 10:29:47 +0200 Subject: [PATCH 13/34] Expand on the implication checking and the rules governing it --- text/0000-pi-types.md | 52 ++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 49 insertions(+), 3 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 10fc9aade95..d3c87c5f390 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -142,8 +142,9 @@ function is invoked given constant parameters ``, the compiler evaluates this expression, and if it returns `false`, an aborting error is invoked. -To sum up, the check happens at monomorphization. The callers bounds must imply -the invoked functions' bounds: +To sum up, the check happens when typechecking the function calls (that is, +checking if the parameters satisfy the trait bounds, and so on). The caller's +bounds must imply the invoked functions' bounds: ### Transitivity of bounds. @@ -151,11 +152,56 @@ We require a bound of a function to imply the bounds of the functions it calls, through a simple unification + alpha-substitution algorithm. The compiler would then enforce that if `f` calls `g`, `unify(bound(g)) ⊆ -unify(bound(f))` (by structural equality). +unify(bound(f))` (by structural equality): + + ExpandBooleanAnd: + P && Q + ────── + P + Q + SubstituteEquality: + P(a) + a = b + ───── + P(b) + +These rules are "exhausting" (recursing downwards the tree and decreasing the +structure), and thus it is possible to check, in this language, that `a ⇒ b` +relatively quickly (`O(n)`). + +More rules can be added in the future (e.g., reflexive equality, common true +statements, etc.). It is however important to preserve the "sequential +property" (that is, each step is a reduction, not an expansion), allowing one +to check the implication in linear time. This is done under type unification. Thus, we only need to check the bounds at the top level. +#### An example + +We will quickly give an example of a possible proof. Say we want to show that +`x = b && x < a ⇒ b < a`. Starting with the left hand side, we can sequentially +prove this, by simple unification (which already exists in the Rust type +checker): + + x = b && x < a + ∴ x = b (ExpandBooleanAnd) + x < a + ∴ b < a (SubstituteEquality) + ¯¯¯¯¯ + +### Contradictive or unsatisfiable bounds + +Contradictive or unsatisfiable bounds (like `a < b, b < a`) cannot be detected, +since such a thing would be undecidable. + +These bounds doesn't break anything, they are simply malformed and unreachable. + +Take `a < b, b < a` as an example. We know the values of `a` and `b`, we can +thus calculate the two bounds, which will clearly fail. We cannot, however, +stop such malformed bounds in _declarations_ and _function definitions_, due to +mathematical limitations. + ## The grammar These extensions expand the type grammar to: From 60467c2c18d16b38b1a438425ae29076beb9ef04 Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 11:58:32 +0200 Subject: [PATCH 14/34] Add subsection of 'motivation' dedicated to examples, at exit-point identities --- text/0000-pi-types.md | 126 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 122 insertions(+), 4 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index d3c87c5f390..90a61ba837a 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -54,6 +54,113 @@ type level arithmetics, lattice types). It allows for creating powerful abstractions without type-level hackery. +## Examples + +### Bounded integers/interval arithmetics + +One can define the so called "bounded integers" (integers which carries an +upper and lower bound, checked at compile time): + +```rust +use std::ops; + +/// A bounded integer. +/// +/// This has two value parameter, respectively representing an upper and a lower bound. +pub struct BoundedInt + where lower <= upper { + /// The inner runtime value. + n: usize, +} + +// To see how this holds the `where` clause above, see the section on `identities`. +impl BoundedInt { + fn new() -> Self { + BoundedInt { + n: n, + } + } +} + +/// Addition of two `BoundedInt` will simply add their bounds. +/// +/// We check for overflow making it statically overflow-free calculations. +impl ops::Add> for BoundedInt + where lower_a <= upper_a, + lower_b <= upper_b, + // Check for overflow by some `const fn`. + is_overflow_safe(upper_a, upper_b) { + // These parameters are constant expression. + type Output = BoundedInt; + + fn add(self, rhs: BoundedInt) -> Self::Output { + BoundedInt { + n: self.n + rhs.n, + } + } +} + +impl From> for BoundedInt + where lower_a <= upper_a, + lower_b <= upper_b, + // We will only extend the bound, never shrink it without runtime + // checks, thus we add this clause: + lower_b <= lower_a && upper_b >= upper_a { + fn from(from: BoundedInt) -> Self { + BoundedInt { + n: from.n, + } + } +} +``` + +### Homogeneous varargs + +We can use arbitrarily length arrays to simulate homogeneous varargs: + +```rust +fn my_func(args: [u32; n]) { /* whatever */ } + +my_func([1, 2, 3]); +my_func([1, 2, 3, 4]); +``` + +### Array generics + +Currently libcore only implements various traits up to arrays of length 32. +This allows for implementing them for arrays of arbitrary length: + +```rust +impl Clone for [T; n] { + fn clone(&self) -> [T; n] { + // Clone it... + } +} +``` + +### Statically checked indexing + +```rust +use std::ops; + +impl ops::Index> for [T; n] { + type Output = T; + + fn index(&self, ind: BoundedInt<0, n>) -> &T { + unsafe { + // This is safe due to the bound on `ind`. + self.unchecked_index(*ind) + } + } +} +``` + # Detailed design [design]: #detailed-design @@ -169,14 +276,25 @@ These rules are "exhausting" (recursing downwards the tree and decreasing the structure), and thus it is possible to check, in this language, that `a ⇒ b` relatively quickly (`O(n)`). -More rules can be added in the future (e.g., reflexive equality, common true -statements, etc.). It is however important to preserve the "sequential -property" (that is, each step is a reduction, not an expansion), allowing one -to check the implication in linear time. +More rules can be added in the future. It is however important to preserve the +"sequential property" (that is, each step is a reduction, not an expansion), +allowing one to check the implication in linear time. This is done under type unification. Thus, we only need to check the bounds at the top level. +#### (Optional extension:) "Exit-point" identities + +These are simply identities which always holds. Whenever the compiler reach one +of these in the `where` clause unfolding, it returns "True": + + LeqReflexive: + f(x) <= f(x) + GeqReflexive: + f(x) >= f(x) + EqReflexive: + f(x) = f(x) + #### An example We will quickly give an example of a possible proof. Say we want to show that From 468f16ad5004742703dba5792bb4fe4732c6e80d Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 12:07:48 +0200 Subject: [PATCH 15/34] Expand motivation with aims --- text/0000-pi-types.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 90a61ba837a..3dd11fb4840 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -54,6 +54,21 @@ type level arithmetics, lattice types). It allows for creating powerful abstractions without type-level hackery. +## What we want, and what we don't want + +We have to be very careful to avoid certain things, while still preserving the core features: + +1. Ability to use, manipulate, and constraint values at type-level. +2. The ability to use said values on expression-level (runtime). + +Yet, we do not want: + +1. SMT-solvers, due to not only undecidability (note, although, that SAT is + decidable) and performance, but the complications it adds to `rustc`. +2. Monomorphisation-time errors, i.e. errors that happens during codegen of + generic functins. We try to avoid adding _more_ of these (as noted by + petrochenkov, these [already exists](https://github.com/rust-lang/rfcs/pull/1657#discussion_r68202733)) + ## Examples ### Bounded integers/interval arithmetics From a01250c8257c0f93cf1bce8e4094cb366cc5e13d Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 12:18:46 +0200 Subject: [PATCH 16/34] Double negation and division by zero handling --- text/0000-pi-types.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 3dd11fb4840..c5d53830bb3 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -286,6 +286,10 @@ unify(bound(f))` (by structural equality): a = b ───── P(b) + DoubleNegation: + ¬¬x + ─── + x These rules are "exhausting" (recursing downwards the tree and decreasing the structure), and thus it is possible to check, in this language, that `a ⇒ b` @@ -309,6 +313,8 @@ of these in the `where` clause unfolding, it returns "True": f(x) >= f(x) EqReflexive: f(x) = f(x) + NegFalseIsTrue: + ¬false #### An example @@ -376,6 +382,12 @@ Since not all parameters' edges are necessarily the identity function, dispatching these would be undecidable. A way to solve this problem is to introduce some syntax allowing to specify the `impl` parameters. +## Division by zero + +If some function contain a constexpr divisor, dependent on some value parameter +of the function, that is (`a / f(x)`), the compiler must ensure that the bound +implies that `f(x) != 0`. + ## An example This is the proposed syntax: From 817ec487af1ff09ae50e3d19c2b9c0c985c22baa Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 12:40:51 +0200 Subject: [PATCH 17/34] Prove decidability --- text/0000-pi-types.md | 35 +++++++++++++++++++++++++++-------- 1 file changed, 27 insertions(+), 8 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index c5d53830bb3..50e54fdff1b 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -291,9 +291,9 @@ unify(bound(f))` (by structural equality): ─── x -These rules are "exhausting" (recursing downwards the tree and decreasing the +These rules are "eliminatory" (recursing downwards the tree and decreasing the structure), and thus it is possible to check, in this language, that `a ⇒ b` -relatively quickly (`O(n)`). +relatively quickly (`O(n)`). For a proof of see the section below. More rules can be added in the future. It is however important to preserve the "sequential property" (that is, each step is a reduction, not an expansion), @@ -302,19 +302,37 @@ allowing one to check the implication in linear time. This is done under type unification. Thus, we only need to check the bounds at the top level. +#### Decidability of this rule set + +One can show this by considering each case: + +1. `ExpandBooleanAnd` eliminates `{P && Q} ⊢ {P, Q}`. The right hand side's + depth is `max(dep(P), dep(Q))`, which is smaller than the original, + `max(dep(P), dep(Q)) + 1` +2. `SubstituteEquality` eliminates `{a = b, P} ⊢ {P[b/a]}`, which is an + elimination, since `dep(P) + 1 > dep(P[b/a]) = dep(P)`. +3. `DoubleNegation` eliminates `{¬¬x} ⊢ {x}`, which is an elimination, since + `dep(x) + 2 > dep(x)`. + #### (Optional extension:) "Exit-point" identities These are simply identities which always holds. Whenever the compiler reach one of these in the `where` clause unfolding, it returns "True": LeqReflexive: - f(x) <= f(x) + f(x) <= f(x) for x primitive integer GeqReflexive: - f(x) >= f(x) + f(x) >= f(x) for x primitive integer EqReflexive: f(x) = f(x) NegFalseIsTrue: ¬false + TrueAndTrue: + true && true + OrTrue1: + P || true + OrTrue2: + true || P #### An example @@ -323,10 +341,11 @@ We will quickly give an example of a possible proof. Say we want to show that prove this, by simple unification (which already exists in the Rust type checker): - x = b && x < a - ∴ x = b (ExpandBooleanAnd) - x < a - ∴ b < a (SubstituteEquality) + x = b && ¬¬(x < a) + ∴ x = b (ExpandBooleanAnd) + ¬¬(x < a) + ∴ ¬¬(b < a) (SubstituteEquality) + ∴ b < a (DoubleNegation) ¯¯¯¯¯ ### Contradictive or unsatisfiable bounds From d46f550dc4634c75ab590118178d4ee9e7928539 Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 13:24:53 +0200 Subject: [PATCH 18/34] Thanks for the feedback, gnzlbg, killercup, and kennytm --- text/0000-pi-types.md | 114 +++++++++++++++++++++++++++++------------- 1 file changed, 78 insertions(+), 36 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 50e54fdff1b..6c769201bab 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -38,7 +38,7 @@ time. ## Type checking -Type checking is done by using a transitive rule, such that `where` bounds must +Type checking is done by using a [transitive rule](#transitivity-of-bounds), such that `where` bounds must be implied by the caller. # Motivation @@ -49,8 +49,8 @@ length arrays. The current proposals are often limited to integers or even lack of value maps, and other critical features. There is a whole lot of other usecases as well. These allows certain often -requested features to live in standalone libraries (e.g., bounded-integers, -type level arithmetics, lattice types). +requested features to live in standalone libraries (e.g., [bounded-integers](#bounded-integersinterval-arithmetics), +[type level numerals](#array-generics), [statically checked indexing](#statically-checked-indexing), lattice types). It allows for creating powerful abstractions without type-level hackery. @@ -66,14 +66,14 @@ Yet, we do not want: 1. SMT-solvers, due to not only undecidability (note, although, that SAT is decidable) and performance, but the complications it adds to `rustc`. 2. Monomorphisation-time errors, i.e. errors that happens during codegen of - generic functins. We try to avoid adding _more_ of these (as noted by + generic functions. We try to avoid adding _more_ of these (as noted by petrochenkov, these [already exists](https://github.com/rust-lang/rfcs/pull/1657#discussion_r68202733)) ## Examples ### Bounded integers/interval arithmetics -One can define the so called "bounded integers" (integers which carries an +One can define the so called "bounded integers" (integers which carry an upper and lower bound, checked at compile time): ```rust @@ -164,10 +164,10 @@ impl Clone for [T; n] { ```rust use std::ops; -impl ops::Index> for [T; n] { +impl ops::Index> for [T; n] { type Output = T; - fn index(&self, ind: BoundedInt<0, n>) -> &T { + fn index(&self, ind: BoundedInt<0, n - 1>) -> &T { unsafe { // This is safe due to the bound on `ind`. self.unchecked_index(*ind) @@ -181,15 +181,13 @@ impl ops::Index> for [T; n] { ## The new value-type construct, `const` -The first construct, we will introduce one allowing us to declare `ε → τ` -constructors (value dependent types). +Declaring a parameter `const x: T` allows using `x` in both an expression context +(as a value of type `T`) and a type context (as a type parameter). In a sense, +const "bridges" the world between values and types, since it allows us to +declare value dependent types ([`ε → τ` constructors](https://en.wikipedia.org/wiki/Dependent_type)). -In a sense, `const` "bridges" between types and values. - -Declaring a parameter `const x: T` allows use in both expression context (as a -value of type `T`) and type context (as a type parameter). - -Such a parameter is declared, like type parameters, in angle brackets. +Such a parameter is declared, like type parameters, in angle brackets (e.g. +`struct MyStruct`). The expr behavior is described as: @@ -198,18 +196,20 @@ The expr behavior is described as: ────────────── Π ⊢ x: T +In human language, this simply means that one can use a constant parameter, +`const x: T`, in expression context, as a value of type `T`. + On the type level, we use the very same semantics as the ones generic parameters currently follows. ## `const fn`s as Π-constructors We are interested in value dependency, but at the same time, we want to avoid -complications such as SMT-solvers and so on. +complications such as [SMT-solvers](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories). -Thus, we follow a purely constructible model, by using `const fn`s. - -This allows one to take some const parameter and map it by some arbitrary, pure -function, following the rules described in [RFC 0911](https://github.com/rust-lang/rfcs/blob/master/text/0911-const-fn.md#detailed-design). +We achieve this by `const fn`, which allows us to take some const parameter and +map it by some arbitrary, pure function, following the rules described in [RFC +0911](https://github.com/rust-lang/rfcs/blob/master/text/0911-const-fn.md#detailed-design). ## Type inference @@ -256,8 +256,8 @@ let l = foo::<_, [1, 2, 3, 4, 5, 6]>(); ## `where` clauses Often, it is wanted to have some statically checked clause satisfied by the -constant parameters. To archive this, in a reasonable manner, we use const -exprs, returning a boolean. +constant parameters (e.g., for the sake of compile-time bound checking). To +archive this, in a reasonable manner, we use const exprs, returning a boolean. We allow such constexprs in `where` clauses of functions. Whenever the function is invoked given constant parameters ``, the compiler @@ -271,9 +271,12 @@ bounds must imply the invoked functions' bounds: ### Transitivity of bounds. We require a bound of a function to imply the bounds of the functions it calls, -through a simple unification + alpha-substitution algorithm. +through a simple reductive, unification algorithm. In particular, this means +that a statement is reduced by some specified rules (see below), that ensures +termination. A statement implies another statement, if the set of statements it +reduces to is a superset of the other statement's reduction set. -The compiler would then enforce that if `f` calls `g`, `unify(bound(g)) ⊆ +The compiler would enforce that if `f` calls `g`, `unify(bound(g)) ⊆ unify(bound(f))` (by structural equality): ExpandBooleanAnd: @@ -364,7 +367,7 @@ mathematical limitations. These extensions expand the type grammar to: - T = scalar (i32, u32, ...) // Scalars + T = scalar (...) // Scalars (basic types s.a. primitive types) | X // Type variable | Id // Nominal type (struct, enum) | &r T // Reference (mut doesn't matter here) @@ -392,14 +395,18 @@ possible extensions, see below). To find the right implementation, we use the data from the type inference (see the inference rules above). Since the parameters are, in fact, not much -semantically different from normal generic parameters, we can resolve it is a -normal manner. +semantically different from normal generic parameters, we can resolve it in a +normal manner (that is, by treating the value parameters as if they were actual +type parameters). -Likewise are disjointness checks based on structural equality. +Likewise are disjointness checks based on structural equality. That is, we only +care about structural equality, not `Eq` or something else. This allows us to +reason more rigorously about the behavior. Since not all parameters' edges are necessarily the identity function, dispatching these would be undecidable. A way to solve this problem is to -introduce some syntax allowing to specify the `impl` parameters. +introduce some syntax allowing to specify the `impl` parameters. This is not +something we consider in this proposal, but a secondary RFC can introduce these. ## Division by zero @@ -463,19 +470,54 @@ This RFC aims to keep a "symmetric" syntax to the current construct, giving an intuitive behavior, however there are multiple things that are worth explaining and/or clearing up: -1. What are Π-types? How are they different from those from other languages? +Q: What are dependent types? + +A: Dependent types are types, which _depends_ on values, instead of types. For + example, [T; 3], is dependent since it depends on the value, `3`, for + constructing the type. Dependent types, in a sense, is similar to normal + generics, where types can depend on other types (e.g. `Vec`), whereas + dependent types depends on values. + +Q: We achieve this by using const fns, which allow us to take ... -2. One will have to understand what `const fn`s are and how they are linked to - Π-types. +A: Various other languages have dependent type systems. Strictly speaking, all + that is required for a dependent type system is value-to-type constructors, + although some languages (coq, agda, etc.) goes a step further and remove the + boundary between value and type. Unfortunately, as cool as it sounds, it has + some severe disadvantages: most importantly, the type checking becomes + undecidable. Often you would need some form of theorem prover to type check + the program, and those has their limitations too. -3. What are the usecases? +Q: What are `const fn` and how is it linked to this RFC? -4. What are the edge cases, and how can one work around those (e.g. failed +A: `const fn` is a function, which can be evaluated at compile time. While it + is currently rather limited, in the future it will be extended (see + [Miri](https://github.com/solson/miri)). You can use constexprs to take one + type-level value, and non-trivially calculate a new one. + +Q: What are the usecases? + +A: There are many usecases for this. The most prominent one, perhaps, is the + generically sized arrays. Dependent types allows one to lift the length of the + array up to the type-level, effectively allowing one to parameterize over them. + +Q: What are the edge cases, and how can one work around those (e.g. failed unification)? -5. How can I use this to create powerful abstractions? +A: If you use this a lot, you will likely encounter edge cases, where the + compiler isn't able to figure out implication, since the reductive rules are + dumb. However, there is hope! Say your function calls some function, where + the compiler cannot prove the bound. You can work around this by simply + adding the called function's `where` bound to the caller's `where` bound. + While, this is a minor annoyance, working around it is relatively easy. + +Q: How can I use this to create powerful abstractions? + +A: ... + +Q: Extensive examples. -6. Extensive examples. +A: Refer to the rest of the RFC. Moreover, we need to "informalize" the rules defined in this RFC. From 54e00aff6789a092f9f0f455dc874c470861be34 Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 13:36:48 +0200 Subject: [PATCH 19/34] "Informalize" the rules --- text/0000-pi-types.md | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 6c769201bab..f01bf6adba7 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -222,6 +222,8 @@ const parameters, by adding an unification relation, simply ────────────── Γ ⊢ T: U +Informally, this means that, you can substitute equal terms (in this case, `const fn` relations). + The relational edge between two const parameters is simple a const fn, which is resolved under unification. @@ -237,9 +239,10 @@ We add an extra rule to improve inference: Γ ⊢ c = x So, if two types share constructor by some Π-constructor, share a value, their -value parameter is equal. +value parameter is equal. Take `a: [u8; 4]` as an example. If we have some +unknown variable `x`, such that `a: [u8; x]`, we can infer that `x = 4`. -This allows us infer: +This allows us infer e.g. array length parameters in functions: ```rust // [T; N] is a constructor, T → usize → 𝓤 (parameterize over T and you get A → 𝓤). @@ -284,16 +287,26 @@ unify(bound(f))` (by structural equality): ────── P Q + +This simply means that `a && b` means `a` and `b`. + SubstituteEquality: P(a) a = b ───── P(b) + +This is an important inference rule, when doing unification. This means that +you can substitute all `a` for all free `b`s, if `a = b`. + DoubleNegation: ¬¬x ─── x +The last rule for now is simply stating that double negation is identity, that +is, `!!a` means that `a` is true. + These rules are "eliminatory" (recursing downwards the tree and decreasing the structure), and thus it is possible to check, in this language, that `a ⇒ b` relatively quickly (`O(n)`). For a proof of see the section below. From 5718d4be01a3b720f6e4936f130e7f15d969a122 Mon Sep 17 00:00:00 2001 From: Pascal Hertleif Date: Thu, 23 Jun 2016 14:39:00 +0200 Subject: [PATCH 20/34] Fix some typos in Pi Types RFCs Also changes the formatting of the FAQ a bit and makes all questions questions :) --- text/0000-pi-types.md | 72 ++++++++++++++++++++++--------------------- 1 file changed, 37 insertions(+), 35 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index f01bf6adba7..827a59819b2 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -483,54 +483,56 @@ This RFC aims to keep a "symmetric" syntax to the current construct, giving an intuitive behavior, however there are multiple things that are worth explaining and/or clearing up: -Q: What are dependent types? +**What are dependent types?** -A: Dependent types are types, which _depends_ on values, instead of types. For - example, [T; 3], is dependent since it depends on the value, `3`, for - constructing the type. Dependent types, in a sense, is similar to normal - generics, where types can depend on other types (e.g. `Vec`), whereas - dependent types depends on values. +Dependent types are types, which _depend_ on values, instead of types. For +example, [T; 3], is dependent since it depends on the value, `3`, for +constructing the type. Dependent types, in a sense, are similar to normal +generics, where types can depend on other types (e.g. `Vec`), whereas +dependent types depend on values. -Q: We achieve this by using const fns, which allow us to take ... +**We achieve this by using const fns, which allow us to take ...** -A: Various other languages have dependent type systems. Strictly speaking, all - that is required for a dependent type system is value-to-type constructors, - although some languages (coq, agda, etc.) goes a step further and remove the - boundary between value and type. Unfortunately, as cool as it sounds, it has - some severe disadvantages: most importantly, the type checking becomes - undecidable. Often you would need some form of theorem prover to type check - the program, and those has their limitations too. +Various other languages have dependent type systems. Strictly speaking, all +that is required for a dependent type system is value-to-type constructors, +although some languages (coq, agda, etc.) goes a step further and remove the +boundary between value and type. Unfortunately, as cool as it sounds, it has +some severe disadvantages: most importantly, the type checking becomes +undecidable. Often you would need some form of theorem prover to type check +the program, and those has their limitations too. -Q: What are `const fn` and how is it linked to this RFC? +**Q: What are `const fn` and how is it linked to this RFC?** -A: `const fn` is a function, which can be evaluated at compile time. While it - is currently rather limited, in the future it will be extended (see - [Miri](https://github.com/solson/miri)). You can use constexprs to take one - type-level value, and non-trivially calculate a new one. +`const fn` is a function, which can be evaluated at compile time. While it +is currently rather limited, in the future it will be extended (see +[Miri](https://github.com/solson/miri)). You can use constexprs to take one +type-level value, and non-trivially calculate a new one. -Q: What are the usecases? +**Q: What are the usecases?** -A: There are many usecases for this. The most prominent one, perhaps, is the - generically sized arrays. Dependent types allows one to lift the length of the - array up to the type-level, effectively allowing one to parameterize over them. +There are many usecases for this. The most prominent one, perhaps, is the +generically sized arrays. Dependent types allows one to lift the length of the +array up to the type-level, effectively allowing one to parameterize over them. -Q: What are the edge cases, and how can one work around those (e.g. failed - unification)? +**Q: What are the edge cases, and how can one work around those (e.g. failed + unification)?** -A: If you use this a lot, you will likely encounter edge cases, where the - compiler isn't able to figure out implication, since the reductive rules are - dumb. However, there is hope! Say your function calls some function, where - the compiler cannot prove the bound. You can work around this by simply - adding the called function's `where` bound to the caller's `where` bound. - While, this is a minor annoyance, working around it is relatively easy. +If you use this a lot, you will likely encounter edge cases, where the +compiler isn't able to figure out implication, since the reductive rules are +dumb. However, there is hope! Say your function calls some function, where +the compiler cannot prove the bound. You can work around this by simply +adding the called function's `where` bound to the caller's `where` bound. +While, this is a minor annoyance, working around it is relatively easy. -Q: How can I use this to create powerful abstractions? +**Q: How can I use this to create powerful abstractions?** -A: ... +... -Q: Extensive examples. +**Q: Can you show some more extensive examples?** -A: Refer to the rest of the RFC. +Refer to the rest of the RFC. + +- - - - Moreover, we need to "informalize" the rules defined in this RFC. From dc4635a2ef074f1271b91c25a695c509ea0cc269 Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 15:54:48 +0200 Subject: [PATCH 21/34] Add section on SMT-solvers, fix gnzlbg's notes --- text/0000-pi-types.md | 108 ++++++++++++++++++++++++++++++++++++------ 1 file changed, 93 insertions(+), 15 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index f01bf6adba7..a0b922b876b 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -83,6 +83,7 @@ use std::ops; /// /// This has two value parameter, respectively representing an upper and a lower bound. pub struct BoundedInt + // Compile time constraints. where lower <= upper { /// The inner runtime value. n: usize, @@ -103,7 +104,8 @@ impl BoundedInt { impl ops::Add> for BoundedInt + const lower_b: usize> ops::Add> for BoundedInt + // We have to satisfy the constraints set out in the struct definition. where lower_a <= upper_a, lower_b <= upper_b, // Check for overflow by some `const fn`. @@ -121,7 +123,7 @@ impl From> for BoundedInt + const lower_b: usize> From> for BoundedInt where lower_a <= upper_a, lower_b <= upper_b, // We will only extend the bound, never shrink it without runtime @@ -161,6 +163,8 @@ impl Clone for [T; n] { ### Statically checked indexing +One can perform simple, interval based, statically checked indexing: + ```rust use std::ops; @@ -176,6 +180,16 @@ impl ops::Index> for [T; n] { } ``` +### Fancy number stuff + +```rust +struct Num; + +trait Divides {} + +impl Divides for Num where b % a == 0 {} +``` + # Detailed design [design]: #detailed-design @@ -235,14 +249,14 @@ We add an extra rule to improve inference: Γ ⊢ x: A Γ ⊢ a: T Γ ⊢ a: T - ────────────── + ──────────── Γ ⊢ c = x So, if two types share constructor by some Π-constructor, share a value, their value parameter is equal. Take `a: [u8; 4]` as an example. If we have some unknown variable `x`, such that `a: [u8; x]`, we can infer that `x = 4`. -This allows us infer e.g. array length parameters in functions: +This allows us to infer e.g. array length parameters in functions: ```rust // [T; N] is a constructor, T → usize → 𝓤 (parameterize over T and you get A → 𝓤). @@ -268,8 +282,8 @@ evaluates this expression, and if it returns `false`, an aborting error is invoked. To sum up, the check happens when typechecking the function calls (that is, -checking if the parameters satisfy the trait bounds, and so on). The caller's -bounds must imply the invoked functions' bounds: +checking if the parameters satisfy the trait bounds). The caller's bounds must +imply the invoked functions' bounds: ### Transitivity of bounds. @@ -332,8 +346,8 @@ One can show this by considering each case: #### (Optional extension:) "Exit-point" identities -These are simply identities which always holds. Whenever the compiler reach one -of these in the `where` clause unfolding, it returns "True": +These are simply identities which always holds. Whenever the compiler reaches one +of these when unfolding the `where` clause, it returns "True": LeqReflexive: f(x) <= f(x) for x primitive integer @@ -369,13 +383,55 @@ checker): Contradictive or unsatisfiable bounds (like `a < b, b < a`) cannot be detected, since such a thing would be undecidable. -These bounds doesn't break anything, they are simply malformed and unreachable. +These bounds don't break anything, they are simply malformed and unreachable. Take `a < b, b < a` as an example. We know the values of `a` and `b`, we can thus calculate the two bounds, which will clearly fail. We cannot, however, stop such malformed bounds in _declarations_ and _function definitions_, due to mathematical limitations. +### SMT-solvers? + +#### What a Rusty SMT-solver would look like + +The simplest and least obstructive SMT-solver is the SAT-based one. SAT is a +class of decision problem, where a boolean formula, with some arbitrary number +of free variables, is determined to be satisfiable or not. Obviously, this is +decidable (bruteforcing is the simplest algorithm, since the search space is +finite, bruteforcing is guaranteed to terminate). + +SAT is NP-complete, and even simple statements such as `x + y = y + x` can take +a long time to prove. A non-SAT (symbolic) SMT-solver is strictly more +expressive, due to not being limited to finite integers, however first-order +logic is not generally decidable, and thus such solvers are often returning +"Satisfiable", "Not satisfiable", "Not known". + +In general, such algorithms are either slow or relatively limited. An example +of such a limitation is in the [Dafny +language](https://github.com/Microsoft/dafny), where programs exist that +compile when having the bound `a \/ b`, but fails when having the bound `b \/ +a`. This can be relatively confusing the user. + +It is worth noting that the technology on this area is still improving, and +these problems will likely be marginalized in a few years. + +Another issue which is present in Rust, is that you don't have any logical +(invariant) information about the return values. Thus, a SMT-solver would work +relatively poorly (if at all) non-locally (e.g. user defined functions). + +That issue is not something that prevents us from adopting a SMT-solver, but it +limits the experience with having one. + +#### Backwards compatibility + +While I am against adding SMT-solvers to `rustc`, it is worth noting that this +change is, in fact, compatible with future extensions for more advanced theorem +provers. + +The only catch with adding a SMT-solver is that errors on unsatisfiability or +contradictions would be a breaking change. By throwing a warning instead, you +essentially get the same functionality. + ## The grammar These extensions expand the type grammar to: @@ -404,7 +460,8 @@ Note that the `const` syntax is only used when declaring the parameter. ## `impl` unification Only one `where` bound can be specified on each disjoint implementations (for -possible extensions, see below). +possible extensions, see below). In other words, no overlap is allowed, even if +the `where` bounds are mutually exclusive. To find the right implementation, we use the data from the type inference (see the inference rules above). Since the parameters are, in fact, not much @@ -416,6 +473,21 @@ Likewise are disjointness checks based on structural equality. That is, we only 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, + +```rust +impl Trait for Struct where some_fn(x) +``` + +is, when checking for implementation uniqueness, semantically behaving like + +```rust +impl Trait for Struct +``` + +since we cannot prove injectivity. Note that this is only about behavior under +_uniqueness checking_. + Since not all parameters' edges are necessarily the identity function, dispatching these would be undecidable. A way to solve this problem is to introduce some syntax allowing to specify the `impl` parameters. This is not @@ -499,7 +571,7 @@ A: Various other languages have dependent type systems. Strictly speaking, all boundary between value and type. Unfortunately, as cool as it sounds, it has some severe disadvantages: most importantly, the type checking becomes undecidable. Often you would need some form of theorem prover to type check - the program, and those has their limitations too. + the program, and those have their limitations too. Q: What are `const fn` and how is it linked to this RFC? @@ -510,9 +582,10 @@ A: `const fn` is a function, which can be evaluated at compile time. While it Q: What are the usecases? -A: There are many usecases for this. The most prominent one, perhaps, is the - generically sized arrays. Dependent types allows one to lift the length of the - array up to the type-level, effectively allowing one to parameterize over them. +A: There are many usecases for this. The most prominent one, perhaps, is + abstracting over generically sized arrays. Dependent types allows one to lift + the length of the array up to the type-level, effectively allowing one to + parameterize over them. Q: What are the edge cases, and how can one work around those (e.g. failed unification)? @@ -570,7 +643,12 @@ _arguments_ instead of constant _parameters_. This allows for bounds on e.g. fn do_something(const x: u32) -> u32 where x < 5 { x } ``` -From the callers perspective, this one is especially nice to work with. +From the callers perspective, this one is especially nice to work with, however +it can lead to confusion about mixing up constargs and runtime args. One +possible solution is to segregate the constargs from the rest arguments by a +`;` (like in array types). + +Another way to semantically justify such a change is by the [`Const` type constructor](#an-extension-a-constexpr-type-constructor) ### Square brackets From 4e36bedd49a043a8b34d27075c375cb5be26939f Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 15:58:07 +0200 Subject: [PATCH 22/34] Add remark --- text/0000-pi-types.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index e18ce7e04c3..248fc51ba10 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -392,6 +392,8 @@ mathematical limitations. ### SMT-solvers? +This RFC doesn't propose such thing, but future possibilities are worth discussing: + #### What a Rusty SMT-solver would look like The simplest and least obstructive SMT-solver is the SAT-based one. SAT is a From b555120abc1d933da7bcbecc1c9d0bec17444510 Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 17:16:03 +0200 Subject: [PATCH 23/34] Add section on possible extensions --- text/0000-pi-types.md | 151 +++++++++++++++++++++++++++++++++--------- 1 file changed, 120 insertions(+), 31 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 248fc51ba10..577d6440892 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -297,12 +297,12 @@ The compiler would enforce that if `f` calls `g`, `unify(bound(g)) ⊆ unify(bound(f))` (by structural equality): ExpandBooleanAnd: - P && Q + P ∧ Q ────── P Q -This simply means that `a && b` means `a` and `b`. +This simply means that `a ∧ b` means `a` and `b`. SubstituteEquality: P(a) @@ -318,8 +318,8 @@ you can substitute all `a` for all free `b`s, if `a = b`. ─── x -The last rule for now is simply stating that double negation is identity, that -is, `!!a` means that `a` is true. +This rule is simply stating that double negation is identity, that is, `!!a` +means that `a` is true. These rules are "eliminatory" (recursing downwards the tree and decreasing the structure), and thus it is possible to check, in this language, that `a ⇒ b` @@ -336,7 +336,7 @@ the top level. One can show this by considering each case: -1. `ExpandBooleanAnd` eliminates `{P && Q} ⊢ {P, Q}`. The right hand side's +1. `ExpandBooleanAnd` eliminates `{P ∧ Q} ⊢ {P, Q}`. The right hand side's depth is `max(dep(P), dep(Q))`, which is smaller than the original, `max(dep(P), dep(Q)) + 1` 2. `SubstituteEquality` eliminates `{a = b, P} ⊢ {P[b/a]}`, which is an @@ -344,34 +344,16 @@ One can show this by considering each case: 3. `DoubleNegation` eliminates `{¬¬x} ⊢ {x}`, which is an elimination, since `dep(x) + 2 > dep(x)`. -#### (Optional extension:) "Exit-point" identities - -These are simply identities which always holds. Whenever the compiler reaches one -of these when unfolding the `where` clause, it returns "True": - - LeqReflexive: - f(x) <= f(x) for x primitive integer - GeqReflexive: - f(x) >= f(x) for x primitive integer - EqReflexive: - f(x) = f(x) - NegFalseIsTrue: - ¬false - TrueAndTrue: - true && true - OrTrue1: - P || true - OrTrue2: - true || P +In fact, this set of rule is strictly reductive (like equality-based unification). #### An example We will quickly give an example of a possible proof. Say we want to show that -`x = b && x < a ⇒ b < a`. Starting with the left hand side, we can sequentially +`x = b ∧ x < a ⇒ b < a`. Starting with the left hand side, we can sequentially prove this, by simple unification (which already exists in the Rust type checker): - x = b && ¬¬(x < a) + x = b ∧ ¬¬(x < a) ∴ x = b (ExpandBooleanAnd) ¬¬(x < a) ∴ ¬¬(b < a) (SubstituteEquality) @@ -551,6 +533,113 @@ fn main() { } ``` +# Experimental extensions open to discussion + +## Candidates for additional rules + + RewriteOr: + P ∨ Q + ────────── + ¬(¬P ∧ ¬Q) + +This rule states that if `a` nor `b`, none of them can be true. It allows us to +rewrite OR in terms of NOT and AND. + +`RewriteOr` does not reduce depth. In fact, it does increase depth, but that +rule is only triggered by `∨`, which no other rules infer. Thus, there is no +way, we can enter a cycle, since `RewriteOr(P)` is a reduction of `P` with +respect to `∨`. + + DisjunctiveSyllogism: + ¬(P ∧ Q) + P + ───── + ¬Q + +Basically, this states that if two propositions are mutually exclusive (that +is, not both of them can be true), and one of them is true, the other must be +false, due to being disjunctive. + +This is strictly reductive. + +Now let's go funky: + + AdditiveCancelationRR: + a + c = b + c + ───────────── + a = b + AdditiveCancelationLL: + c + a = c + b + ───────────── + a = b + AdditiveCancelationRL: + a + c = c + b + ───────────── + a = b + AdditiveCancelationLR: + c + a = b + c + ───────────── + a = b + MultiplicativeCancelationRR: + ac = bc + ───────────── + a = b + MultiplicativeCancelationLL: + ca = cb + ───────────── + a = b + MultiplicativeCancelationRL: + ac = cb + ───────────── + a = b + MultiplicativeCancelationLR: + ca = bc + ───────────── + a = b + +These are all reductive. + +## Expression reduction rules + +We might want to have expression reduction rules beyond the basic const +folding. This would allow certain symbolic comparation to improve. + + DistributiveMultiplicationLhs: + c(a + b) ↦ ca + cb + DistributiveMultiplicationRhs: + (a + b)c ↦ ca + cb + +This is simply the distributive property of multiplication. + + AdditionLeftAssociate: + a + (b + c) ↦ (a + b) + c + MultiplicationLeftAssociate: + a(bc) ↦ (ab)c + +This rules allows us to observe that `a(bc)` is no different from `(ab)c` + +All these rules are reductive. + +## "Exit-point" identities + +These are simply identities which always holds. Whenever the compiler reaches one +of these when unfolding the `where` clause, it returns "True": + + LeqReflexive: + f(x) <= f(x) for x primitive integer + GeqReflexive: + f(x) >= f(x) for x primitive integer + EqReflexive: + f(x) = f(x) + NegFalseIsTrue: + ¬false + TrueAndTrue: + true ∧ true + OrTrue1: + P ∨ true + OrTrue2: + true ∨ P + # How we teach this This RFC aims to keep a "symmetric" syntax to the current construct, giving an @@ -575,21 +664,21 @@ some severe disadvantages: most importantly, the type checking becomes undecidable. Often you would need some form of theorem prover to type check the program, and those have their limitations too. -**Q: What are `const fn` and how is it linked to this RFC?** +**What are `const fn` and how is it linked to this RFC?** `const fn` is a function, which can be evaluated at compile time. While it is currently rather limited, in the future it will be extended (see [Miri](https://github.com/solson/miri)). You can use constexprs to take one type-level value, and non-trivially calculate a new one. -**Q: What are the usecases?** +**What are the usecases?** There are many usecases for this. The most prominent one, perhaps, is abstracting over generically sized arrays. Dependent types allows one to lift the length of the array up to the type-level, effectively allowing one to parameterize over them. -**Q: What are the edge cases, and how can one work around those (e.g. failed +**What are the edge cases, and how can one work around those (e.g. failed unification)?** If you use this a lot, you will likely encounter edge cases, where the @@ -599,11 +688,11 @@ the compiler cannot prove the bound. You can work around this by simply adding the called function's `where` bound to the caller's `where` bound. While, this is a minor annoyance, working around it is relatively easy. -**Q: How can I use this to create powerful abstractions?** +**How can I use this to create powerful abstractions?** ... -**Q: Can you show some more extensive examples?** +**Can you show some more extensive examples?** Refer to the rest of the RFC. From 892e3d68d75cb36d4eaa2226ed9954f230d5380c Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 17:24:33 +0200 Subject: [PATCH 24/34] Fix title on the second question --- text/0000-pi-types.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 577d6440892..c6b9eb80380 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -537,6 +537,10 @@ fn main() { ## Candidates for additional rules +Currently, the set of rules is rather conservative for rewriting. To make it +easier to work with, one can add multiple new reductive rules, at the expense +of implementation complexity: + RewriteOr: P ∨ Q ────────── @@ -654,7 +658,7 @@ constructing the type. Dependent types, in a sense, are similar to normal generics, where types can depend on other types (e.g. `Vec`), whereas dependent types depend on values. -**We achieve this by using const fns, which allow us to take ...** +**How does this differ from other languages' implementations of dependent types?** Various other languages have dependent type systems. Strictly speaking, all that is required for a dependent type system is value-to-type constructors, From 754b94418fb619863efdf70754e8e19dd34a502a Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 21:06:06 +0200 Subject: [PATCH 25/34] Add section on structural equality, add symbolic implication --- text/0000-pi-types.md | 77 +++++++++++++++++++++++++++++-------------- 1 file changed, 53 insertions(+), 24 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index c6b9eb80380..8343603b1e5 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -293,7 +293,7 @@ that a statement is reduced by some specified rules (see below), that ensures termination. A statement implies another statement, if the set of statements it reduces to is a superset of the other statement's reduction set. -The compiler would enforce that if `f` calls `g`, `unify(bound(g)) ⊆ +The compiler would enforce that if `f` calls `g`, `unify(bound(g)) ⊆ unify(bound(f))` (by structural equality): ExpandBooleanAnd: @@ -535,6 +535,27 @@ fn main() { # Experimental extensions open to discussion +## Structural equality will prevail! + +When `const fn` methods arrive, we can extend the concept of structural +equality beyond the "simple" types (e.g., vectors). + +Structural equality, in this case, is defined as an equivalence relation, which +allows substitution without changing semantics. + +This trat should be unsafe, and defined as + +```rust +unsafe trait StructuralEq { + const fn structural_eq(&self, &Self) -> bool; +} +``` + +This allows us to compare values at type level without loosing the substitution +property. + +Such a thing is unevitable, if we want to be able depend on non-structural values. + ## Candidates for additional rules Currently, the set of rules is rather conservative for rewriting. To make it @@ -644,6 +665,26 @@ of these when unfolding the `where` clause, it returns "True": OrTrue2: true ∨ P +### A constexpr type constructor + +Add some language item type constructor, `Const`, allowing for constructing +a constexpr-only types. + +`x: T` can coerce into `Const` if `x` is constexpr. Likewise, can `Const` +coerce into `T`. + +```rust +fn do_something(x: Const) -> u32 { x } + +struct Abc { + constfield: Const, +} +``` + +It is unclear how it plays together with `where` bounds. + +The pro is that it adds ability to implement e.g. constant indexing, `Index>`. + # How we teach this This RFC aims to keep a "symmetric" syntax to the current construct, giving an @@ -683,7 +724,7 @@ the length of the array up to the type-level, effectively allowing one to parameterize over them. **What are the edge cases, and how can one work around those (e.g. failed - unification)?** + unification)?** If you use this a lot, you will likely encounter edge cases, where the compiler isn't able to figure out implication, since the reductive rules are @@ -722,6 +763,14 @@ Another drawback is the lack of implication proves. # Alternatives [alternatives]: #alternatives +## Use purely symbolic `where` clause checking + +We can simplify things somewhat, by using a purely symbolic model of +implication. Say that a set of clause, `A`, implies a set of clause `B`, iff. +`B ⊆ A`. + +## SMT + Use full SMT-based dependent types. These are more expressive, but severely more complex as well. @@ -767,36 +816,16 @@ fn do_something() -> u32 where x < 5 { x } do_something::<2>(); ``` -### An extension: A constexpr type constructor - -Add some language item type constructor, `Const`, allowing for constructing -a constexpr-only types. - -`x: T` can coerce into `Const` if `x` is constexpr. Likewise, can `Const` -coerce into `T`. - -```rust -fn do_something(x: Const) -> u32 { x } - -struct Abc { - constfield: Const, -} -``` - -It is unclear how it plays together with `where` bounds. - -The pro is that it adds ability to implement e.g. constant indexing, `Index>`. - ### `with` instead of `where` Some have raised concerns of mixing things up there. Thus one can use the syntax `with` to denote bounds instead. -### Lazily type check without transitivity rule +## Lazily type check without transitivity rule Simply evaluate the bounds when calling. Remove the requirement of implication. -### Allow multiple implementation bounds +## Allow multiple implementation bounds Allow overlapping implementations carrying bounds, such that only one of the conditions may be true under monomorphization. From c7a2f28264e7d6bacee25f9111be8f682130f813 Mon Sep 17 00:00:00 2001 From: ticki Date: Thu, 23 Jun 2016 21:29:55 +0200 Subject: [PATCH 26/34] Fix structural equality section --- text/0000-pi-types.md | 60 ++++++++++++++++++++++++------------------- 1 file changed, 34 insertions(+), 26 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 8343603b1e5..02101b21c6d 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -285,7 +285,23 @@ To sum up, the check happens when typechecking the function calls (that is, checking if the parameters satisfy the trait bounds). The caller's bounds must imply the invoked functions' bounds: -### Transitivity of bounds. +## Structural equality + +Structural equality plays a key role in type checking of dependent types. + +Structural equality, in this case, is defined as an equivalence relation, which +allows substitution without changing semantics. + +Any constant parameter must have the `structural_match` property as defined in +[RFC #1445](https://github.com/rust-lang/rfcs/pull/1445). This property, added +through the `#[structural_match]` attribute, essentially states that the `Eq` +implementation is structural. + +Without this form of equality, substitution wouldn't be possible, and thus +typechecking an arbitrarily value-depending type constructor would not be +possible. + +### Transitivity of bounds We require a bound of a function to imply the bounds of the functions it calls, through a simple reductive, unification algorithm. In particular, this means @@ -535,27 +551,6 @@ fn main() { # Experimental extensions open to discussion -## Structural equality will prevail! - -When `const fn` methods arrive, we can extend the concept of structural -equality beyond the "simple" types (e.g., vectors). - -Structural equality, in this case, is defined as an equivalence relation, which -allows substitution without changing semantics. - -This trat should be unsafe, and defined as - -```rust -unsafe trait StructuralEq { - const fn structural_eq(&self, &Self) -> bool; -} -``` - -This allows us to compare values at type level without loosing the substitution -property. - -Such a thing is unevitable, if we want to be able depend on non-structural values. - ## Candidates for additional rules Currently, the set of rules is rather conservative for rewriting. To make it @@ -833,16 +828,29 @@ conditions may be true under monomorphization. # Unresolved questions [unresolved]: #unresolved-questions -What syntax is preferred? +## Syntactical/conventional -How does this play together with HKP? +What syntax is preferred? What should be the naming conventions? Should we segregate the value parameters and type parameters by `;`? -Should disjoint implementations satisfying some bound be allowed? +## Compatibility -Should there be a way to parameterize functions dynamically? +How does this play together with HKP? + +How can one change bounds without breaking downstream? Shall some form of +judgemental OR be added? What API would need to be rewritten to take advantage of Π-types? + +## Features + +Should there be a way to parameterize functions dynamically? + +## Semantics + +Find some edge cases, which can be confusing. + +Are there other rules to consider? From 9573c4d4756cb1533a5dd96d7740eb9d0d6be2b7 Mon Sep 17 00:00:00 2001 From: ticki Date: Fri, 24 Jun 2016 01:02:31 +0200 Subject: [PATCH 27/34] Add alternative with inherited bounds --- text/0000-pi-types.md | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 02101b21c6d..c6457966f3e 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -816,15 +816,28 @@ do_something::<2>(); Some have raised concerns of mixing things up there. Thus one can use the syntax `with` to denote bounds instead. -## Lazily type check without transitivity rule - -Simply evaluate the bounds when calling. Remove the requirement of implication. - ## Allow multiple implementation bounds Allow overlapping implementations carrying bounds, such that only one of the conditions may be true under monomorphization. +## Type/`where` clause checking + +### Lazily type check without transitivity rule + +Simply evaluate the bounds when calling. Remove the requirement of implication. +This introduces errors at monomorphization time. + +### Inheriting `where` clauses + +An interesting idea to investigate is to let functions inherit called +function's `where` clauses. This allows for non-monomorphization, yet +ergonomic, `where` clauses. + +An important symmetry is lost, though: trait bounds in `where` clauses. These +are not inherited, but explicit. A way to avoid this asymmetry, [`with` could +be used](#with-instead-of-where). + # Unresolved questions [unresolved]: #unresolved-questions From 74ef189662b172645d01350e6029e17df89c5d6c Mon Sep 17 00:00:00 2001 From: ticki Date: Fri, 24 Jun 2016 15:01:18 +0200 Subject: [PATCH 28/34] Move the SMT-section --- text/0000-pi-types.md | 96 +++++++++++++++++++++++-------------------- 1 file changed, 52 insertions(+), 44 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index c6457966f3e..214e32a1d1d 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -388,50 +388,6 @@ thus calculate the two bounds, which will clearly fail. We cannot, however, stop such malformed bounds in _declarations_ and _function definitions_, due to mathematical limitations. -### SMT-solvers? - -This RFC doesn't propose such thing, but future possibilities are worth discussing: - -#### What a Rusty SMT-solver would look like - -The simplest and least obstructive SMT-solver is the SAT-based one. SAT is a -class of decision problem, where a boolean formula, with some arbitrary number -of free variables, is determined to be satisfiable or not. Obviously, this is -decidable (bruteforcing is the simplest algorithm, since the search space is -finite, bruteforcing is guaranteed to terminate). - -SAT is NP-complete, and even simple statements such as `x + y = y + x` can take -a long time to prove. A non-SAT (symbolic) SMT-solver is strictly more -expressive, due to not being limited to finite integers, however first-order -logic is not generally decidable, and thus such solvers are often returning -"Satisfiable", "Not satisfiable", "Not known". - -In general, such algorithms are either slow or relatively limited. An example -of such a limitation is in the [Dafny -language](https://github.com/Microsoft/dafny), where programs exist that -compile when having the bound `a \/ b`, but fails when having the bound `b \/ -a`. This can be relatively confusing the user. - -It is worth noting that the technology on this area is still improving, and -these problems will likely be marginalized in a few years. - -Another issue which is present in Rust, is that you don't have any logical -(invariant) information about the return values. Thus, a SMT-solver would work -relatively poorly (if at all) non-locally (e.g. user defined functions). - -That issue is not something that prevents us from adopting a SMT-solver, but it -limits the experience with having one. - -#### Backwards compatibility - -While I am against adding SMT-solvers to `rustc`, it is worth noting that this -change is, in fact, compatible with future extensions for more advanced theorem -provers. - -The only catch with adding a SMT-solver is that errors on unsatisfiability or -contradictions would be a breaking change. By throwing a warning instead, you -essentially get the same functionality. - ## The grammar These extensions expand the type grammar to: @@ -551,6 +507,58 @@ fn main() { # Experimental extensions open to discussion +## SMT-solvers? + +This RFC doesn't propose such thing, but future possibilities are worth discussing: + +### What a Rusty SMT-solver would look like + +The simplest and least obstructive SMT-solver is the SAT-based one. SAT is a +class of decision problem, where a boolean formula, with some arbitrary number +of free variables, is determined to be satisfiable or not. Obviously, this is +decidable (bruteforcing is the simplest algorithm, since the search space is +finite, bruteforcing is guaranteed to terminate). + +SAT is NP-complete, and even simple statements such as `x + y = y + x` can take +a long time to prove. A non-SAT (symbolic) SMT-solver is strictly more +expressive, due to not being limited to finite integers, however first-order +logic is not generally decidable, and thus such solvers are often returning +"Satisfiable", "Not satisfiable", "Not known". + +In general, such algorithms are either slow or relatively limited. An example +of such a limitation is in the [Dafny +language](https://github.com/Microsoft/dafny), where programs exist that +compile when having the bound `a \/ b`, but fails when having the bound `b \/ +a`. This can be relatively confusing the user. + +It is worth noting that the technology on this area is still improving, and +these problems will likely be marginalized in a few years. + +Another issue which is present in Rust, is that you don't have any logical +(invariant) information about the return values. Thus, a SMT-solver would work +relatively poorly (if at all) non-locally (e.g. user defined functions). This +is often solved by having an exression of "unknown function", which can have +any arbitrary body. + +That issue is not something that prevents us from adopting a SMT-solver, but it +limits the experience with having one. + +### Backwards compatibility + +While I am against adding SMT-solvers to `rustc`, it is worth noting that this +change is, in fact, compatible with future extensions for more advanced theorem +provers. + +The only catch with adding a SMT-solver is that errors on unsatisfiability or +contradictions would be a breaking change. By throwing a warning instead, you +essentially get the same functionality. + +### Implementation complications + +It will likely not be hard to implement itself, by using an external SMT-solver +(e.g., Z3). The real proble lies in the probles with performance and +"obviousness" of the language. + ## Candidates for additional rules Currently, the set of rules is rather conservative for rewriting. To make it From 9f06922692ba49ff19aaae4a41a46e1ce8fcb1d0 Mon Sep 17 00:00:00 2001 From: ticki Date: Fri, 24 Jun 2016 16:37:47 +0200 Subject: [PATCH 29/34] Add Hoare-based value/type optional extension --- text/0000-pi-types.md | 170 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 168 insertions(+), 2 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 214e32a1d1d..ce1ee04d68b 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -355,8 +355,8 @@ One can show this by considering each case: 1. `ExpandBooleanAnd` eliminates `{P ∧ Q} ⊢ {P, Q}`. The right hand side's depth is `max(dep(P), dep(Q))`, which is smaller than the original, `max(dep(P), dep(Q)) + 1` -2. `SubstituteEquality` eliminates `{a = b, P} ⊢ {P[b/a]}`, which is an - elimination, since `dep(P) + 1 > dep(P[b/a]) = dep(P)`. +2. `SubstituteEquality` eliminates `{a = b, P} ⊢ {P[b ← a]}`, which is an + elimination, since `dep(P) + 1 > dep(P[b ← a]) = dep(P)`. 3. `DoubleNegation` eliminates `{¬¬x} ⊢ {x}`, which is an elimination, since `dep(x) + 2 > dep(x)`. @@ -507,6 +507,11 @@ fn main() { # Experimental extensions open to discussion +## Remark! + +These are _possible_ extensions, and not something that would be a part of the +initial implementation. These a brought up for the sake of discussion. + ## SMT-solvers? This RFC doesn't propose such thing, but future possibilities are worth discussing: @@ -688,6 +693,167 @@ It is unclear how it plays together with `where` bounds. The pro is that it adds ability to implement e.g. constant indexing, `Index>`. +## Towards a "fully" dependent type system + +In the future, we might like to extend it to a fully dependent type system. +While this is, by definition, a dependent type system, one could extend it to +allow runtime defind value parameters. + +Consider the `index` example. If one wants to index with a runtime defined +integer, the compiler have to be able to show that this value does, in fact, +satisfy the `where` clause. + +There are multiple ways to go about this. We will investigate the Hoare logic way. + +### Is this bloat? + +Well, we can't know if it is. It depends on how expressive, const parameters +are in practice, or more so, if there exists edge cases, which they do not cover. + +### "Sizingness" + +Certain value parameters have impact on the size of some type (e.g., consider +`[T; N]`). It would make little to no sense, to allow one to determine the size +of some value, say a constant sized array, at runtime. + +Thus, one must find out if a value parameter is impacting the size of some +type, before one can allow runtime parameterization. + +Currently, only one of such cases exists: constant sized arrays. One could as +well have a struct containing such a primitive, thus we have to require +transitivity. + +If a value parameter has no impact on the size, nor is used in a parameter of a +constructor, which is "sizing", we call this value "non-sizing". + +Only non-sizing value parameters can be runtime defined. + +### Hoare logic invariants and runtime calls + +As it stands currently, one cannot "mix up" runtime values and value parameter +(the value parameters are entirely determined on compile time). + +It turns out reasoning about invariants is not as hard as expected. [Hoare +logic](https://en.wikipedia.org/wiki/Hoare_logic) allows for this. + +One need not SMT solvers for such a feature. In fact, one can reason from the +rules, we have already provided. With the addition of MIR, this might turn out +to be more frictionless than previously thought. + +Hoare logic can be summarized as a way to reason about a program, by giving +each statement a Hoare triple. In particular, in addition to the statement +itself, it carries a post- and precondition. These are simple statements that +can be incrementally inferred by the provided Hoare rules. + +Multiple sets of axioms for Hoare logics exists. The most famous one is the set +Tony Hoare originally formulated. + +For a successful implementation, one would likely only need a tiny subset of +these axioms: + +#### Assignment axiom schema + +This is, by no doubt, the most important rule in Hoare logic. It allows us to +carry an assumption from one side of an assignment to another. + +It states: + + ──────────────────── + {P[x ← E]} x = E {P} + +That is, one can take a condition right after the assignment, and move it prior +to the assignment, by replacing the variable with the assigned value. + +An example is: + +```rust +// Note: This should be read from bottom to top! + +// Now, we replace a with a + 3 in our postcondition, and get a + 3 = 42 in our precondition. +a = a + 2; +// Assume we know that a = 42 here. +``` + +This rule propagate "backwards". Floyd formulated a more complicated, but forwards rule. + +#### `while` rule + +The `while` rule allows us to reason about loop invariants. + +Formally, it reads + + {P ∧ B} S {P} + ─────────────────────────── + {P} (while B do S) {¬B ∧ P} + +`P`, in this case, is the loop invariant, a condition that much be preserved +for each iteration of the body. + +`B` is the loop condition. The loop ends when `P` is false, thus, as a +postcondition to the loop, `¬B`. + +#### Conditional rule + +The conditional rule allows one to reason about path-specific invariants in +e.g. `if` statements. + +Formally, it reads + + {B ∧ P} S {Q} + {¬B ∧ P } T {Q} + ──────────────────────────── + {P} (if B then S else T) {Q} + +This allows us to do two things: + +1. Lift conditionals down to the branch, as precondition. + +2. Lift conditions up as postconditions to the branching statement. + +--- + +In addition, we propose these Rust specific axioms: + +#### Non-termination rule + +This can be used for reasoning about assertions and panics, along with aborts +and other functions returning `!`. + +Formally, the rule is: + + f: P → ! + p: P + ─────────────────────────── + (if P then f p else E) {¬P} + +This simply means that: + +```rust +if a { + // Do something `!` here, e.g. loop infinitely: + loop {} +} else { + // stuff +} +// We know, since we reached this, that !a. +``` + +#### How this allows runtime calls + +Runtime calls are parameterized over runtime values. These allows the compiler +to semantically reason about the value of some variable. Thus, the bound can be +enforced on compile time, by making sure the statements of the value iplies +whatever bound that must be satisfied. + +#### Advantages and tradeoffs + +It should be obvious that this extension is a big change, both internally and +externally. It makes Rust much more complicated, and drives it in a direction, +which might not be wanted. + +It aligns with Rust's goals: effective statical checking. As such, runtime +assertions are to a less extend needed. + # How we teach this This RFC aims to keep a "symmetric" syntax to the current construct, giving an From 6b88ae55fea0a170c437b94743a08aabe80dc06f Mon Sep 17 00:00:00 2001 From: ticki Date: Fri, 24 Jun 2016 19:11:43 +0200 Subject: [PATCH 30/34] Fix typos --- text/0000-pi-types.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index ce1ee04d68b..a626cd5575f 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -770,7 +770,7 @@ An example is: // Note: This should be read from bottom to top! // Now, we replace a with a + 3 in our postcondition, and get a + 3 = 42 in our precondition. -a = a + 2; +a = a + 3; // Assume we know that a = 42 here. ``` @@ -851,7 +851,7 @@ It should be obvious that this extension is a big change, both internally and externally. It makes Rust much more complicated, and drives it in a direction, which might not be wanted. -It aligns with Rust's goals: effective statical checking. As such, runtime +It aligns with Rust's goals: effective static checking. As such, runtime assertions are to a less extend needed. # How we teach this From 998c29279fc6e8b478ecaf1b4832a897b4bf009f Mon Sep 17 00:00:00 2001 From: ticki Date: Fri, 24 Jun 2016 23:33:28 +0200 Subject: [PATCH 31/34] Transcription rules for inequalities --- text/0000-pi-types.md | 103 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 99 insertions(+), 4 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index a626cd5575f..7e22643dcc8 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -190,6 +190,11 @@ trait Divides {} impl Divides for Num where b % a == 0 {} ``` +### Playground + +[This repo](https://github.com/ticki/rfc-1657-playground) is a playground for +usecases of such a feature. Refer to that for more examples. + # Detailed design [design]: #detailed-design @@ -314,7 +319,7 @@ unify(bound(f))` (by structural equality): ExpandBooleanAnd: P ∧ Q - ────── + ───── P Q @@ -566,6 +571,8 @@ It will likely not be hard to implement itself, by using an external SMT-solver ## Candidates for additional rules +### Propositional logic + Currently, the set of rules is rather conservative for rewriting. To make it easier to work with, one can add multiple new reductive rules, at the expense of implementation complexity: @@ -586,7 +593,7 @@ respect to `∨`. DisjunctiveSyllogism: ¬(P ∧ Q) P - ───── + ──────── ¬Q Basically, this states that if two propositions are mutually exclusive (that @@ -597,6 +604,8 @@ This is strictly reductive. Now let's go funky: +### Cancelation + AdditiveCancelationRR: a + c = b + c ───────────── @@ -632,6 +641,87 @@ Now let's go funky: These are all reductive. +### Inequalities + +Inequalities are something, we are interested in simplifying. These carry many +interesting properties, which shall be covered: + + RewriteGeq: + a ≥ b + ───── + b ≤ a + +Here, we rewrite greater than or equal to a form of less than or equal. + + RewriteLessThan: + a < b + ──────── + a ≤ b + ¬(a = b) + RewriteGreaterThan: + a > b + ──────── + a ≥ b + ¬(a = b) + +This allows us to rewrite less than (`<`) and greater than (`>`), in terms of +their equality accepting versions. + + LeqAdditiveCancelationRR: + a + c ≤ b + c + ───────────── + a ≤ b + LeqAdditiveCancelationLL: + c + a ≤ c + b + ───────────── + a ≤ b + LeqAdditiveCancelationRL: + a + c ≤ c + b + ───────────── + a ≤ b + LeqAdditiveCancelationLR: + c + a ≤ b + c + ───────────── + a ≤ b + LeqMultiplicativeCancelationRR: + ac ≤ bc + ───────────── + a ≤ b + LeqMultiplicativeCancelationLL: + ca ≤ cb + ───────────── + a ≤ b + LeqMultiplicativeCancelationRL: + ac ≤ cb + ───────────── + a ≤ b + LeqMultiplicativeCancelationLR: + ca ≤ bc + ───────────── + a ≤ b + +These are known as the cancelation laws, and are essentially the inequality +version, of those stated for equal. + + LeqNegation: + ¬(a ≤ b) + ──────── + a > b + +This allows us to define the _negation_ of less than or equals to. + +--- + +Unfortunately, transitivity is not reductive. + +### Other relational definitions + +Non-eqaulity is defined by: + + a ≠ b + ──────── + ¬(a = b) + ## Expression reduction rules We might want to have expression reduction rules beyond the basic const @@ -651,6 +741,11 @@ This is simply the distributive property of multiplication. This rules allows us to observe that `a(bc)` is no different from `(ab)c` +Lastly, we are nterested in rewriting subtraction in terms of addition: + + SubtractionToAddition: + a - b ↦ a + (-b) + All these rules are reductive. ## "Exit-point" identities @@ -659,9 +754,9 @@ These are simply identities which always holds. Whenever the compiler reaches on of these when unfolding the `where` clause, it returns "True": LeqReflexive: - f(x) <= f(x) for x primitive integer + f(x) ≤ f(x) for x primitive integer GeqReflexive: - f(x) >= f(x) for x primitive integer + f(x) ≥ f(x) for x primitive integer EqReflexive: f(x) = f(x) NegFalseIsTrue: From 09aef5972acaf75f199885b25b1e74b3051b2d29 Mon Sep 17 00:00:00 2001 From: ticki Date: Fri, 24 Jun 2016 23:37:04 +0200 Subject: [PATCH 32/34] Clarify notation --- text/0000-pi-types.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index 7e22643dcc8..de5610c9fa4 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -370,11 +370,11 @@ In fact, this set of rule is strictly reductive (like equality-based unification #### An example We will quickly give an example of a possible proof. Say we want to show that -`x = b ∧ x < a ⇒ b < a`. Starting with the left hand side, we can sequentially +`(x = b) ∧ ¬¬(x < a) ⇒ b < a`. Starting with the left hand side, we can sequentially prove this, by simple unification (which already exists in the Rust type checker): - x = b ∧ ¬¬(x < a) + (x = b) ∧ ¬¬(x < a) ∴ x = b (ExpandBooleanAnd) ¬¬(x < a) ∴ ¬¬(b < a) (SubstituteEquality) From 0f3a499761229ceab1c3dc62d7277829235428ef Mon Sep 17 00:00:00 2001 From: ticki Date: Sat, 25 Jun 2016 16:23:57 +0200 Subject: [PATCH 33/34] Typos --- text/0000-pi-types.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index de5610c9fa4..a2e85dfd9e2 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -716,7 +716,7 @@ Unfortunately, transitivity is not reductive. ### Other relational definitions -Non-eqaulity is defined by: +Non-equality is defined by: a ≠ b ──────── @@ -741,7 +741,7 @@ This is simply the distributive property of multiplication. This rules allows us to observe that `a(bc)` is no different from `(ab)c` -Lastly, we are nterested in rewriting subtraction in terms of addition: +Lastly, we are interested in rewriting subtraction in terms of addition: SubtractionToAddition: a - b ↦ a + (-b) @@ -937,7 +937,7 @@ if a { Runtime calls are parameterized over runtime values. These allows the compiler to semantically reason about the value of some variable. Thus, the bound can be -enforced on compile time, by making sure the statements of the value iplies +enforced on compile time, by making sure the statements of the value implies whatever bound that must be satisfied. #### Advantages and tradeoffs From 2dbfe2d8f6b9a55ecab4668a3fbf1ca9f769d469 Mon Sep 17 00:00:00 2001 From: ticki Date: Mon, 27 Jun 2016 10:03:17 +0200 Subject: [PATCH 34/34] Fix typos --- text/0000-pi-types.md | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/text/0000-pi-types.md b/text/0000-pi-types.md index a2e85dfd9e2..745082cfb10 100644 --- a/text/0000-pi-types.md +++ b/text/0000-pi-types.md @@ -279,7 +279,7 @@ let l = foo::<_, [1, 2, 3, 4, 5, 6]>(); 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 const exprs, returning a boolean. +archive this, in a reasonable manner, we use constexprs, returning a boolean. We allow such constexprs in `where` clauses of functions. Whenever the function is invoked given constant parameters ``, the compiler @@ -547,7 +547,7 @@ these problems will likely be marginalized in a few years. Another issue which is present in Rust, is that you don't have any logical (invariant) information about the return values. Thus, a SMT-solver would work relatively poorly (if at all) non-locally (e.g. user defined functions). This -is often solved by having an exression of "unknown function", which can have +is often solved by having an expression of "unknown function", which can have any arbitrary body. That issue is not something that prevents us from adopting a SMT-solver, but it @@ -566,7 +566,7 @@ essentially get the same functionality. ### Implementation complications It will likely not be hard to implement itself, by using an external SMT-solver -(e.g., Z3). The real proble lies in the probles with performance and +(e.g., Z3). The real problem lies in the issues with performance and "obviousness" of the language. ## Candidates for additional rules @@ -718,9 +718,10 @@ Unfortunately, transitivity is not reductive. Non-equality is defined by: - a ≠ b - ──────── - ¬(a = b) + NeqDefinition: + a ≠ b + ──────── + ¬(a = b) ## Expression reduction rules @@ -768,7 +769,7 @@ of these when unfolding the `where` clause, it returns "True": OrTrue2: true ∨ P -### A constexpr type constructor +## A constexpr type constructor Add some language item type constructor, `Const`, allowing for constructing a constexpr-only types. @@ -831,7 +832,7 @@ As it stands currently, one cannot "mix up" runtime values and value parameter It turns out reasoning about invariants is not as hard as expected. [Hoare logic](https://en.wikipedia.org/wiki/Hoare_logic) allows for this. -One need not SMT solvers for such a feature. In fact, one can reason from the +One need not SMT-solvers for such a feature. In fact, one can reason from the rules, we have already provided. With the addition of MIR, this might turn out to be more frictionless than previously thought.