The latest Futhark language update introduces a bit of dependent typing on array lengths:
https://futhark-lang.org/blog/2020-03-15-futhark-0.15.1-released.html
It's a start, probably it will be refined later. This moderate amount of dependent typing is useful for Rust code too.
See const-generics which allows a limited amput of dependent typing for Rust. As an example of usage, staticvec is a crate that utilizes this to build an fixed capacity Vec.
Sadly nightly is still required to use staticvec.
staticvec is quite far from what you need to implement even a limited form of dependent typing with slices, vecs, etc, in Rust to handle lenghts.
All of that can be done today, in a somewhat painful and slow-to-compile form, using generic-array and typenum.
See the heapless crate crate for an example of a rich data structures library built on generic-array.
Hopefully all of its current usage can eventually be replaced with const generics, whenever they're stabilized.
True, I just wanted to bring up some related work in Rust. Since const generics still can't handle general expressions just yet, staticvec can't really do any of the interesting dependent type stuff. But that is being worked on right now, so this limitation may be lifted soon*.
* hopefully soon
Author of StaticVec here: while it's true the underlying language functionality the crate uses is definitely still "a work in progress", I disagree that the crate is "far from even a limited form of dependent typing".
Though I personally have never thought about it in those particular terms as that's just not really how I think about things in general, several of StaticVec's methods do essentially make succesful use of what you're calling "dependent typing" right now, and even make it work with type inference in what I think is a pretty ergonomic way.
Specifically, have a look at concat as well as intersperse.
Both work perhaps even better with inferred types than they do without it, and for intersperse there's actually an (IMO) rather cool example of that kind of usage at the bottom of the small example program I have in my README.md. I'll post the relevant snippet here directly too for the sake of convenience:
// The type parameter is inferred as `StaticVec<usize, 8>`.
let filled = StaticVec::<_, 128>::filled_with_by_index(|i| {
staticvec![
i + 1,
i + 2,
i + 3,
i + 4,
]
.intersperse((i + 4) * 4)
});
println!("{:?}", filled);
}
If you're not familiar with what filled_with_by_index does, the docs for it are here.
Basically though, the compiler is able to figure out that the usage of the staticvec! macro returns a StaticVec<usize, 4>, and that the immediate usage of intersperse off of that StaticVec instance returns a StaticVec<usize, 8>, and finally that the resulting filled StaticVec variable amounts to having a type signature of StaticVec<StaticVec<usize, 8>, 128>.
So it is, I'd say, a pretty cut-and-dry example of exactly the kind of "specific concrete types created on the fly based solely on the input" thing you're talking about.
Also, in response to:
While heapless does currently still implement more overall data structures than staticvec, in my (obviously biased) opinion the ones that are implemented by both crates right now are rather more complete in staticvec. For the sake of easy comparison, the list consists of:
Not that I'm in any way interested in any kind of "rivalry" or trying to diminish heapless or say it's a bad crate or anything like that (as most importantly the way heapless is implemented is the only way a crate of its age could possibly be implemented).
That said, one of my goals with staticvec overall has always been maximum completeness and not leaving anyone saying "man, I sure wish staticvec had XYZ feature", and based on the current state of it I don't think it's unreasonable for me to at least point out the extents I've gone to in order to make that be (in a constantly increasing way) the case.
This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.