Structural vs. Mathematical “Under” (2023)
11 points by Arya
11 points by Arya
Oh nice, I do really like that languages like BQN and Uiua implement the under operator. To me it seems like the distinction between the mathematical and the structural under aren’t all that hard to discern, so a single operator makes sense to me. Though I do appreciate the purity of the mathematical under, so it might be nice to have different operators for different concepts (though then you have to choose two glyphs for it, which also sounds hard).
On the similarity: I think the mathematical under is a special case of structural under! Structural under is a lens: you break up the input into a subpart and a context, change the subpart, and re-wrap with the context. With “drop 2” the context re-adds the first two elements. With invertible functions, like “log”, the context applies the inverse.
Just a small nit: under is not quite a lens, actually. To give an example for the mathematical variant: one of the lens laws is set l (view l s) s ≡ s; i.e., setting what you just got out doesn’t change anything. But then if we take view l s = L s (where the rhs means we apply the lens L to s, changing l to L due to some BQN shenanigans) and set l v s = v⌾L s, we transform the above law into something like
(L s)⌾L s ≡ s
However, taking L to be Square ← ⋆⟜2, we see that (Square ¯1)⌾Square ¯1 evaluates to 1 and not ¯1. You should rather see mathematical under as a kind of conjugation operation, in the sense that F⌾G x is the same as G⁼ F G x, where G⁼ is a right inverse of G.
Oh, let me see if I get what you mean. If I wanted to make a lens for Square, the first problem is that it’s not invertible–it has collisions. drop 2 has collisions too, but we can still make a lens by having the context remember the information that was dropped. So a lens for Square would have the context remember the sign of the original input, so that when you start with -2 and set its square to be 4 (which it already is), you get -2 back.
But BQN (and APL?) doesn’t define “under” this way: it uses Undo. Which is apparently a right inverse, despite the name sounding like left inverse!
This makes me think Under should just be a lens, and only use inverses for functions that are really invertible (or as invertible as possible given floating-point’s limitations).
Sort of, yes, if Square were invertible, then given the definition of under we see that (G x)⌾G x = G⁼ (G x) G x = G⁼ G x = x, so indeed this lens law (and all others, for that matter) is satisfied. However, I personally think of lenses as purely structural—they are somehow pointers into a larger data structure. They don’t necessarily need to be invertible (e.g., the function \(a, b) -> a can be turned into a lens), as that’s what set and view are for: providing enough context so that “modify this data structure at this pointer and then return the data structure” makes sense. I think structural under fits this description, while mathematical under doesn’t really.
Put another way for Square: according to the lens laws, set l has to satisfy some kind of “strong” surjectivity as a function of (Value, State) -> State. More explicitly, the law set l (view l s) s ≡ s implies that for every v there exists some s with set l v s = s. In particular, one picks v = (view l s) which should always satisfy this, and we have already seen that this fails for Square. So we actually have that ⌾Square is “not surjective enough”, if that makes any sense.
(I agree that ⁼ is unfortunately named, but it’s too late to change that now!)