4 ms·

I assume you mean strict (the opposite of lazy) instead of non-pure (which means imperative). Well, even then, Rust does not only give you control over executi

by vog 10y ago

I assume you mean strict (the opposite of lazy) instead of non-pure (which means imperative). Well, even then, Rust does not only give you control over execution order, but also tight control over memory management, while keeping it safe. Haskell allows for good reasoning about correctness. In OCaml, you can additionally reason about execution order, but memory management and garbage collector are still somewhat "unpredictable" (i.e. hard to reason about). On top of that, in Rust, you can reason clearly about memory usage and aliasing. These new, modern languages follow a clear path about keeping quality and correctness (hence safety) while having more and more control over performance, without going back to low-level where you would loose clarity about correctness and safety. (Note, however, that the distinction between correctness and performance is over-simplified here, because performance can also be part of correctness, e.g. for real-time systems, or in systems where scalability is an important requirement.)

pron 10y ago
> pure (the opposite of imperative). Pure is not quite the opposite of imperative; declarative is the opposite of imperative, although in practice it is true that pure functional languages tend to be more declarative that imperative functional ones. You can have pure (AKA referentially transparent) imperative languages if they are synchronous[1]. The synchronous style is especially well suited to reactive/interactive applications, and quite popular in hard realtime applications. Also, we don't really have exact definitions to any of these terms (imperative, pure, functional, declarative). Here is my attempt for approximate, problematic definitions: * Functional -- a language that models most/all computations as (possibly partial) mathematical functions, and constructs a program by assembling those functions. * Imperative -- a language that models computation as state transitions, specifying what state should the computation have at each step. * Declarative -- a language that describes what result should the program give (as a function, a relation or a behavior) rather than at each step. * Pure -- a language where the semantic value of the composition of syntactic terms can be determined by the semantic value of each of the component terms and no others. [1]: https://en.wikipedia.org/wiki/Synchronous_programming_language https://en.wikipedia.org/wiki/Synchronous_programming_langua...
- catnaroek 10y ago
  You've just defined “pure” as “can be given a denotational semantics”. I have news for you: even ALGOL can be given a denotational semantics. --- @pron Nowadays I prefer the terms “effect-free” and “effectful”, rather than “pure” and “impure”, since I don't want to suggest that effects are somehow “wrong” or “evil”. By definition, values are effect-free. An effect is anything that invalidates some equational law that holds for values. For example, integer equality is decidable, and `x == x` evaluates to `true` when `x` is any integer value. However, if we substitute `x` with the expression `foo()`, where: int counter = 0; // or any other initial value int foo() { return counter++; } Then `foo() == foo()` doesn't evaluate to `true` anymore. Hence `foo` is an effectful procedure. Of course, nontermination is an effect too. If we had defined `foo` as: int foo() { while(true); return 0; } Then `foo() == foo()` would similarly fail to evaluate to `true`.
  - pron 10y ago
    Yeah, I know my definitions are problematic. Remember that the term "referential transparency" was introduced to computer science by Strachey in his Fundamental Concepts in Programming Languages as a property of procedural, imperative languages. How would you define pure? --- > An effect is anything that invalidates some equational law that holds for values. Ah, I can certainly accept that as a definition, except that I'm not sure how different it is from mine, because the equational law you refer to applies to syntactic terms (`foo` in your example) and the language's equality operator (`==` in your example). It's easy to come with an equivalence relation that would hold for `foo`, but not at the syntax level (e.g., equality that takes `foo` to mean `foo`'s definition and the content of the heap, and the value of `foo` would not be its return value but its behavior -- i.e., the behavior of foo for equal heap contents is always the same).
    - catnaroek 10y ago
      > except that I'm not sure how different it is from mine, because the equational law you refer to applies to syntactic terms An effectful language can be given a denotational semantics. At least from what I've seen, when most people say “pure”, they mean “effect-free”. > It's easy to come with an equivalence relation that would hold for `foo`, but not at the syntax level [emphasis mine] Yep, indeed, that's the whole point.
