Re:Case against OOP is understated, not overstated (2020)
by zozbot234 on Thursday February 10, 2022 @06:46PM
(#30294552)
They seem to be necessary if you want a notion of "equivalence" (for both values and types) that enables you to make functions, operations, constructs etc. independent of any notion of "underlying representation" as well as seamlessly applicable across equivalent 'representations'. This is desirable in both higher mathematics (where homotopy types were first developed) and software engineering, for much the same reasons.
[ Parent
| on HN ]
Re:Case against OOP is understated, not overstated (2020)
by arrow7000 on Thursday February 10, 2022 @08:41PM
(#30295704)
Could you explain this to a layman with an interest in FP?
Re:Case against OOP is understated, not overstated (2020)
by secdeal on Friday February 11, 2022 @05:23AM
(#30299642)
I read about this a while ago, I'm not an expert but this is my take on it:
In homotopy type theory an equivalence of types is a first class value that you can manipulate. And also you can separate types from their 'implementations'. Classic example is you have a Nat type, with a Peano construction (Nat is a zero or a successor of a Nat.) This is not very efficient, but you write functions with it, prove things etc. It's time to optimize, and you change your Nat implementation to something more efficient (e.g. a Nat is Zero, or twice a Nat, or twice a Nat + 1). Your functions and proofs that you wrote with the previous implementation still will work and your type signatures won't have to change