4 ms·

At the assembly level, we are always working with continuation passing style. Normal calls are implemented by pushing their "return address" on the stack and th

by fmap 9y ago

At the assembly level, we are always working with continuation passing style. Normal calls are implemented by pushing their "return address" on the stack and then jumping to it after the procedure has finished. Formally, this is exactly a continuation. However, all continuations here are linear (or rather affine - called at most once) and this allows you to allocate and free "closures" for your continuations with a stack discipline.

JadeNB 9y ago
> all continuations here are linear (or rather affine - called at most once) Does the term 'linear' just not exist in this context, or does it have a different meaning?
- lmkg 9y ago
  Linear means called exactly once. Linearity requires proof that the value is definitely used, which is tricky. Affine types are more common in practice, even though people will call them linear.
  - gugagore 9y ago
    How does this relate to linear(/affine) as in e.g. y = mx (+ b) ?
    - drdeca 9y ago
      It's related to linear logic and affine logic, and both are kinda related to linear algebra I think. With linear algebra, a function f is linear if, for any a,b, f(a+b)=f(a)+f(b) Suppose there is a vending machine that sells soda for $1 each (doesn't have a menu, just dispenses the soda, for simplicity). If you put in $1, you get a soda. If you put in $1+$1, you get a soda + a soda. The amount of soda you get is linear in the amount of money you put in. This might not be a correct explanation of why it is called linear. Also I don't really understand how the affine fits in this analogy, other than that "affine" is a somewhat weaker assumption than linear. I hope someone can give a better answer than I did, because I thought I knew the answer, but when I tried to explain it, I found that I did not really know the answer.
    - JadeNB 9y ago
      I wondered the same! It seems to have to do with Girard's idea that linear logic involves 'additive' and 'multiplicative' 'universes' (all words in quotes because I've only skimmed to try to get an idea—even the editors of TCS apparently found the paper unreferee-able). See logical p. 3 (physical p. 4) of http://iml.univ-mrs.fr/~girard/linear.pdf http://iml.univ-mrs.fr/~girard/linear.pdf . (How exponentials fit into the picture I don't know.) Then drdeca (https://news.ycombinator.com/item?id=14684219 https://news.ycombinator.com/item?id=14684219) 's explanation of why affine logic is so called seems plausible, but I haven't looked into it.
    - JadeNB 9y ago
      It was suggested on LtU that Girard explicitly addressed this connection, although it may still be somewhat rarefied; see the "Added in print" note at the bottom of logical p. 131 of http://www.sciencedirect.com/science/article/pii/0168007288900255 http://www.sciencedirect.com/science/article/pii/01680072889... .
kazinator 9y ago
Formally, it is no such thing. Assembly language programs in the conventional style save registers into the stack, and that's also where they put arguments when there are too many to put into the arg registers.

by fmap 9y ago

JadeNB 9y ago

> all continuations here are linear (or rather affine - called at most once) Does the term 'linear' just not exist in this context, or does it have a different meaning?

lmkg 9y ago
Linear means called exactly once. Linearity requires proof that the value is definitely used, which is tricky. Affine types are more common in practice, even though people will call them linear.
- gugagore 9y ago
  How does this relate to linear(/affine) as in e.g. y = mx (+ b) ?
  - drdeca 9y ago
    It's related to linear logic and affine logic, and both are kinda related to linear algebra I think. With linear algebra, a function f is linear if, for any a,b, f(a+b)=f(a)+f(b) Suppose there is a vending machine that sells soda for $1 each (doesn't have a menu, just dispenses the soda, for simplicity). If you put in $1, you get a soda. If you put in $1+$1, you get a soda + a soda. The amount of soda you get is linear in the amount of money you put in. This might not be a correct explanation of why it is called linear. Also I don't really understand how the affine fits in this analogy, other than that "affine" is a somewhat weaker assumption than linear. I hope someone can give a better answer than I did, because I thought I knew the answer, but when I tried to explain it, I found that I did not really know the answer.
  - JadeNB 9y ago
    I wondered the same! It seems to have to do with Girard's idea that linear logic involves 'additive' and 'multiplicative' 'universes' (all words in quotes because I've only skimmed to try to get an idea—even the editors of TCS apparently found the paper unreferee-able). See logical p. 3 (physical p. 4) of http://iml.univ-mrs.fr/~girard/linear.pdf http://iml.univ-mrs.fr/~girard/linear.pdf . (How exponentials fit into the picture I don't know.) Then drdeca (https://news.ycombinator.com/item?id=14684219 https://news.ycombinator.com/item?id=14684219) 's explanation of why affine logic is so called seems plausible, but I haven't looked into it.
  - JadeNB 9y ago
    It was suggested on LtU that Girard explicitly addressed this connection, although it may still be somewhat rarefied; see the "Added in print" note at the bottom of logical p. 131 of http://www.sciencedirect.com/science/article/pii/0168007288900255 http://www.sciencedirect.com/science/article/pii/01680072889... .

kazinator 9y ago

Formally, it is no such thing. Assembly language programs in the conventional style save registers into the stack, and that's also where they put arguments when there are too many to put into the arg registers.