catnaroek 10y ago
Reasoning about correctness in Standard ML is easier than in either Haskell or OCaml, since induction on strictly positive datatypes actually works as a reasoning principle. You don't need to manually assert silly preconditions such as “this list is finite” (Haskell) or “this list isn't cyclic” (OCaml). On the other hand, neither Haskell nor the MLs tackle the problem of safely managing ephemeral resources. Rust does this, but it sacrifices the ability to conveniently share immutable data structures (Rc and Arc exist, but they aren't very convenient). The good news is that this doesn't have to be a dichotomy. You can have GC for in-memory data structures and deterministic destruction for everything else: https://news.ycombinator.com/item?id=12766781 https://news.ycombinator.com/item?id=12766781
- vog 10y ago
  > The good news is that this doesn't have to be a dichotomy. You can have GC for in-memory data structures and deterministic destruction for everything else That's very interesting. Please correct me if I'm wrong, but I think this is not the final solution, either, because you still have the GC running, which prevents strict proofs about performance e.g. for real-time systems. Here, the Rust approach has benefits as it enables you to get very far without a GC.
  - catnaroek 10y ago
    Sure.

by vog 10y ago

pron 10y ago

> pure (the opposite of imperative). Pure is not quite the opposite of imperative; declarative is the opposite of imperative, although in practice it is true that pure functional languages tend to be more declarative that imperative functional ones. You can have pure (AKA referentially transparent) imperative languages if they are synchronous[1]. The synchronous style is especially well suited to reactive/interactive applications, and quite popular in hard realtime applications. Also, we don't really have exact definitions to any of these terms (imperative, pure, functional, declarative). Here is my attempt for approximate, problematic definitions: * Functional -- a language that models most/all computations as (possibly partial) mathematical functions, and constructs a program by assembling those functions. * Imperative -- a language that models computation as state transitions, specifying what state should the computation have at each step. * Declarative -- a language that describes what result should the program give (as a function, a relation or a behavior) rather than at each step. * Pure -- a language where the semantic value of the composition of syntactic terms can be determined by the semantic value of each of the component terms and no others. [1]: https://en.wikipedia.org/wiki/Synchronous_programming_language https://en.wikipedia.org/wiki/Synchronous_programming_langua...

catnaroek 10y ago
You've just defined “pure” as “can be given a denotational semantics”. I have news for you: even ALGOL can be given a denotational semantics. --- @pron Nowadays I prefer the terms “effect-free” and “effectful”, rather than “pure” and “impure”, since I don't want to suggest that effects are somehow “wrong” or “evil”. By definition, values are effect-free. An effect is anything that invalidates some equational law that holds for values. For example, integer equality is decidable, and `x == x` evaluates to `true` when `x` is any integer value. However, if we substitute `x` with the expression `foo()`, where: int counter = 0; // or any other initial value int foo() { return counter++; } Then `foo() == foo()` doesn't evaluate to `true` anymore. Hence `foo` is an effectful procedure. Of course, nontermination is an effect too. If we had defined `foo` as: int foo() { while(true); return 0; } Then `foo() == foo()` would similarly fail to evaluate to `true`.
- pron 10y ago
  Yeah, I know my definitions are problematic. Remember that the term "referential transparency" was introduced to computer science by Strachey in his Fundamental Concepts in Programming Languages as a property of procedural, imperative languages. How would you define pure? --- > An effect is anything that invalidates some equational law that holds for values. Ah, I can certainly accept that as a definition, except that I'm not sure how different it is from mine, because the equational law you refer to applies to syntactic terms (`foo` in your example) and the language's equality operator (`==` in your example). It's easy to come with an equivalence relation that would hold for `foo`, but not at the syntax level (e.g., equality that takes `foo` to mean `foo`'s definition and the content of the heap, and the value of `foo` would not be its return value but its behavior -- i.e., the behavior of foo for equal heap contents is always the same).
  - catnaroek 10y ago
    > except that I'm not sure how different it is from mine, because the equational law you refer to applies to syntactic terms An effectful language can be given a denotational semantics. At least from what I've seen, when most people say “pure”, they mean “effect-free”. > It's easy to come with an equivalence relation that would hold for `foo`, but not at the syntax level [emphasis mine] Yep, indeed, that's the whole point.

catnaroek 10y ago

Reasoning about correctness in Standard ML is easier than in either Haskell or OCaml, since induction on strictly positive datatypes actually works as a reasoning principle. You don't need to manually assert silly preconditions such as “this list is finite” (Haskell) or “this list isn't cyclic” (OCaml). On the other hand, neither Haskell nor the MLs tackle the problem of safely managing ephemeral resources. Rust does this, but it sacrifices the ability to conveniently share immutable data structures (Rc and Arc exist, but they aren't very convenient). The good news is that this doesn't have to be a dichotomy. You can have GC for in-memory data structures and deterministic destruction for everything else: https://news.ycombinator.com/item?id=12766781 https://news.ycombinator.com/item?id=12766781

vog 10y ago
> The good news is that this doesn't have to be a dichotomy. You can have GC for in-memory data structures and deterministic destruction for everything else That's very interesting. Please correct me if I'm wrong, but I think this is not the final solution, either, because you still have the GC running, which prevents strict proofs about performance e.g. for real-time systems. Here, the Rust approach has benefits as it enables you to get very far without a GC.
- catnaroek 10y ago
  Sure.