Luke refactored a bunch of code into js/src/vm/Stack.h. In a comment on the JS engine internals group, he wrote (emphasis mine):

David and Waldo raised the very reasonable question of whether

`js::StackFrame`

should be in its own file rather than in vm/Stack.h (its big). My reasoning for not wanting to is that`FrameRegs + StackFrame + StackSegment + StackSpace + *FrameGuard`

altogether forma single logical data structure which I’d like to present as a whole[…] The same perspective shows up in math as many-sorted algebra so its not just C++ crazy-talk ðŸ™‚

None of us could figure out what that last sentence meant. We prevailed upon Luke to elaborate. I thought his explanation was a nice insight, so I’m sharing it here.

I’ll hazard an answer, knowing full well that there are at least three PhDs on the list who know a lot more about this than I do and may smite my answer with truth. (I’m at a layover in Hong Kong — be gentle ðŸ™‚

A single-sorted algebraic “structure” is something like a monoid, group, ring, field, etc: an abstract domain with a collection of operations (over this domain) and axioms that the operations must satisfy (e.g., distributivity, associativity, commutativity, etc). A single-sorted “algebra” implements a structure by picking a particular domain and set of operations that satisfy the axioms of the structure. (For example, the ring structure specifies an abstract + and * with a couple of axioms (associativity of +, distributivity, inverse for + and *, etc); the integers with arithmetic + and * are an algebra).

An important idea about all this is that, when you prove things about an algebraic structure, the proof is expressed only in terms of the declared operations/axioms of the structure, and not the particular details of any one algebra, so your theorem holds for all algebras of that structure. Now this starts to sound like abstract data types in computer science (s/structure/public interface/, s/axioms/specification/, s/algebra/concrete class/) and we can see that abstract algebraists are kinda like programmers who really really like reusable code.

A many-sorted structure/algebra is just the extension of the concept that can have more than one domain (thus, the operations can include more than one domain in their signature). An example is a vector space (which has a domain of scalars and a domain of vectors).

So then what’s the correspondence of these multi-sorted structures/algebras in programming? Classes/interfaces (of mainstream OOP languages) associate all operations with a single domain of values. I have little doubt there exist languages which solve the problem directly. We can hack multi-sorted-ness in C++ while maintaining some semblance of interface/implementation separation by just having multiple classes (one per domain) and making them all friends of each other. Then there is the question as to how to distribute the operations between the classes (or perhaps as non-member functions), but unless you want runtime polymorphism (which requires something like multi-methods), it’s a question of aesthetics.

I mentioned this originally because recognizing many-sorted algebras as a peer concept to single-sorted algebras helps to avoid a design mindset of “every class must be its own encapsulated island” which I feel can be detrimental when trying to modularize complex data structures like we have in SpiderMonkey. The Stack was one example; I think low-level objects + property tree will be another.

Very interesting stuff. I’m not familiar with model theory, but I think I get the intuition behind having multiple domains to define your operations on. Since algebraic structures are defined as type classes in Haskell, I think multi-parameter type classes would be able to define many-sorted algebraic structures: http://www.haskell.org/haskellwiki/Multi-parameter_type_class

(BTW, I have an exam in around 16 hours from now, and I just couldn’t resist spending an hour thinking about this stuff and how it all works out. If I fail the exam it’s all your fault. ðŸ˜› )

Yes! Haskell multi-parameter type classes are exactly this. Good call!

An hour away from studying is good for the brain. You’ll do fine.