I loop over strings a lot. Can I fit them into a nice recursive structure without runtime overhead?
Bonus round: My loops over strings often aren't straight-forward one-byte-at-a-time iterations. Sometimes my loops look at 8 or even 16 bytes in a single iteration. How does that fit in with more sophisticated types like you're describing?
In theory, there's no reason one couldn't compile a linked list in source to a flat array at runtime if the access pattern was right (and linear types should make that kind of optimization a lot more practical. This might even be something one could implement "in userspace" in a language with linear types - like a safe version of an iterator. Certainly I'd be excited to try - I'm not claiming this is immediately production-quality). Or one could ask where the string is coming from in the first place, and trust some kind of fusion-style optimization to remove the intermediate datastructure entirely at runtime.
Peeling off the front 8 or 16 elements should be no harder than peeling off the front 1, though naively you might have to handle each partial case from 1 to 15.
I wonder what the upcoming linear types work will do.
I think I under-specified my requirement. :-) By "16 bytes at a time," I mean, "run a single CPU instruction on those 16 bytes."
But yeah, I get your drift. I can see how it might be theoretically possible. I suppose the key gains might be in how much confidence a programmer can have that their code compiles down to the right set of instructions.
In the long term I hope for a "nice" language (in particular one in which checked correctness is easy) with explicit performance semantics along the lines of http://www.cs.cmu.edu/~rwh/papers/iolambda/short.pdf . But yeah under the current state of the art there is no ideal approach, so there's a tradeoff in practice even though I don't think there should be one in theory.
How does that fit
Right. I am trying to brighten that line between the sophistication of type systems, the runtime performance of programs and the simplicity of code. I think they are connected in interesting ways, and some of the more rewarding learning I've ever done has consisted of using more sophisticated type system techniques without paying too much on the performance and/or simplicity side of things.