Parameterize types over numerics / type level integers

[brson]

This is a postponement issue tracking postponed RFCs in the general area of "functions generic over a constant" or "generic constants" and so forth.

Example use cases for items parameterized by a constant:

• implement a trait for [T; N] for any N
• small vector types (SmallVec<32>)

Example use cases for generic constants:

• initializers like const FOO<T> = SomeType { value: None::<T> }; (const fn can also address this)

Here is a list of relevant RFCs:

• Constants that depend on type parameters in generic code #1062
• RFC: Generic const and static #1520 -- generic const and static
• Allow types to be parameterized by integer (and bool) constant values. #884

[Binero]

Is there any update on this?

[quantheory]

Checking types which depend on constants which depend on types is a thorny issue, and I think that that's where we are at right now. See #1062. If we could work out how to use associated constants in generic code better, that would get us a lot closer to type-level numbers (or constants in general).

[burdges]

It's maybe worth signaling @edwinb and @david-christiansen here, although Idris itself takes a far more drastic solution.

[quantheory]

I would be interested if they have any comments. Rust has a couple of considerations that are different from some other languages that already have dependent types (including Idris):

1. We don't have any guarantee that type checking will terminate (actually, we have Turing completeness at the type level). So we don't have any constraint that we have to keep type checking decidable, because it's not in the first place. It's more a matter of being "as complete as possible" in some practical sense, without sacrificing soundness.

2. Array sizes are based around the primitive integer type usize rather than on inductively defined type-level naturals. We normalize by fully evaluating the expressions that specify sizes, i.e. the compiler actually knows (or can lazily evaluate) the exact size of every array as a 32/64-bit integer during type checking.

   This falls apart the moment we allow a constant expression to contain a value that we don't actually know during type checking, e.g. a generic constant parameterized by some unknown type. So the challenge is to come up with a new method of normalizing constant expressions during type-checking, something backwards-compatible and not confusingly inconsistent with current features.

[yongqli]

I would love to see this as well. My particular use case would be implementing something like:

fn kalman_filter<S, N>(prev_state: [[f64; S]; S], obs: ([f64; N], [[f64; S]; N])) -> [[f64; S]; S]

• I only need to assert equality between generic type
• I would like to be able to override the default implementation; for example, it might be possible to do a better job optimizing matrix inversion for a 3x3 matrix.

[david-christiansen]

I'm saying this as someone who is merely an enthusiastic observer of Rust, having never actually used it. So please take it with a major grain of salt.

I wouldn't think that Idris-style dependent types would work particularly well in a language that isn't designed for them from the get-go - especially not in a language with side effects! I would imagine that, instead of automatically promoting user-written functions to the type level, it would be better to have a sub-language of allowed operations on the numeric types. Then, you can use techniques like Presburger arithmetic solvers or SMT solvers that know how to solve equality constraints over these expressions that arise during type checking.

@yav somewhat-recently extended GHC to support type checker plugins that can do whatever they want with equality constraints. He's used this to implement type-level naturals at https://github.com/yav/type-nat-solver - this is probably a better place to look than Idris.

[milibopp]

@david-christiansen
What do you think about only promoting an explicit subset of the language to the type level? I wonder, whether the recently introduced const fn may qualify for this purpose… At least, as far as I know, this part is free of side-effects so far. Of course, this makes reasoning about equality significantly harder.

There is still the idea to allow parametrization over values of more general types. So we may want to avoid doing too much special-casing that works for type-level numerics only. Maybe this is too ambitious altogether. But even if we do it for numerics using some specialized solver first, I'd prefer to keep it extensible, so that the option to move to something more general is available.

[edwinb]

I don't know how well this would work for Rust (my instinct is that
you'd need to redesign quite a bit), but I have sometimes wondered if we
could have an imperative language with full dependent types by having
only the pure subset available at the type level, more or less as you
suggest.

This isn't even that different from what we do in Idris, in the sense
that, at the type level, Idris treats non-total functions as constants,
so you don't quite have the full language available. I don't see why
something similar couldn't be done in principle for an imperative
language, but I expect there will be interesting challenges in practice.

It's also a bit like what happens in programs using the Idris effects
library - there is a separation between the pure programs which effects
can be parameterised by, and the effectful programs themselves.

There's probably a PhD or two in this if anyone fancies having a go :)

On 29/06/2015 10:01, Eduard Bopp wrote:

@david-christiansen https://github.com/david-christiansen
What do you think about only promoting an explicit subset of the
language to the type level? I wonder, whether the recently introduced
|const fn| may qualify for this purpose… At least, as far as I know,
this part is free of side-effects so far. Of course, this makes
reasoning about equality significantly harder.

