As for why type-obsessed languages use terms like this, I guess we can blame math, as the article briefly mentions. Something is homomorphic ("same form") if there is a map ("relationship, point-to-point equivalence") with another structure.
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".
I like your explanation overall. But "point-to-point equivalence" is a little off from the math notion of homomorphism, and I think also the type theory version, if I understand correctly how you're using that phrase. It seems to imply that the homomorphism is 1-to-1 (as does the phrase "if you know the mapping you can turn one into the other"), which isn't necessarily required for the mathematical idea of a homomorphism: homomorphisms can map multiple elements of the source space to a single element of the destination space. So there may not be a well-defined way to 'go back' from the result of applying the homomorphism to the original input. (A homomorphism that isn't 'lossy' in this way is called an isomorphism.)
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.
It depends what the fundamental operations are in your context.
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.)
If we're talking homomorphisms, no it can't: the whole point of the homomorphism is that the addition operation works regardless of whether you do it in the source space (2 + 4 = 6, then reduce mod 5) or the target space, where you're dealing with entirely different objects (2 mod 5 added to 4 mod 5, where each of these is an object in the target space and not an ordinary integer).
You seem to be describing a bijection. The core property of a homomorphism is that it preserves structural properties of the source in the target. But it doesn’t have to be reversible. A reversible homomorphism is called an isomorphism.
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.)
Nit (taking "homomorphism" to mean the more general notion of a morphism where you just preserve some property): an isomorphism is an invertible homomorphism where the inverse is also a homomorphism. For some structures (e.g. vector spaces+linear maps, and I believe all other algebraic structures), the inverse of a homomorphism is always also a homomorphism. For others (e.g. along the lines of your connectivity example, topological spaces+continuous maps), the inverse does not necessarily preserve the structure you are interested in.
Linear maps (aka linear transforms – scales, rotations, and shears) are a type of homomorphism probably familiar to many. Linear maps are quite intuitively "structure-preserving" – particularly, by definition they preserve vector-vector addition and scalar-vector multiplication:
f(v + u) = f(v) + f(u)
f(k * v) = k * f(v)
Homomorphisms that are also invertible (ie. bijective) are called isomorphisms, a term which is perhaps slightly more often encountered.
I'm not sure that the Earth as-a-sphere/as-a-projection is the best practical example. It is not isomorphic, which is a pretty strong requirement for representations that are not local mappings. For this reason, useful representations of the Earth that are not spheres tend to be homeomorphisms, like projections onto a cube, or embeddings.
The fact that projections are both popular and not isomorphic is a source of continuous pain when dealing with Earth-scale geospatial data models.
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.
> where T is a type parameter are known as homomorphic mapped types, which means that the mapped type is a structure preserving function of T.
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.
In the service of trying to be clear and not confuse anyone they actually create things that are confusing and obtuse.
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 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.
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.
> 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 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.
> 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)?
My biggest pet peeve with typescript is how it never explains most of this stuff officially.
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.
I could be wrong, but I think it's maybe because the creators of typescript aren't that interested in actively encouraging people to use this kind of stuff as an end to itself?
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.
Oh I didn't even know that, huh. I'm still hoping people eventually get the effect system approach to be sufficiently ergonomic for it to make it's way into more languages.
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".