I like the ideal of “language minimalism” – that the language provide a minimal set of operators, and that all further operations be modeled atop those. With regards to code proofs, language minimalism means we have less to trust and validate.
Arrow primitives are a sufficient minimal set for ad-hoc data plumbing:
first :: (x~>x')*(x*y) ~> (x'*y)
swap :: (x*y) ~> (y*x)
assocl :: (x*(y*z)) ~> ((x*y)*z)
intro1 :: x ~> (Unit*x)
elim1 :: (Unit*x) ~> x
-- SOME DERIVED PLUMBING
assocr :: ((x*y)*z) ~> (x*(y*z))
assocr = swap assocl swap assocl swap
rot2 :: (x*(y*z)) ~> (y*(x*z))
rot2 = assocl [swap] first assocr
second :: (y~>y')*(x*y) ~> (x*y')
second = swap [swap] first swap first swap
rot3 :: (a*(b*(c*d))) ~> (c*(a*(b*d)))
rot3 = [rot2] second rot2
zip2 :: ((a*b)*(c*d)) ~> ((a*c)*(b*d))
zip2 = assocr rot3 rot2 assocl
However, it’s worth noting that most of these derivations use blocks, i.e. capturing code as a literal. In the single-stack environment, this wasn’t a problem: the block was simply dropped on top of the stack, and `first` would immediately apply it. The multi-stack environment presents a new challenge, though.
Our multi-stack (plus hands) environment looks like `
(sL*(sC*sR))*(lH*rH)`. Literals, including blocks, are now primitives that expect this environment and add to the current stack (sC). So if we start defining rot2 and add the `
[swap]` block, we cannot immediately apply `first`, since [swap] is buried deep within our environment.
Further, all my rich data plumbing that might extract the swap block for application will add even more blocks to the stack.
I determined that the necessary data plumbing must be defined without using blocks, even if that means adding new language primitives. The question, then, is what is a minimal set of primitives to work without blocks? Since my head was already swimming from staring at equations, I decided to let my computer help me derive the needed functions. I pulled out Prolog.
% certain primitives (excluding id)
% derivable functions (without using blocks)
% test for a function of up to N elements.
path(X,Y,N) :- uPath(X,Y,N,[X],P),length(P,NL)
% add primitive
uPath(X,Y,N,H,[OP|P]) :- (N > 0),prim(X,OP,S),
% add library function
(N > 0),lib(X,W,S,_),
% function found!
uPath(X,X,N,_,) :- (N >= 0).
Here, I’m simply using Prolog’s lists to model product types, and I can test for a function of up to a given length. The next questions I had were: “which functions should I be able to implement without blocks?” and “what primitives would I be willing to implement?”
The functions I decided to look for were:
- The basic rot2, rot3, zip2, second, already described above.
- ‘insert’ value from outside enviroment to current stack, and ‘extract’ it back
- insertStack and extractStack, same as insert and extract except takes current stack
- take: move top element from current stack to right hand
- put: move element from right hand to current stack
- appE: apply top block on current stack to whole environment
- appS: apply top block on current stack to rest of current stack
- appX: apply top block on current stack to the second element of the current stack
I approached this initially by proposing a few primitives that I would be willing to implement, and trying to minimize that set. I’d rather not walk through the derivation process (it involved lots of edit-and-test on the Prolog), so I’ll just skip to the conclusion: if I add rot3 to my primitives, I can derive the other data plumbing without using blocks.
rot2 = intro1 rot3 intro1 rot3 elim1 elim1
zip2 = assocr rot3 rot2 assocl
insert = rot2 swap rot3 rot2 zip2 rot3 rot3 swap
extract = swap rot3 zip2 rot3 rot2 swap rot2
insertStack = assocl swap rot3 rot2 swap
extractStack = swap rot3 assocl swap rot2
take = extract rot3 rot3
put = rot3 insert
second = assocl swap rot2 first swap
appE = extract intro1 swap assocr first swap elim1
appS = extractStack assocr first insertStack
appX = extract rot2 extract rot3 first insert
Sweet! Data plumbing without blockage!
(I wonder if there’s any plumbing that can’t be done with just a sequence of rot3, swap, assocl, intro1, and elim1.)
Anyhow, with this I can now properly bootstrap Awelon, without trying to shove blocks past one another. All of this data plumbing will be optimized away by the compiler, so I’m not worried about it building up like it seems to be.