Three Dollar Quill

No luck thinking about my other projects, so right now I'm thinking about a paper that I got linked earlier today, A Foundation for Typed Concatenative Languages. This paper sets out an equivalent to the lambda calculus, but for concatenative languages. One thing it mentions towards the end is that the expressiveness is somewhat limited by the needs of type inference, as opposed to the explicit type annotations involved with even a simply-typed variant.

Now, it mentions some issues with specifying a simply-typed variant, but if it goes into detail on them, then I didn't read the paper closely enough. That said, I'm going to charge ahead with the first idea I thought of. To whit, my experience with bidirectional typing is that it allows for much of the syntax to match the untyped calculus, with just the addition of a single ascription operation. Now, I'll say up front one of the issues that occurred to me as I was writing this up, which is that I'm not sure it will actually deliver on the particular expressiveness gains that are in question here. As I see it, the goal is to allow for type sequences to freely mix individual types and sequence variables, and I'm not sure if the stuff I have in mind will actually accomplish that.

If I'm thinking about this correctly (load-bearing "if")... Let's suppose we have an ascription that contains a sequence or individual variable. An individual variable can match itself, or maybe needs to be specialized, not sure. A sequence variable has to apply to an arbitrary expression instead of a single word. I guess it can work via binding.

I'll try hand-waving now. Suppose we've taken a function, and ascribed it a type that takes two sequences, and returns them in the other order. I'm not sure this can be implemented, so this thought experiment is likely to run into problems, but it might not. The call expression should probably synthesize, so we have it... I'm not getting any insight out of thinking about this.

Part of the problem, besides that I'm not writing stuff down on paper, is that I'm not sure what "the right" way to bidirectionalize lambda-compose is.

...

Taking another look at figure 5, I suppose the issue is the Lam rule, right? It decomposes a sequence, so it would need to handle leading sequence variables, right?

I'm not sure; I'm not getting anywhere tonight.

Good night.