Foundations of Dawn: The Untyped Concatenative Calculus
dawn-lang.org
dawn-lang.org
Dang, I think you buried the lede.
What would be an example of a computation more compactly expressed in the untyped concatenative calculus than in the binary lambda calculus [1] (where compactness can be directly measured as size in bits) ?
I suppose that your programs can also be represented in binary with 3 bits encoding the 6 intrinsics plus the two symbols '[' and ']', and the end of a program could be encoded by an unmatched ']' at the end.
Okay.
I like Forth too, but that's laying it on a tad thick, imo.
But that's my goal. I'm not really interested in writing just another programming language. Even if I fail miserably, hopefully breaking the work up into small pieces and publishing as I go will at least inspire others with similar goals.
There are also other projects that aim to make formal software development much easier [0][1] and of course there's SPARK Ada.
Dawn itself will be notably different, though still ultimately based on the same core calculus.
While you could build layers that express a more conventional set of language idioms, most of the value in using this language as opposed to some other will be in exploiting the unconventional expressiveness of the mechanics.
However, I don't think writing Dawn will be as unfamiliar as it might seem, especially to functional programmers.
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
}
[1] https://www.dawn-lang.org/posts/introducing-dawn-(part-1)
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!
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.)
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.
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.
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
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.
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.
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.
> to democratize formal software verification in order to make it much more feasible and realistic to write perfect software
to me that sounds like only people curious by nature or propense to try new programming languages as the language seems like an unfinished typed APL dialect, but perhaps I didn't get the idea enough.
Could you add some practical examples next to the theoretical points at each step?
Once we build up functionality nearing that of Dawn, it should be more feasible to provide practical examples that demonstrate the value of the language.
I have a question: Why not base this project on Factor, which has a pretty decent existing implementation and compiler? (But few people use it..)
I think one could add better typing to Factor by creating a separate module for words (like docs and tests are now) which would describe the types of each word (and also other stipulations). Then these could be type checked separately.
As an aside, I always thought that it would be nice if a programming language could specify "stipulations", kinda like assertions but instead of having them inside word definitions (programs), have them outside (so that you could refer to them). For example, if something is a monad instance, the stipulation could specify that it has to follow monad laws. It would be then possible to automatically verify these stipulations (like QuickCheck does it, for example) or just assume they are true and use them for automated program deriving (or during compilation for optimization). A word annotated as having a certain type is just a special case of stipulation. Factor already has some stipulations like that in the form of additional word annotations (e.g. the word is free of side effects).
I have some ambitious ideas that aren't really compatible with Factor, or with any other existing language.
1. Is the "main stack" (the unnamed one, the one your program begins with focus on) specially identifiable in some way? I note further down this comment tree that, if the "main stack" is simply whichever one happens to be in focus, there are some exciting possibilities for coroutines that are simply resumed in focus of the stack that they treat as their main.
2. Are stack names always statically known in Dawn? Put differently, can you generate fresh stack names at runtime? If so, what does that look like, and how does that impact a theoretical reduction from multi-stack Dawn to single-stack Dawn? If not, can you envision additional intrinsics for supporting coroutines without requiring the user program to virtualize stacks manually?
3. Do you have any thoughts on concurrency in general in Dawn? I'm a big fan of the mental model offered by concurrent logic paradigms (especially Saraswat's concurrent constraint programming), where concurrent systems interact monotonically over shared logical variables. I think there's a subtle and exciting alignment between that concept and your named stacks. Does this line up with any of your thoughts?
4. (A bonus) What happens when an operation is attempted on an empty stack? I assume some form of exceptional case occurs, but in the face of concurrency, would it make sense to yield execution until something else puts an element onto the stack? (Probably not, because of FIFO semantics, but it's a fun question!)
2. Yes, they're statically known.
3. It should ultimately be possible to compile Dawn to concurrent nets and therefore to evaluate concurrent sections concurrently, but I've spent very little time thinking about that. I definitely want to support traditional explicit multithreading and something like async/await M:N threading, but the details are unclear. It should be no less ergonomic or safe than Rust.
4. In Dawn it will be a type error. In the untyped calculus it's a runtime error.
Excellent!
> It should ultimately be possible to compile Dawn to concurrent nets and therefore to evaluate concurrent sections concurrently
I'm thinking more along the lines of Multicore OCaml's approach to concurrency, which uses effect handlers to support userland scheduling without requiring explicit support from the OS. In particular, I'm not asking for different parts of a program to execute truly in parallel.
From my standpoint, concurrency has more to do with how you structure your programs -- I think of it as another view on modularity. In particular, to "evaluate concurrent sections concurrently" is something a user program would do, not something the compiler has to implement in terms of lower-level primitives.
Correction: to interaction nets: https://en.wikipedia.org/wiki/Interaction_nets
This coincidence is curious.
[1] you can check this at https://mbuliga.github.io/quinegraphs/lambda2mol.html#y_comb...
where you can see how the term Y (\x.x) reduces. In the λ>mol textarea delete what is written there and just copy/paste
(\g.((\x.(g (x x))) (\x.(g (x x))))) input
then click the λ>mol button. Then the start button. Stop whenever you want.
[2] the graph akin to a pair clone - apply can be seen at https://mbuliga.github.io/quinegraphs/quinelab.html#howtolab
where you copy/paste this graph as written in the mol notation:
A input y x^FOE x output y
"A" is the apply node and "FOE" is a clone node (say).