6 ms·

How this semantics is extended to handle named multi-stacks? For instance, how is interpreted the main example of the introduction [1]? {fn f => {spread $

How this semantics is extended to handle named multi-stacks? For instance, how is interpreted the main example of the introduction [1]? {fn f => {spread $x $y $z} {$z drop} {$y clone square pop} {$x square pop} add {$y abs pop} sub } Notably, how to interpret the second use of $y that makes sense only because the former y value has been duplicated in the first $y call? [1] https://www.dawn-lang.org/posts/introducing-dawn-(part-1) https://www.dawn-lang.org/posts/introducing-dawn-(part-1)

smaddox 5y ago
My next post will cover this :-)
js8 5y ago
Not author, but TBH I don't see the advantage of his multi-stack proposal compared to local variables as in Factor; I think they are equivalent actually. If Factor had full stack type inference, you could look between any two words and ask what the state the stack is in. Then if you wanted to split the word definition inside the local binding at that point (assuming this is something useful to do, I am not convinced), then automatic algorithm to do that would be just: Put the required locals to the stack manually at the end of the last word, and then define the next word as having that stack as input. As a special case, you could extract any sub-sequence that doesn't really manipulate the stack into a word. I am also not clear what the advantage of multistacks is for side effect control. In Factor, there is already an implicit set of globals that are available at any point, i.e. all the words in the vocabulary. And there already is, on top of that, a mechanism how to restrict all callees from using certain words (for example, restrict only to pure subset, or subset with certain capabilities); this can also be formally verified. I just think that simply restricting the used vocabulary is a more powerful mechanism for restricting effects. But I guess I will learn this in the next blogpost, looking forward to it!
- Twisol 5y ago
  > I am also not clear what the advantage of multistacks is for side effect control. If you only ever push "effects" onto a stack, you're just building up a trace. The CALM theorem (Consistency as Logical Monotonicity) tells us that concurrent systems can coordinate as long as published information is increased monotonically (rather than destructively changed); as a limiting case, traces are the trivial representation of a series of operations as a monotonically growing set of information. The alignment between these domains makes me really excited for the next posts in this series. I'm expecting to see a restriction on "drop" for stacks of this type (as alluded to in this post). And if any reader only ever reads a limited suffix of the stack, the runtime (or compiler!) can eagerly prune unreachable parts of the stack. Also, this makes me very excited for coroutines in this language. I don't think the "main" stack is specially identified in any way, it's just the stack you were using before focusing on another stack. Coroutines are then managed simply by focusing on their stack before resumption; their main stack is simply the ambient one we've set up for them. (Though you may have to do some amount of stack virtualization to avoid needing to generate new stack names; the multistack reduction I posited in a nearby comment relies incidentally on all stack names being statically known.)
  - smaddox 5y ago
    > If you only ever push "effects" onto a stack, you're just building up a trace. That's an interesting concept, but not my plan for capabilities/effects. Instead, I'll be relying on linearity and qualified types. > Also, this makes me very excited for coroutines in this language. I am interested to see how they work out, too! I've only done a small amount of brainstorming about how they work. I'll likely need to give it some more thought as I formalize the multistack semantics.
- smaddox 5y ago
  > [...] TBH I don't see the advantage of his multi-stack proposal compared to local variables as in Factor [...] Local variables effectively turn the language into the lambda calculus. They're equivalent in the sense of any two Turing-complete languages being "equivalent", but there are important distinctions. First, allowing the binding of values to variables breaks automatic enforcement of linearity (and of the other substructural sub-languages when intrinsics are restricted). Second, it breaks the concatentive principal and forces you to worry about variable hoisting and renaming when factoring and refactoring. > I am also not clear what the advantage of multistacks is for side effect control [...] It's less about control and more about ergonomics and simplicity. Multistacks will essentially give us a capabilities/effects system for free, once we have qualified types with type inference.
Twisol 5y ago
I'm guessing we'll see a reduction much like those for multi-head or multi-tape Turing machines to single-tape, single-head, classical Turing machines. First, let's suppose the main ("unnamed") virtual stack has index 0, and the others ($x, $y, $z, and so on) have positive indices. Our "physical" stack will contain these virtual stacks as quotations. The main stack is at the top (index zero), and other stacks are deeper in the stack (given by their index). Each virtual stack is represented by a series of nested quotations, so for example the stack "a b c" would be stored on the physical stack as [[[[nil] a] b] c]. We need to define `nil`; it should be something that turns a virtual stack underflow into a physical stack underflow, so let's pick: nil = [swap drop clone apply] clone apply If we want to push (or pop) an element between a virtual stack and the physical stack, we need to traverse down to it; meaning we need to store all of the stacks with index less than our target temporarily. We can do this by successively quoting and composing the top two elements of the real stack, so that given a stack `a b c d` we can move `a` to the second position (and `b c d` all into the first position) as `a [b [c [d]]]`; a `swap` then makes `a` available for immediate operation, after which we `swap again` before returning to the original configuration of the physical stack. Now, given a program to run, we can see all of the named stacks it uses. This lets us preallocate all of our virtual stacks onto the physical stack at startup. A virtualized stack operation will pop N elements from up to N virtual stacks onto the physical stack, perform some operation, and then push M elements from the physical stack onto up to M virtual stacks.
- smaddox 5y ago
  In the existing prototypes, only expression stacks are nested, not value stacks. The value multistack is flat and is modeled by a map from stack name to value stack. Eventually, when compiling to C (and potentially to machine code), values on the different stacks will effectively be assigned to slots on the C stack, which seems similar to what you're describing.
  - Twisol 5y ago
    > The value multistack is flat and is modeled by a map from stack name to value stack. Makes sense for a real implementation, of course. It's nice to have a theoretical reduction, though, so we know there's no semantic difference between using multiple stacks and using a single stack.

smaddox 5y ago

My next post will cover this :-)

