5 ms·

Rust is pretty much based around linear types (well I think technically it's a variant of that, I have heard about "affine types", don't know the difference), m

Rust is pretty much based around linear types (well I think technically it's a variant of that, I have heard about "affine types", don't know the difference), more precisely the move semantics. EDIT: Oh, the expert has spoken while I was writing. See steveklabnic's answer !

steveklabnik 9y ago
> I have heard about "affine types", don't know the difference Linear types: must be used exactly once Affine types: can't be used more than once
lmkg 9y ago
> I have heard about "affine types", don't know the difference A value with a linear type is used exactly once. A value with an affine type is used at most once. In other words, both types prevent double-use of single-use resources, but linear types additionally guarantee no leaks of said resources. True linear types are far less common in practice, because in order to prove that a value is actually consumed, you have to prove that the program doesn't go into an infinite loop first. Which, y'know, good luck with that.
- mcaruso 9y ago
  > True linear types are far less common in practice, because in order to prove that a value is actually consumed, you have to prove that the program doesn't go into an infinite loop first. Which, y'know, good luck with that. I don't know much about the subject, but I just read the GHC proposal and it seems they don't consider this an issue: https://ghc.haskell.org/trac/ghc/wiki/LinearTypes https://ghc.haskell.org/trac/ghc/wiki/LinearTypes (see: "Isn't a linear function that diverges unsound?")
  - lmkg 9y ago
    Key quote from your link (emphasis added): > The properties of linear types which we need are not compromised by non-termination. This is an implicit admission that Haskell "linear types" are not "true" linear types, but instead only have a subset of the defining properties. I don't mean this in a disparaging fashion. Pretty much everyone uses the name "linear types" even though "affine types" is what they actually have. And I'm totally on-board with this. "Linear" is a more common word than "affine," and the defining difference isn't the property of linear types that most people care about (double-frees are a bigger deal than leaks). And, of course, the fact that you can't actually determine true linearity for Turing-Complete languages. For what it's worth, it sounds like Haskell's "linear types" provides slightly more guarantees than true affine types, albeit less than true linear types.
    - mcaruso 9y ago
      Interesting! Thanks
    - Risord 9y ago
      Disclaimer: I am totally out of my field and I have no idea precise definitions of terms etc. Is it haulting really in conflict with linear types? If we inspect function from outside and we pick random time T after starting (but before finish) the event has been happen at most once. After function is finished event is done exactly once. I think conceptually situation is pretty much the same is T: 1ns | trillion years | infinite. So I feel that "It WILL happen after infinite time." is valid claim and therefore haulting by itself is not a problem. In real world issue seems to be that we cannot run our software from very long to infinite time whenever is it haulted or not => at some point we kill that process. Killing process on the other hand is harmful thing for promise to run exactly once since killed process won't product anything new for sure. So in practice haulting results always to killing process but if process is killed it don't mean that process was haulted. So I claim that you shouldn't proof that your system won't hault but instead you should proof that process cannot be killed if anything. At the end it depends how we want box our world. What you think?
      - chriswarbo 9y ago
        You're right that proving that a program halts doesn't tell us whether or not it's practical to run (it could take 1 trillion years), but it can be useful for other reasons. For example, if a function claims to return a value of type T, and we can prove that the function halts, then we know that a value of type T must exist (it's whatever the function will return, however long that takes). This is how dependently typed languages can implement pre and post conditions: we can represent conditions as types, and put preconditions as extra argument types, and postconditions as extra return values (e.g. in a tuple). For example, we might have a function 'f1' which turns 'A' values into 'B' values: f1 : A -> B f1 myA = ... If we require some precondition 'PRE' to hold for the argument, and postcondition 'POST' to hold for the return value, we can use dependent types to represent them: f2 : (a : A) -> PRE a -> (b : B, POST b) f2 myA preProof = ... We can 'f1' by just giving it an 'A' argument, but the precondition won't be checked. Likewise, we learn nothing about whether the output satisfies the postcondition. With 'f2', we must give it an extra argument, representing a proof that the precondition holds for the given 'A' value. The function must also do more work: not only must it return a 'B' value, but it must also give us a proof that that 'B' value satisfies the postcondition (we can pass that proof around, e.g. if another function requires it as a precondition). If we can prove that these calculations will halt, then we don't actually need to run them at all! Knowing that 'PRE a' can be proved in a finite amount of time (however long) is itself a proof of 'PRE a'! (And likewise for 'POST b'). Hence we can "erase" this proof stuff after type checking, to generate code equivalent to 'f1'. If we don't know whether or not those proof calculations will halt, we can't use this shortcut, and we're forced to run the proof calculations in full at runtime (which may not halt, or might take a trillion years!).
- bjz_ 9y ago
  > Which, y'know, good luck with that. Most dependent type systems like Agda, Coq, Idris, Lean, and ATS have termination checking, so it is possible! They can't determine whether arbitrary programs terminate, but you can capture a large subset of programs. Turns out most code doesn't actually need Turing completeness.
  - noblethrasher 9y ago
    Since I've started paying attention, I've noticed that most of the code I write doesn't need anything more powerful than formal regular expressions, and vanishingly rarely needs to go beyond deterministic context-free.
    - geokon 9y ago
      Now you've got me curious :) Could you give some examples? I've never come across regular expressions outside of string handling

