[HN Gopher] What the heck is a homomorphic mapped type?
___________________________________________________________________
What the heck is a homomorphic mapped type?
Author : kiyanwang
Score : 70 points
Date : 2024-01-06 11:58 UTC (1 days ago)
(HTM) web link (andreasimonecosta.dev)
(TXT) w3m dump (andreasimonecosta.dev)
| retrac wrote:
| 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".
| kvdveer wrote:
| Your explanation is so much easier to parse than TFA, thank you
| very much.
| dboreham wrote:
| It's all the same: Mathematics is a kind of programming,
| programming is a kind of Mathematics. Mathematics people get to
| use longer words.
| edejong wrote:
| ...and shorter variable names.
| Sharlin wrote:
| 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.
| mancerayder wrote:
| As an engineer without a comp sci/mathy background, I wanted to
| say - thanks for an excellent and simple explanation to this
| foundational concept!
| wging wrote:
| 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.
| skybrian wrote:
| Is preserving one operation enough to call it a homomorphism?
| How trivial can that operation be?
|
| If we have an is_positive() operation, maybe mapping numbers
| to either -1 or 1 is enough? Or maybe map to true or false?
| ajross wrote:
| > type-obsessed languages
|
| 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.
| layer8 wrote:
| 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.)
| jandrewrogers wrote:
| 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.
| muglug wrote:
| If you're somewhat new to TypeScript, this doc explains what a
| mapped type is (with a wonderful example referencing Only Fools
| And Horses):
|
| https://www.typescriptlang.org/docs/handbook/2/mapped-types....
| Klathmon wrote:
| 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.
| epolanski wrote:
| > My biggest pet peeve with typescript is how it never explains
| most of this stuff officially.
|
| From my anecdotical experience, 99 % of people cannot even
| define a mapped type or other core TypeScript concepts.
| resoluteteeth wrote:
| 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.
| wavemode wrote:
| Even PureScript ended up ditching the whole row-polymorphic
| Eff thing and now uses one big IO monad (called "Effect").
|
| The juice ended up not being worth the squeeze, so to speak.
| miiiiiike wrote:
| > My biggest pet peeve with typescript is how it never explains
| most of this stuff officially.
|
| 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.
| ksjskskskkk wrote:
| i can't imagine the abuse that's is working with JavaScript to
| hail typescript as the salvation. I'm sorry for all of you.
| epolanski wrote:
| What is the alternative? Because I tried them all from
| Clojurescript, Scala.js to Elm.
|
| TypeScript is a very pleasurable language to use.
| ksjskskskkk wrote:
| you just listed worse tortures and confirmed the abuse
| clouding your judgment.
|
| like pollution, with js the only effective action is
| reduction.
| epolanski wrote:
| You realize your comments come out just snarky and unaware?
| Not much value is added to the discussion.
| titzer wrote:
| > 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.
| kristopolous wrote:
| 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.
| rickstanley wrote:
| What is PL?
| tejtm wrote:
| programing language
| skybrian wrote:
| In this case, programming language research.
| mrkeen wrote:
| > 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.
| tubthumper8 wrote:
| > 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)?
| rkagerer wrote:
| Darn, I thought this would be some kind of data type primitive
| related to hommomorphic encryption.
___________________________________________________________________
(page generated 2024-01-07 23:01 UTC)