There is still the idea to allow parametrization over values of more
general types. So we may want to avoid doing too much special-casing
that works for type-level numerics only. Maybe this is too ambitious
altogether. But even if we do it for numerics using some specialized
solver first, I'd prefer to keep it extensible, so that the option to
move to something more general is available.

—
Reply to this email directly or view it on GitHub
#1038 (comment).

[glaebhoerl]

cc @jroesch @freebroccolo @kmcallister

[quantheory]

I have been busy most of the last week, really the last few weeks, so I'll give a few belated responses now. (I'll spare you the full details, but the punchline is a car accident last week, in which I was luckily not injured.) I regret that I can't really connect my thoughts to Idris, since I haven't learned it all that well yet; however I hope that my experience with Haskell bridges the gap a bit.

@yongqli I believe that #1062 would be a good start toward using constants this way. If it was accepted and implemented, you could use associated constants as a "workaround" until the dependent type situation improved. However, treating 3x3 matrices specially would require other changes to Rust. I am interested in some similar problems, like specialization for SIMD. (Operations on 2D/4D/8D vectors might be sped up relative to other sizes.) It's not clear how Rust will handle that kind of specialization.

@david-christiansen I appreciate your input (and I hope I'm not too verbose in replying). I think that @aepsil0n has given a similar response to what I would have said. Even though Rust 1.0 has (mostly) stabilized the language, the relatively new and unstable const function feature provides the possibility of having a pure subset of the language that can be promoted to the type level. (In fact, I've somewhat felt that this is the point of most const language features in Rust.) Because of this, I think that being able to check for equality of types is the real problem, whereas purity of operations is a relatively manageable issue (at least in theory).

I've gradually come around to @freebroccolo's point of view (as I understand it, which may not be very well). For backwards compatibility, the compiler presumably has to evaluate constant expressions as completely as possible (under our current understanding of "evaluation", i.e. where you can literally get some primitive value at the end). But past that, we need some kind of solver to deal with generic code, and we aren't very constrained by compatibility. It is possible, but not ideal, to build an SMT solver directly into the compiler without a detailed explanation. (The problem being that any "obvious" generalization of Rust's current arithmetic capability is probably undecidable, and in any case, the effect on compile times would be unpredictable in practice. For a systems language, of course, for most code a sufficiently dedicated/intelligent/experienced human should be able to tell whether it will compile, and roughly how it will scale, without knowing the gory details of the internals of a specific compiler. One awkward aspect in developing a new systems language is that we want the reference compiler to be excellent, while simultaneously wanting the language to be specified clearly enough that other compilers can arise and work well.)

It's almost certainly better to do something like what @yav has done with GHC and allow plugins to deal with arithmetic during type-checking (though this may be a ways off for Rust, since we have only vaguely planned a stable API for syntax-phase plugins, and don't support type-checking-phase plugins yet at all). But if a particular representation and set of operations for type-nats can be defined at the plugin/library level, we can define types/traits in the standard library that provide a standard representation. At least in theory, this provides the opportunity for a decent standard solution for users like @yongqli and I, who have specific use cases that only need simple checks, while more advanced users can pick different plugins/solvers if for some reason the standard implementation fails on certain cases.

@edwinb I'm thinking that that was mostly just an offhand comment, but I'm about to go back to school for an applied maths PhD, so maybe we should talk. Having been both a physicist-in-training (think Fortran 95) and the amateur developer of Rust's associated constant capability, I've certainly thought about imperative languages plus dependent types. =)

Actually, something like Haskell's DataKinds might not be a bad approach. The difficulty seems to be that we already allow primitives (particularly usize) at the type level.

[milibopp]

@quantheory interesting, our background and interests seems to be very similar. i have actually been thinking a lot about applying more advanced type system features such as this or full dependent types to numerical simulation techniques. I'm mostly approaching this from a numerical fluid dynamics point of view. Rust's type system is not quite powerful enough to do too fancy things, but using Idris for this application domain appears to be out of the question for performance reasons (although that last statement probably requires some benchmarking).

There are things like compile-time physical units (fairly straight-forward, once this feature is implemented) or efficient numerical solvers for certain kinds of equations that make use of information available compile-time for code generation. I'd love to talk about these things in more detail and share ideas at some point (perhaps independent of Rust). But, for now, just file this under motivation and use cases ;)

[droundy]

I think it might be worth pointing out here that @paholg has already implemented signed Peano numbers at the type level in rust:

http://paholg.com/doc/dimensioned/peano/index.html

Personally, I'd love to have type-level numbers not so much for new features (since we can already implement them ourselves) but for good error messages and in order to be able to write generic code that works with arrays. I feel like comparison, equality and addition and subtraction would by themselves be sufficient for a whole lot of benefit, without danger of adding (much) to the complexity of a human understanding rust code, or the dangers of undecideable code.

