[lmm]

As a Scala user: the further I've got into a functional/MLey style the more linear my code has become. Options or collections are very naturally handled with "fold" (cata). Loops probably shouldn't be infinite - if you're looping it's usually because you're folding along a data structure, and those ought to be finite (one of the ideas I'm toying with is a type-level natural indexed recursion-schemes like library, to make it easy to construct recursive structures that are known-finite).

I don't know if it's where Rust wants to be, but I want a practical-oriented ML-family language that does this.

[burntsushi]

Friendly challenge (because I agree with you, but constantly run into limitations):

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?

[lmm]

In practice, probably not.

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.

[mrkgnao]

GHC already does a lot of loop fusion and optimizing away of linked lists (which is good given the unfortunate overdue of cons-lists over nicer things among Haskell users) which can be extended to work with user code using rewrite rules. Libraries like text, bytestring, and vector do exactly the elision of intermediate structures that you talk about, allowing you to convert from a vector to a list, apply some function that annoyingly only works with lists, and convert back into a vector, and have that compile into a single tight for-loop in many cases.

I wonder what the upcoming linear types work will do.

[burntsushi]

> 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 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.

[lmm]

Ultimately what we want is a representation that makes it easy to understand the performance characteristics of a given piece of code (and I'd agree that this is an area where the purist functional tradition has lagged behind). In the past assembly was this, but I don't know that it can be these days; I've read that on modern hardware, the biggest factor affecting performance is cache efficiency. So even seeing the sequence of machine instructions might not be enough to allow a developer to reason about performance, because two similar-looking sequences of CPU instructions can easily end up having very different performance characteristics (branch prediction can have a similar effect AIUI).

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.

[mafribe]

As a typing system developer I suspect there is a hard trade-off / sweetspot between complexity of the types/fold constructs and guarantees that can be enforced by types.

   How does that fit

Probably doesn't and typing systems for general purpose languages will probably have to fall back on general recursion to handle it. And there's nothing wrong with this. Language simplicity is also a virtue. If your recursion is complicated and correctness so important that testing is insufficient, then I recommend post-programming verification with a program logic.

[burntsushi]

> And there's nothing wrong with this.

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.

[_lm_]

You might find Idris's totality checking very interesting, if you haven't already seen it!

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html...