What the heck is a homomorphic mapped type?
andreasimonecosta.dev
andreasimonecosta.dev
I'll use the example of actual maps. The Earth is a globe. There are projections (mappings) between Earth-as-a-sphere and Earth-as-a-flat-2D-projection. A globe and a projection are homomorphic; if you know the mapping you can turn one into the other. This is useful, because sometimes it's much easier to do certain things with one way of viewing the problem, for example, drawing a straight line between two points.
Unsurprisingly this comes up a lot in type theory. The globe and the projection are both types, and closely related types. And Haskell etc. borrowed the term because, well, type theory.
Quite a few things share common operations - lists and graphs, for example. If you have a graph and walk it, it produces a list. Graphs can be (with only partial structure preservation) collapsed into lists. So any algorithm that works on a list can work on a graph, in theory. In a language like Haskell you can use a list operator on a graph automatically, the compiler can work it out, just tell it how to walk the graph. This tendency to try to preserve those structures, to allow that sort of fancy lifting, gets a lot of emphasis in languages like Haskell and Typescript. And they call it homomorphism, though it has become rather far-stretched from its math roots, I suppose. As the Haskell Wiki puts it "a homomorphism is defined by a function's ability to preserve the operations of the two underlying structures involved in the mapping".
f(v + u) = f(v) + f(u)
f(k * v) = k * f(v)
An example is reduction mod 5: it's a (ring) homomorphism because the relevant laws of arithmetic work just the same if you do arithmetic in the ordinary integers then reduce the result mod 5, or if you instead reduce all numbers mod 5 first and then apply special 'modulo 5' versions of those arithmetic operations. (E.g. 7 + 19 = 26 = 1 mod 5, but also (7 mod 5 + 19 mod 5) = (2 mod 5) + (4 mod 5) = 1 mod 5, where that last '+' is addition mod 5 instead of integer addition.) But you don't, given just '1 mod 5', know whether the original source integer was 1, 6, 21, -4, or any of infinitely many other choices.
Another example: projecting 3d space down to 2d by just dropping the third coordinate: (x, y, z) -> (x, y). That's a vector space homomorphism, but there isn't a way to recover the z-coordinate given just (x, y).
An example from the Haskell wiki mentioned above (I think you're referring to https://en.wikibooks.org/wiki/Haskell/Monoids#Homomorphisms) is the `length` function: given only the result of applying the homomorphism, `length(a)`, it's not possible to recover a.
If we have an is_positive() operation, maybe mapping numbers to either -1 or 1 is enough? Or maybe map to true or false?
There are different types of map that we call "X homomorphism" for different types of algebraic structure X (groups, rings, fields, vector spaces, modules, algebras, etc). In an abstract algebra course you'd probably first encounter the definition of a 'group homomorphism' (preserves the group's multiplication operation, whatever that is: f(x*y) = f(x)*f(y)), and then a separate definition of a 'ring homomorphism' (preserves the ring's addition and multiplication, which are the two operations you have on a ring - f(x+y)=f(x)+f(y) and f(xy) = f(x)f(y)), etc. The definitions are similar, but they are distinct: a group homomorphism is between groups, a ring homomorphism is between rings, etc. (There's also a more formal sense in which they're examples of the same thing, you'd look into category theory for more on that.)
So what's going on in your example? Well, you could define a simple type of algebraic structure where, for any instances of that structure, you can only ask the question "is x positive" for one of its elements x and get a yes or no answer, and then define 'homomorphisms' between such structures as maps that take 'positive' elements of the source space to 'positive' elements of the destination space (and vice versa). But I'm not sure you'd really be able to use it for much. (On https://en.wikipedia.org/wiki/Homomorphism#Definition, that'd correspond to having exactly one unary operation μ(x) = is_positive(x) and no other operations, not even addition.)
It can just be integer addition. 2 + 4 = 6 = 1 mod 5 is a true statement.
That quip is really the essence of the disconnect. At its core, typesafety is a boring and practical technique used to prevent mistakes. And that's all it is. You model your software with some "typing" rules that more or less match the real world desires of its behavior, and that prevents you from accidentally confusing a FrobWidget with the FrobConfig from which it was instantiated. And that's a good thing.
But the problem is that mapping of abstract types to real world ideas is inherently glitchy and leaky, for the intractable reason that (1) software isn't ever going to completely match the desires for its real world behavior (because everyone wants slightly different things!) and (2) those desires are going to change over time anyway.
But that's not a pleasant situation for Serious Language People. So programming language theory ended up in the weeds trying to create a calculus to handle all the edge cases. And the result is nonsense like this.
Typesafety is good up to a point, and Haskell in particular launched itself way past that threshold. Rust too is clearly on the wrong side of it. TypeScript is aiming in that direction. Of modern languages, my feeling is that Java and Go and similar tools are probably closest to the sweet spot.
For example, if you have a property p(x, y) on points x, y in the source (e.g. in the geographic map example, p(x, y) might be the property that x and y are connected by land), then a homomorphism h that preserves p would mean that the target also has a similar property q, and that whenever p(x, y) holds, then q(h(x), h(y)) also holds.
However, there might be elements x ≠ y for which nevertheless h(x) = h(y). That is, the homomorphism may map different source elements to the same target element. One example is a projection from 3D space to 2D space.
Furthermore, there may be elements x and y for which p(x, y) does not hold but for which q(h(x), h(y)) holds. For example, in the geographic map example, the sea level in the target may be lower, so that there are more land connections than in the source. It’s still a homomorphism as long as all land connections in the source are mapped to land connections in the target. (But there may be non-connections in the source that become connections in the target.)
The fact that projections are both popular and not isomorphic is a source of continuous pain when dealing with Earth-scale geospatial data models.
I work in PL and this type of language is pervasive. It is motivated by wanting PL terminology to be precise, meaning it always means the same thing to everyone, because there are agreed upon, robust, mathematical definitions for specific terms.
The problem is that laypeople don't know PL terminology. It's incumbent on PL people to explain using words that people understand what they are trying to say. Those words that people understand can be made clear (but maybe not robust or precise) but it takes a really excellent command of language to do so.
I have my struggles with this. I have learned (and now occasionally teach) formal PL notations--semantics, inference rules, type systems. Occasionally I review papers in research fields (like POPL). Research papers are constantly pushing the boundaries and too-often flaunt complexity as a substitute for technical difficulty or depth. I fear PL has entered a spiraling Tower-of-Babble situation where only experts can understand what is in the field. And while that's true of practically any field, PL is particularly bad because it keeps inventing at best intimidating and at worst impenetrable mathematical notations that make reading PL papers impossible for the uninitiated. (Granted that the OP was just about jargon, not notation, but the wider point is that it is rampant in PL). In systems papers, one can read the words because there are fewer jargon words and generally no new weird notations.
The language in this documentation is self-serving to PL nerds and needs to be rewritten to target normal people. Anything else is just needless elitism and wankery, IMHO.
Some technical people get past this stage and realize the flaw while others clutch onto it as a virtue and double down.
Also, it's usually done sloppily. They'll mix in the imprecise with precise and you'll scratch your head trying to find what this particular documents special definition of a word is because you assume that they're trying to be excessively formal and must not just mean something informally when in fact they do.
Other times they'll just toss something in like "observer functoid" and assume that you know what they think it must mean.
It's just bad writing. In my head I just visualize a green college aged kid writing it thinking this is the big league. When you peal back the jargon curtain you invariably find it's just a couple basic ideas all dolled up strutting down an 8 1/2 x 11 catwalk in a word pageantry.
> The language in this documentation is self-serving to PL nerds and needs to be rewritten to target normal people. Anything else is just needless elitism and wankery, IMHO.
Which documentation are you referring to, the TypeScript documentation? That's very much written for normal people without math jargon. Or are you referring to the documentation for other languages (ex. Haskell)?
This is the perfect description of why "a monad is a monoid in the category of endofunctors" is such a meme-worthy statement. There's pretty much nobody who knows what a "monoid" or "endofunctor" is that needs the concept explained to them in the first place.
The docs try to dumb things down but in my opinion it just makes it harder to understand these more complex pieces. Like the article mentions, the typescript handbook no longer even mentions the term homomorphic!
After working with typescript heavily for a few years I kind of had a bit of an intuition for some of the details here, but the article helped finally explain it in a way that I can truly understand.
From my anecdotical experience, 99 % of people cannot even define a mapped type or other core TypeScript concepts.
Typescript's type system is extremely advanced, but it mostly only has such an advanced type system because that's the only way to support patterns that people are already using in javascript.
So for example, typescript has stuff like row polymorphism, because you may need to be able to add and remove properties to javascript objects, and row polymorphism is the only way to make that type safe, but it's not a language like purescript where the whole language is oriented around using row polymorphism for the effect system and the documentation is going to actively encourage you to use row polymorphism if you weren't already as a new pattern that you should use for your code.
The official documentation is simply going to tell you, if you try to look up how to add/remove properties in a type safe way, how you can do that within the type system.
Unfortunately I think this leads to a situation where only people who are already familiar with some of these ideas from other languages are really interested in experimenting with it, which may be a bit of a missed opportunity.
The juice ended up not being worth the squeeze, so to speak.
All of it is in the documentation.. And saying that, I ordered two books on Typescript this week exclusively to brush on on stuff like this. So, yep.
https://www.typescriptlang.org/docs/handbook/2/mapped-types....
TypeScript is a very pleasurable language to use.
like pollution, with js the only effective action is reduction.