3 ms·

> Imperative languages can do that [distinguish pure from impure computations] very, very easily. In an imperative language, can I write a map or filter whose

> Imperative languages can do that [distinguish pure from impure computations] very, very easily. In an imperative language, can I write a map or filter whose argument is guaranteed to be pure? [Note that my notion of "pure" is stronger than Haskell's: I consider nontermination an effect.] Can you easily convince the type system that an imperative loop will indeed terminate? [Without supplying anything even vaguely resembling a proof.] With pattern matching and recursion, the compiler can check whether recursive calls are always passed smaller arguments. > Good luck finding one with the same performance... I'm pretty sure that, with substructural types, it's possible to update a single array element in O(1) in a referentially transparent manner. Conceptually, you're destroying the old array, and creating a new one with the same contents, except for the updated element. But, because the old array won't be used anymore, this can be done in-place. As far as I can tell, no other imperative facilities are needed to sort an array. > as correct as they're required to be What does this even mean?

pron 11y ago
> In an imperative language, can I write a map or filter whose argument is guaranteed to be pure? Of course. See, e.g. Java's checked exceptions. If you marked every effectful function as throwing a checked exception, the compiler can enforce which effects are allowed. > Can you easily convince the type system that an imperative loop will indeed terminate? [Without supplying anything even vaguely resembling a proof.] With pattern matching and recursion, the compiler can check whether recursive calls are always passed smaller arguments. Model checkers can do this just as well. > What does this even mean? That programs aren't required to be 100% correct, just as they aren't required to be as fast as possible. It is perfectly acceptable for most programs to fail on rare edge cases. If there is an inverse relationship between the manifestation of the bug in the frequency of the circumstances that causes it, then you're fine (put simply: it's OK to fail with ever higher probability on ever rarer cases).

pron 11y ago

> In an imperative language, can I write a map or filter whose argument is guaranteed to be pure? Of course. See, e.g. Java's checked exceptions. If you marked every effectful function as throwing a checked exception, the compiler can enforce which effects are allowed. > Can you easily convince the type system that an imperative loop will indeed terminate? [Without supplying anything even vaguely resembling a proof.] With pattern matching and recursion, the compiler can check whether recursive calls are always passed smaller arguments. Model checkers can do this just as well. > What does this even mean? That programs aren't required to be 100% correct, just as they aren't required to be as fast as possible. It is perfectly acceptable for most programs to fail on rare edge cases. If there is an inverse relationship between the manifestation of the bug in the frequency of the circumstances that causes it, then you're fine (put simply: it's OK to fail with ever higher probability on ever rarer cases).