5 ms·

> it is rarely fully understood I beg to differ. Case in point: type classes, the Monoid type class, and Monoids as the mathematical concept; all well understo

> it is rarely fully understood I beg to differ. Case in point: type classes, the Monoid type class, and Monoids as the mathematical concept; all well understood, proofs of their existence and properties are stated exactly, and when implemented by a compiler behaves exactly as expected when the program is executed. This is precisely what people mean when they say "abstraction is the essence of progamming"... ... when they understand what abstractions are and use a precise definition. Unfortunately there exist many programmers in the world who do not use precise definitions and don't know how to state mathematical laws or invariant properties of relations. They too use the word "abstraction" and they often mean... whatever it is they mean. It differs from person to person and is often used when they're waving their hands and trying to make a point. Update: The overwhelmingly vast majority of programmers don't think about integer representations and how arithmetic is implemented these days; some do and that's fine, but the software world continues to ship vastly complex programs and systems without having to care about it and everything still works. That's abstraction at work.

cwzwarich 4y ago
Those abstractions are still leaky, e.g. it's entirely possible that an optimizing compiler could apply correct monoid laws and end up with a program that has vastly different space usage.
- agentultra 4y ago
  Without abstraction it would be difficult to write a proof that your implementation of the monoid laws stay within specified bounds. It's not "leaky" if the specification doesn't say anything about the space bounds. That's a separate concern from "abstraction" itself. Update The idea of a monoid is divested of any real-world implementation and that's what makes it useful (and consequently also hard to explain). The important thing is that there are laws to how the operations on monoids compose and relate to one another that must be maintained no matter how they're implemented in an actual computer.
cloogshicer 4y ago
I'm one of those programmers you mentioned. Could you help me? I'm genuinely trying to learn more about this. What is the precise mathematical definition of the term abstraction? Any links to good resources are appreciated.
- agentultra 4y ago
  > Mathematical abstraction is the process of considering and manipulating operations, rules, methods and concepts divested from their reference to real world phenomena and circumstances, and also deprived from the content connected to particular applications. https://journals.openedition.org/philosophiascientiae/914?lang=en https://journals.openedition.org/philosophiascientiae/914?la...
  - cloogshicer 4y ago
    Thanks for the link!
a1369209993 4y ago
> Case in point: type classes, the Monoid type class, and Monoids as the mathematical concept; [...] when implemented by a compiler behaves exactly as expected when the program is executed. Not true in general. For some specific instances (such as fixed-size Int under addition or multiplication[0]), it works[1], but in the general case (eg Integer under add or mul, [Foo] under concat) `a <> b` can fail with out-of-memory if a and b are large enough. (This debateably violates closure of `<>` (you could say `undefined`/`error "out of memory"`/etc is a valid element), but indirectly breaks all the other Monoid laws like `(a<>b)<>c==a<>(b<>c)`, since the result is `undefined`(/etc), rather than `True`.) 0: Actually, I'm not sure it's true even then: does Haskell actually guarantee 2s-complement truncation on overflow? 1: Give or take "How many bits does Int truncate to?".
- agentultra 4y ago
  Isn't this why fixed, signed integer types don't have a Monoid instance? https://hackage.haskell.org/package/base-4.17.0.0/docs/Data-Int.html https://hackage.haskell.org/package/base-4.17.0.0/docs/Data-... For arbitrary sized `Integer` type, which is basically a libgmp arbitrary integer, we also don't have a Monoid.
  - a1369209993 4y ago
    > Isn't this why fixed, signed integer types don't have a Monoid instance? No. Integers (signed or unsigned, fixed or arbitrary-precision) don't have Monoid instances since Haskell requires a single class instance per type, and it's ambigous which instance should be the "canonical" one. The types `Num a => Sum a` and `Num a => Product a` have Monoid instances, but it's not clear whether the "canonical" instance for a given integer type should have `(<>)` defined as `(+)` or `(*)`... or `min`, `max`, `and`, `or`, `xor`, `lcm`, `gcd`, or any of several dozen other monoidal operations. Conversely, `[a]` doesn't really have any resonable monoidal operation other then `concat`, and most of the existing Monoid instances (most conspicuously Sum and Product above) are even more nothing-else-is-reasonable, if only because of their names.
    - 4y ago

cwzwarich 4y ago

Those abstractions are still leaky, e.g. it's entirely possible that an optimizing compiler could apply correct monoid laws and end up with a program that has vastly different space usage.

agentultra 4y ago
Without abstraction it would be difficult to write a proof that your implementation of the monoid laws stay within specified bounds. It's not "leaky" if the specification doesn't say anything about the space bounds. That's a separate concern from "abstraction" itself. Update The idea of a monoid is divested of any real-world implementation and that's what makes it useful (and consequently also hard to explain). The important thing is that there are laws to how the operations on monoids compose and relate to one another that must be maintained no matter how they're implemented in an actual computer.

cloogshicer 4y ago

I'm one of those programmers you mentioned. Could you help me? I'm genuinely trying to learn more about this. What is the precise mathematical definition of the term abstraction? Any links to good resources are appreciated.

agentultra 4y ago
> Mathematical abstraction is the process of considering and manipulating operations, rules, methods and concepts divested from their reference to real world phenomena and circumstances, and also deprived from the content connected to particular applications. https://journals.openedition.org/philosophiascientiae/914?lang=en https://journals.openedition.org/philosophiascientiae/914?la...
- cloogshicer 4y ago
  Thanks for the link!

a1369209993 4y ago

> Case in point: type classes, the Monoid type class, and Monoids as the mathematical concept; [...] when implemented by a compiler behaves exactly as expected when the program is executed. Not true in general. For some specific instances (such as fixed-size Int under addition or multiplication[0]), it works[1], but in the general case (eg Integer under add or mul, [Foo] under concat) `a <> b` can fail with out-of-memory if a and b are large enough. (This debateably violates closure of `<>` (you could say `undefined`/`error "out of memory"`/etc is a valid element), but indirectly breaks all the other Monoid laws like `(a<>b)<>c==a<>(b<>c)`, since the result is `undefined`(/etc), rather than `True`.) 0: Actually, I'm not sure it's true even then: does Haskell actually guarantee 2s-complement truncation on overflow? 1: Give or take "How many bits does Int truncate to?".

agentultra 4y ago
Isn't this why fixed, signed integer types don't have a Monoid instance? https://hackage.haskell.org/package/base-4.17.0.0/docs/Data-Int.html https://hackage.haskell.org/package/base-4.17.0.0/docs/Data-... For arbitrary sized `Integer` type, which is basically a libgmp arbitrary integer, we also don't have a Monoid.
- a1369209993 4y ago
  > Isn't this why fixed, signed integer types don't have a Monoid instance? No. Integers (signed or unsigned, fixed or arbitrary-precision) don't have Monoid instances since Haskell requires a single class instance per type, and it's ambigous which instance should be the "canonical" one. The types `Num a => Sum a` and `Num a => Product a` have Monoid instances, but it's not clear whether the "canonical" instance for a given integer type should have `(<>)` defined as `(+)` or `(*)`... or `min`, `max`, `and`, `or`, `xor`, `lcm`, `gcd`, or any of several dozen other monoidal operations. Conversely, `[a]` doesn't really have any resonable monoidal operation other then `concat`, and most of the existing Monoid instances (most conspicuously Sum and Product above) are even more nothing-else-is-reasonable, if only because of their names.
  - 4y ago