6 ms·
>what you are asking for would require dependent typing. I know nothing about Rust, but you might find Oleg Kiselyov's: "Eliminating Array Bound Checking throu
by GregBuchholz 10y ago
>what you are asking for would require dependent typing.
I know nothing about Rust, but you might find Oleg Kiselyov's: "Eliminating Array Bound Checking through Non-Dependent Types" interesting.
http://okmij.org/ftp/Haskell/eliminating-array-bound-check.lhs http://okmij.org/ftp/Haskell/eliminating-array-bound-check.l...
You may also like:
http://okmij.org/ftp/Haskell/number-parameterized-types.pdf http://okmij.org/ftp/Haskell/number-parameterized-types.pdf
http://okmij.org/ftp/Computation/resource-aware-prog/tfp.pdf http://okmij.org/ftp/Computation/resource-aware-prog/tfp.pdf
- eddyb 10y agoIf that is what I think it is, see https://docs.rs/indexing https://docs.rs/indexing for something similar, crafted from invariance over higher-ranked lifetimes, instead of types. I don't think Rust can ever replicate the Haskell implementation identically (if we had HRTB over types), as type parametrism is gone (see: specialization RFC). However, lifetime parametrism serves a similar role in Rust, and lifetimes are closer to a concept of "instance" than types.