Lambda the Ultimate

We showed in a forthcoming paper (CSF'24) that a compiler can translate high-level sequential code into a distributed concurrent program that uses cryptography to achieve security. All source-level security properties are preserved -- robust hyperproperty preservation. This requires a new kind of compiler correctness proof based on the kind of simulation used in Universal Composability.
See Acay, Gancher, Recto, Myers, "Secure Synthesis of Distributed Cryptographic Applications".

Haxl allows for IO operations to be batched by having Applicative operators that result in a "slightly unlawful" Monad instance -- rather than strictly having (<*>) = ap where ap f x = f >>= (<$> x), it's merely "morally equivalent," as it performs the IO operations in parallel rather than in serial as ap would do.

I'm wondering if it's possible to implement something similar in a language that implements effects in terms of delimited continuations rather than in terms of monads. It seems a lot less obvious how to do so, at least; when evaluating the arguments of an applicative-shaped function call (pure function, effectful arguments), the effect handler must process them one by one, and can't introspect on the continuation to see what future effects might be performed.

An unfortunate solution might be to have a domain-specific optimization pass, reliant on inlining and other optimizations, that notes an effect as having some "do these in parallel" operator and transforms a program that unconditionally performs multiple effects in sequence to a single effect that uses that operator. However, this is terribly unsatisfying, since it's a non-semantics-preserving optimization, rather than something that falls directly out of the user-written code.

I implemented a language a while ago.

Based on some feedback, I change it's syntax from concatenative:

https://github.com/cicada-lang/inet-cute

- Stack-based like forth.
- Simple and shorter code.
- Easy to do refactoring.

to applicative:

https://github.com/cicada-lang/inet-js

- JavaScript-like syntax.
- Using pattern matching to define interaction rule.
- Can use currying, because we have explicit parentheses.

But I am still not sure which is better.

What do you think?

website: https://inet.run

code: https://github.com/cicada-lang/inet-js

Hi There,

Perhaps someone here might be kind enough to check out a paper I have published at [1] and provide some feedback.

It is an analysis of the travelling salesman problem and the sorting problem, examining the topologies of their solution spaces.

1.- https://github.com/enriquepablo/article-tsp/blob/mirror/article.ipynb

Thank you.

I'm elbows-deep in a language implementation, and since (for a new experience) it's not some kind of LISP, I'm dealing with infix operators and implicit operator precedence. I solved a little problem and thought you all might find my rambling thoughts about it interesting.

I noticed that treating relational comparison operators strictly as context-free binary operators matches the way they are in many programming languages but does not match the way they're used in mathematics (and some other programming languages).

When I write
A < B < C < D

assuming we have a context-free parser and left-associative relative operations, this is
(((A < B) < C) < D)
and we wind up comparing the result of a comparison. But this is not what a mathematician means when they write that expression. Standard infix math notation wants it interpreted as
(A < B) && (B < C) && (C < D).

Engineering considerations say we want that with single subexpression evaluation and short-circuit semantics.

If generating code for a C program, the relop doesn't check whether the left subtree is another relop; all it knows is that the left subtree returned #false (or #true), so it compares its right subtree to that value. And treats booleans as a subrange of numbers [0..1], so the comparisons have humorous results that require "inside" knowledge about the binary representation of booleans to comprehend. We get single subexpression evaluation but no short-circuit semantics.

In languages like Java, comparing booleans and numbers is a static type error, because static type errors are probably more useful than humorous results that require inside knowledge about binary representation of booleans to correctly interpret. No subexpression evaluation, no short circuit semantics.

If it's a logic-descended language, the comparison may return NIL or a non-NIL value, and the non-NIL value it returns is the value of the last subexpression evaluated, meaning the value of the right subtree. This treats numbers as a subrange of boolean values (all of them are #true). And any relop whose left subtree is NIL returns NIL without evaluating its right subtree. An analogue of the mathematician's interpretation of chained relational operations falls out "naturally" and if you never do numeric operations on a value you got in a context that encouraged you to think of it as a boolean, you will never notice the difference. You also get single subexpression evaluation, you get short circuit semantics - all seems good!

But it breaks static type checking. This means NIL is its own type, and relational operators have to check for it at runtime, and it can get returned to continuations that expect numbers. So now everything that uses booleans or numbers has to do runtime type checking. From a static type checking POV treating numbers as a subrange of booleans is even more expensive than treating booleans as a subrange of numbers.

When I'm traversing the abstract syntax tree after parsing, I can have different code templates to emit code for relational operations. I pick one depending on whether a subtree or the parent node is or is not another relop. So I get static type checking, I get the mathematician's interpretation of chained relational operators, I get the efficiency of caching a single evaluation instead of expanding a macro and evaluating something a second time.... all is good.

But now I broke referential transparency. Identical subexpressions encountered in different contexts mean different things. All the type checking can be done statically, but the relational ops other than the root of the chain are making a choice between jumping to their own continuation site in their parent relational op (to return a number) or to the boolean continuation at the call site of the whole chain (to return #false). Only the root of the chain is special; it has no numeric continuation, and can jump instead to the exit continuation to return #true. This is statically typed return polymorphism.

I was considering whether to be upset about breaking referential transparency, but then I realized people are using languages with exceptions all the time without complaining about it, so referential transparency can take a walk, I guess, if it gets us static type checking.

I've recently been working on formalizing the type system for one of my programming languages. While writing out the rules for inference I found it helpful to use both traditional type syntactic inference as well as some categorical language. The back-and-forth is so common that I have considered color-coding terms to indicate when they correspond to an object or morphism in which category.

My question for LtU is whether color-coding seems goofy or maybe helpful in some contexts. I have considered alternatives and I think there are three options:

1) Color-code terms by Category
2) Add text describing which terms correspond to which Category
3) Alter the term/type syntax to make category an explicit syntactic property

I've just finished documentation on my new programming language ALT.

It took me a lot of attempts (+- 20 implementations in scala and typescript) to come up with the current semantics. I would be grateful for some feedback.

Info should be available at:
https://groups.google.com/g/pltea

Those of you who apply advanced PL ideas to operating systems might be interested in the upcoming PLOS 2023 workshop. See the abbreviated CFP below, and please consider submitting a short paper!

Thanks! ---

Eric.

Historically, operating system development and programming language development went hand-in-hand. Today, although the systems community at large retains an iron grip on C, many people continue to explore novel approaches to OS construction based on new programming language ideas. This workshop will bring together researchers and developers from the programming language and operating system domains to discuss recent work at the intersection of these fields. It will be a platform for discussing new visions, challenges, experiences, problems, and solutions arising from the application of advanced programming and software engineering concepts to operating systems construction, and vice versa.

Please visit the Web site for more info: https://plos-workshop.org/2023/