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.