that's quite a metric signature

I think the point is that the C code being called is probably vectorized in your sense

In terms of paradigm, this whole thing should be pretty familiar to imperative programmers, who work with maps and sets and iterators like this all the time.

There's value in not forcing the programmer to talk to you in your language (declarative queries) but instead meeting them where they are.

The other thing is, we would not aspire to back this whole thing with an actual DB, which is the path ORMs went down. Instead, the relation type would be an in-memory datatype.

In particular, a fragment consisting of

- for loops over relations
- while loops with monotone conditions
- x ∪= y etc.

seems likely to be tractable.

Much as it is possible to write imperative code that the compiler can analyze to a functional DFG, especially in the absence of aliasing, in this language we'd analyze imperative code and emit RC.

Instead, I'm talking more about the idea of an imperative PL that has relations as a basic (known to the compiler) datatype, and where loop nests are compiled to relational calculus.

I think we may be talking about different things. When I say "relational", I don't mean that there is ambient non-determinism as in Prolog. I agree that mixing that with imperative programming is a bad idea in most cases.

I haven't looked into this deeply enough, but I always felt that the intersection of imperative and relational programming was underexplored.

Imperative languages should have query planner-like loop nest optimizations, opts that know about map/set semantics, data layout opts, incrementalization.

For quotient types, you don't quotient a type by another type, but instead by an equivalence relation, so the analogy is broken

Difference types are afaik impossible to have all the properties of the integers (e.g. 1 - 1 = 1 + (-1) = 0, so that would imply a map 1 -> 0)

Unless I'm unfamiliar with some history, John Backus's name is Backus, not Bakhaus?

My company is using a cool PL abstraction in our compute kernel language: it's imperative, but ordering of effects comes purely from data dependencies.

Side effectful ops have "token" inputs and outputs that reify fragments of the world. A typed version would be similar to separation logic.