steveklabnik 9y ago

> I have heard about "affine types", don't know the difference Linear types: must be used exactly once Affine types: can't be used more than once

lmkg 9y ago

> I have heard about "affine types", don't know the difference A value with a linear type is used exactly once. A value with an affine type is used at most once. In other words, both types prevent double-use of single-use resources, but linear types additionally guarantee no leaks of said resources. True linear types are far less common in practice, because in order to prove that a value is actually consumed, you have to prove that the program doesn't go into an infinite loop first. Which, y'know, good luck with that.

mcaruso 9y ago
> True linear types are far less common in practice, because in order to prove that a value is actually consumed, you have to prove that the program doesn't go into an infinite loop first. Which, y'know, good luck with that. I don't know much about the subject, but I just read the GHC proposal and it seems they don't consider this an issue: https://ghc.haskell.org/trac/ghc/wiki/LinearTypes https://ghc.haskell.org/trac/ghc/wiki/LinearTypes (see: "Isn't a linear function that diverges unsound?")
- lmkg 9y ago
  Key quote from your link (emphasis added): > The properties of linear types which we need are not compromised by non-termination. This is an implicit admission that Haskell "linear types" are not "true" linear types, but instead only have a subset of the defining properties. I don't mean this in a disparaging fashion. Pretty much everyone uses the name "linear types" even though "affine types" is what they actually have. And I'm totally on-board with this. "Linear" is a more common word than "affine," and the defining difference isn't the property of linear types that most people care about (double-frees are a bigger deal than leaks). And, of course, the fact that you can't actually determine true linearity for Turing-Complete languages. For what it's worth, it sounds like Haskell's "linear types" provides slightly more guarantees than true affine types, albeit less than true linear types.
  - mcaruso 9y ago
    Interesting! Thanks
  - Risord 9y ago
    Disclaimer: I am totally out of my field and I have no idea precise definitions of terms etc. Is it haulting really in conflict with linear types? If we inspect function from outside and we pick random time T after starting (but before finish) the event has been happen at most once. After function is finished event is done exactly once. I think conceptually situation is pretty much the same is T: 1ns | trillion years | infinite. So I feel that "It WILL happen after infinite time." is valid claim and therefore haulting by itself is not a problem. In real world issue seems to be that we cannot run our software from very long to infinite time whenever is it haulted or not => at some point we kill that process. Killing process on the other hand is harmful thing for promise to run exactly once since killed process won't product anything new for sure. So in practice haulting results always to killing process but if process is killed it don't mean that process was haulted. So I claim that you shouldn't proof that your system won't hault but instead you should proof that process cannot be killed if anything. At the end it depends how we want box our world. What you think?
    - chriswarbo 9y ago
      You're right that proving that a program halts doesn't tell us whether or not it's practical to run (it could take 1 trillion years), but it can be useful for other reasons. For example, if a function claims to return a value of type T, and we can prove that the function halts, then we know that a value of type T must exist (it's whatever the function will return, however long that takes). This is how dependently typed languages can implement pre and post conditions: we can represent conditions as types, and put preconditions as extra argument types, and postconditions as extra return values (e.g. in a tuple). For example, we might have a function 'f1' which turns 'A' values into 'B' values: f1 : A -> B f1 myA = ... If we require some precondition 'PRE' to hold for the argument, and postcondition 'POST' to hold for the return value, we can use dependent types to represent them: f2 : (a : A) -> PRE a -> (b : B, POST b) f2 myA preProof = ... We can 'f1' by just giving it an 'A' argument, but the precondition won't be checked. Likewise, we learn nothing about whether the output satisfies the postcondition. With 'f2', we must give it an extra argument, representing a proof that the precondition holds for the given 'A' value. The function must also do more work: not only must it return a 'B' value, but it must also give us a proof that that 'B' value satisfies the postcondition (we can pass that proof around, e.g. if another function requires it as a precondition). If we can prove that these calculations will halt, then we don't actually need to run them at all! Knowing that 'PRE a' can be proved in a finite amount of time (however long) is itself a proof of 'PRE a'! (And likewise for 'POST b'). Hence we can "erase" this proof stuff after type checking, to generate code equivalent to 'f1'. If we don't know whether or not those proof calculations will halt, we can't use this shortcut, and we're forced to run the proof calculations in full at runtime (which may not halt, or might take a trillion years!).
bjz_ 9y ago
> Which, y'know, good luck with that. Most dependent type systems like Agda, Coq, Idris, Lean, and ATS have termination checking, so it is possible! They can't determine whether arbitrary programs terminate, but you can capture a large subset of programs. Turns out most code doesn't actually need Turing completeness.
- noblethrasher 9y ago
  Since I've started paying attention, I've noticed that most of the code I write doesn't need anything more powerful than formal regular expressions, and vanishingly rarely needs to go beyond deterministic context-free.
  - geokon 9y ago
    Now you've got me curious :) Could you give some examples? I've never come across regular expressions outside of string handling