[Yamakaky]

Wow, this crate is awesome!

[eddyb]

For floating-point numbers in types, @mrmonday started a discussion about it in the Idris community, which ended up as the issue idris-lang/Idris-dev#2609 where type unification in the presence of floating-point numbers allows you to prove False = True i.e. Void.

Not having reflexive type equality might hurt rustc's type-handling performance, which is why I was against it, but it turns out that affects the type system itself, not just the implementation.

[mrmonday]

There's also some discussion of this over in the D forums, if anyone's interested: http://forum.dlang.org/thread/rvgslgwzvqwchpowhntg@forum.dlang.org.

[ghost]

@eddyb honestly the thing with floats in the Idris issue shouldn't be surprising because they are just poorly behaved with respect to equality and algebraic properties.

Personally, I think the only reasonable approach here is to use a proper (co)algebraic or topological encoding of real numbers and force the types/specifications to be approximate. Something like Abstract Stone Duality (see Baeur's Marshall and Taylor's slides) would probably be the way to go.

This would probably make them less convenient to use but it would be better than doing something unsound with the type system.

[steveklabnik]

Adding "type level integers" to the title because I can never find this RFC with search

[alexchandel]

If and when Rust adds syntax for dependent typing, including "type-level numbers", it should be very generic. The syntax should be compatible with the promotion of suitable datatypes and traits like Haskell's, although of course Idris's type-level values are much cleaner. Permitting only the pure, total subset of the language is suitable for this.

[dbrgn]

Is there anything that is being done in this area?

I'm not well versed in the area of type systems, so I can't really judge the feasibility of this feature. But right now I see the following not-so-nice things in Rust:

• The docs of APIs dealing with arrays are often cluttered with impls for [T; 0] through [T; 32]. See array itself, for example.
• Based on what I know of rust, it's currently not possible to create a function that does "multiplication of two vectors that must have the same length" at the type level.
• Traits like Clone are only implemented for arrays up to length 32. It's very surprising if adding a number to an array can cause the array to become un-cloneable by default. Also, I think the number 32 is quite arbitrary, right?

Please point out the mistakes in my statements, if there are any :)

[ERnsTL]

Just hit this issue the other day as well when I wanted to simply clone an [u8; 4096]. Apparently Clone isn't implemented for an array of bytes. What could possibly be more cloneable? Please make this possible.

[Binero]

@ERnsTL It is implemented for arrays up to size 32 if I'm not mistaken.

[ticki]

@ERnsTL as a hack, you can use ptr::read. Just remember to make sure that the inner type is actually copy.

[eddyb]

@ticki I thought all [T; N] were Copy iff T: Copy, hardcoded in the compiler, only the Clone implementation doesn't exist.

[ticki]

Copy requires a Clone bound.

[eddyb]

@ticki Yes, but the compiler returns "implemented" without checking anything other than the contained type.

[ticki]

Oh, cool. I thought that'd result in type unsafety.

[retep998]

@ticki It does result in type unsafety, well, it results in ICEs anyway, especially around trait objects.

I personally get around the issue by wrapping the array in another type, and implementing Copy and Clone for that type where instead of deriving Clone I'd take advantage of the fact that the type is Copy and do impl Clone for Foo { fn clone(&self) { *self }}.

[ticki]

Here you go: #1657

It is a general solution to type-level values (Π-constructors).

[iqualfragile]

@pcwalton
some, limited arithmetic is quite useful, for example if you want to implement one (binary|quad|oct)tree.
you would need to have an 2**N sized child-array for N being the dimension.

[genbattle]

I'm consistently disappointed every three months when I come back to this RFC and it's still languishing in the backlog.

This papercut makes it very painful to use fixed-length arrays with generics in Rust.

[ketsuban]

@genbattle The reason this RFC specifically is "languishing" is because the discussion has moved on as a result of @ticki's work none of which I understand a word of, and which to the best of my understanding appears to now be focused on this meta-RFC.

(Should this RFC be closed as it addresses a subset of that one?)

[golddranks]

Here's a link to a more recent update on how the Language team thinks about the matter. https://internals.rust-lang.org/t/lang-team-minutes-const-generics/5090 I think of the RFCs @ketsuban linked, the first one is the relevant one, but it's pending on an update based on the discussion and the mentoring.

[genbattle]

I'm glad some updates have been provided, it's very reassuring to know that this issue is being worked on in the background (and that the name has changed slightly). I'll keep an eye out for further news on const generics, hopefully they land by the end of the year as planned!

[withoutboats]

See RFC #2000

[steveklabnik]

RFC 2000 was accepted 🎊

[Centril]

Closing in favor of #2424 and rust-lang/rust#44580.