js8 5y ago

Not author, but TBH I don't see the advantage of his multi-stack proposal compared to local variables as in Factor; I think they are equivalent actually. If Factor had full stack type inference, you could look between any two words and ask what the state the stack is in. Then if you wanted to split the word definition inside the local binding at that point (assuming this is something useful to do, I am not convinced), then automatic algorithm to do that would be just: Put the required locals to the stack manually at the end of the last word, and then define the next word as having that stack as input. As a special case, you could extract any sub-sequence that doesn't really manipulate the stack into a word. I am also not clear what the advantage of multistacks is for side effect control. In Factor, there is already an implicit set of globals that are available at any point, i.e. all the words in the vocabulary. And there already is, on top of that, a mechanism how to restrict all callees from using certain words (for example, restrict only to pure subset, or subset with certain capabilities); this can also be formally verified. I just think that simply restricting the used vocabulary is a more powerful mechanism for restricting effects. But I guess I will learn this in the next blogpost, looking forward to it!

Twisol 5y ago
> I am also not clear what the advantage of multistacks is for side effect control. If you only ever push "effects" onto a stack, you're just building up a trace. The CALM theorem (Consistency as Logical Monotonicity) tells us that concurrent systems can coordinate as long as published information is increased monotonically (rather than destructively changed); as a limiting case, traces are the trivial representation of a series of operations as a monotonically growing set of information. The alignment between these domains makes me really excited for the next posts in this series. I'm expecting to see a restriction on "drop" for stacks of this type (as alluded to in this post). And if any reader only ever reads a limited suffix of the stack, the runtime (or compiler!) can eagerly prune unreachable parts of the stack. Also, this makes me very excited for coroutines in this language. I don't think the "main" stack is specially identified in any way, it's just the stack you were using before focusing on another stack. Coroutines are then managed simply by focusing on their stack before resumption; their main stack is simply the ambient one we've set up for them. (Though you may have to do some amount of stack virtualization to avoid needing to generate new stack names; the multistack reduction I posited in a nearby comment relies incidentally on all stack names being statically known.)
- smaddox 5y ago
  > If you only ever push "effects" onto a stack, you're just building up a trace. That's an interesting concept, but not my plan for capabilities/effects. Instead, I'll be relying on linearity and qualified types. > Also, this makes me very excited for coroutines in this language. I am interested to see how they work out, too! I've only done a small amount of brainstorming about how they work. I'll likely need to give it some more thought as I formalize the multistack semantics.
smaddox 5y ago
> [...] TBH I don't see the advantage of his multi-stack proposal compared to local variables as in Factor [...] Local variables effectively turn the language into the lambda calculus. They're equivalent in the sense of any two Turing-complete languages being "equivalent", but there are important distinctions. First, allowing the binding of values to variables breaks automatic enforcement of linearity (and of the other substructural sub-languages when intrinsics are restricted). Second, it breaks the concatentive principal and forces you to worry about variable hoisting and renaming when factoring and refactoring. > I am also not clear what the advantage of multistacks is for side effect control [...] It's less about control and more about ergonomics and simplicity. Multistacks will essentially give us a capabilities/effects system for free, once we have qualified types with type inference.

Twisol 5y ago

I'm guessing we'll see a reduction much like those for multi-head or multi-tape Turing machines to single-tape, single-head, classical Turing machines. First, let's suppose the main ("unnamed") virtual stack has index 0, and the others ($x, $y, $z, and so on) have positive indices. Our "physical" stack will contain these virtual stacks as quotations. The main stack is at the top (index zero), and other stacks are deeper in the stack (given by their index). Each virtual stack is represented by a series of nested quotations, so for example the stack "a b c" would be stored on the physical stack as [[[[nil] a] b] c]. We need to define `nil`; it should be something that turns a virtual stack underflow into a physical stack underflow, so let's pick: nil = [swap drop clone apply] clone apply If we want to push (or pop) an element between a virtual stack and the physical stack, we need to traverse down to it; meaning we need to store all of the stacks with index less than our target temporarily. We can do this by successively quoting and composing the top two elements of the real stack, so that given a stack `a b c d` we can move `a` to the second position (and `b c d` all into the first position) as `a [b [c [d]]]`; a `swap` then makes `a` available for immediate operation, after which we `swap again` before returning to the original configuration of the physical stack. Now, given a program to run, we can see all of the named stacks it uses. This lets us preallocate all of our virtual stacks onto the physical stack at startup. A virtualized stack operation will pop N elements from up to N virtual stacks onto the physical stack, perform some operation, and then push M elements from the physical stack onto up to M virtual stacks.

smaddox 5y ago
In the existing prototypes, only expression stacks are nested, not value stacks. The value multistack is flat and is modeled by a map from stack name to value stack. Eventually, when compiling to C (and potentially to machine code), values on the different stacks will effectively be assigned to slots on the C stack, which seems similar to what you're describing.
- Twisol 5y ago
  > The value multistack is flat and is modeled by a map from stack name to value stack. Makes sense for a real implementation, of course. It's nice to have a theoretical reduction, though, so we know there's no semantic difference between using multiple stacks and using a single stack.