[HN Gopher] Programming with Categories
___________________________________________________________________
Programming with Categories
Author : kercker
Score : 220 points
Date : 2020-09-02 15:08 UTC (7 hours ago)
(HTM) web link (brendanfong.com)
(TXT) w3m dump (brendanfong.com)
| mortdeus wrote:
| the second i saw haskell i started saying eternally, "ABORT
| ABORT!"
|
| You are going to have to revive jesus to come up with a
| functional language that simplifies coding over a procedural one.
| Especially over an object oriented one.
| gumby wrote:
| For those who might not realize: IAP is the period between
| semesters at MIT, roughly most of January. So this is is a quick,
| accessible introduction, not a heavy semester-long slog.
| mncharity wrote:
| When taught in January at MIT, a highlight was something I'd not
| seen elsewhere: someone called it the "aftermath" (3-pun). After
| the one-hour traditional-ish lecture (on video), the room was
| reserved for an additional hour.
|
| When previously taught, people would remain afterwards to ask
| questions, discuss math, and chat. So this was an iterative-
| improvement formalization of that.
|
| People would gather in front of the blackboards in fluid
| discussion clusters. Catalyzed by the three instructors and wizzy
| others, not all having to stay for the entire hour, but drifting
| off as discussion died away. They could show material they had
| pruned from the lecture, for want of time. Or got dropped as they
| ran over. Alternate presentation approaches they had considered,
| before selecting another. They could be much more interactive.
| One commented roughly "If I was tutoring someone, I'd never
| present the material this way". It was a delightful mix of
| catching the speaker after a talk to ask questions, a professor's
| office hours, a math major's lounge, an after-talk social,
| tutoring, an active-learning inverted classroom, hanging out with
| neighbors in front of the hallway blackboard, chalk clattering
| and cellphones clicking to snag key insights... It was very very
| nifty.
|
| So, the book is nice. And lecture notes. And videos. But... the
| best part isn't there. Perhaps the next iterative improvement is
| to capture the aftermath on video, and share that too.
|
| And as we look ahead, planning distance-learning and XR tools...
| maybe something like this is a vision to aspire too. The insane
| ratio of expertise to people learning is not something one can
| plausibly replicate in meatspace. But as conversations in front a
| virtual blackboard gradually become technically feasible,
| something like this might pay for the cost of it, with
| transformative impact.
| mortdeus wrote:
| wait, you are saying that at MIT you had to sit for a video?
|
| Why are you paying for that nonsense?
| mortdeus wrote:
| " not all having to stay for the entire hour,"
|
| No F that. If everybody (or their benefactor) is paying
| literally paying $666 (no joke thats what 40,000/60 equates
| to) everytime they show up to class, then everybody and their
| mother who decides to open their mouth can stay for the full
| 60 mintutes to hear the same stupid questions asked and
| answered over and over again.
|
| Thats the minimalistic price of having socialism/marxism show
| up on my favorite programming language golang.org thank you
| very much.
| iso8859-1 wrote:
| Videos of the lectures from last year:
| https://www.youtube.com/watch?v=NUBEB9QlNCM
| nwallin wrote:
| Here's the full playlist:
| https://www.youtube.com/playlist?list=PLhgq-BqyZ7i7MTGhUROZy...
| mcalus3 wrote:
| "We will assume no background knowledge on behalf of the student,
| starting from scratch on both the programming and mathematics."
|
| This is a fantastic "side effect" of the fact that category
| theory isn't built on any other mathematical knowledge. You don't
| even need even any arithmetics for that.
| picklenerd wrote:
| This is almost every upper division undergrad math class. It
| was always fun watching people squirm when they pulled out some
| useful fact from their past 14 years of math education and then
| got told they had to prove it before they could use it.
| Someone wrote:
| If only it were limited to facts learned from math education.
| For example, there's the Jordan curve theorem
| (https://en.wikipedia.org/wiki/Jordan_curve_theorem), which I
| guess most four-year olds 'know to be true' from their
| experience with coloring books.
| Tainnor wrote:
| Yeah, but from that same Wikipedia article:
|
| > It is easy to establish this result for polygons, but the
| problem came in generalizing it to all kinds of badly
| behaved curves, which include nowhere differentiable
| curves, such as the Koch snowflake and other fractal
| curves, or even a Jordan curve of positive area constructed
| by Osgood (1903).
|
| So to some extent, the reason why such an "obvious"
| statement requires a complicated proof is because our
| everyday notions of what a "closed curve" is are much more
| restricted than what we consider in mathematics. This is
| kind of common in maths, especially in fields with a lot of
| visual intuition.
| qppo wrote:
| to get super meta, one could say that the opposite is true:
| arithmetic requires categories
| dan-robertson wrote:
| Except this isn't really true in the common sense meaning
| (schoolchildren do arithmetic fine without knowing about
| category theory) or in the formal sense you're trying to get
| at (there are formal axiomatic foundations which arithmetic
| can be based on which do not need category theory. A simple
| proof is by causality: arithmetic was successfully formalised
| before category theory was invented)
| spirographer wrote:
| At a meta level, Category Theory requires some comfort with
| abstraction, which really only comes with a mathematical
| education. So while it may stand apart from much math, it
| relies on your strong mathematical foundations.
| dkarl wrote:
| As so many undergraduate math textbooks say, "No background
| is assumed beyond sufficient mathematical maturity."
| pizza wrote:
| Which is kind of ironic, because students take classes
| exactly because they feel 'immature' with respect to that
| subject.. Honestly, most of my smoothest educational
| experiences with hard topics assumed some immaturity on my
| part, and that that was OK
| dan-robertson wrote:
| People don't generally take category theory because they
| don't really understand how proofs work or how to read
| definitions. The maturity required is about being able to
| cope with proving things and following proofs based on
| definitions which will probably seem somewhat bizarre at
| first and unmotivated at first. The immaturity you seem
| to talk about is people taking category theory because
| they don't know category theory but that's different and
| not what is meant by mathematical maturity.
|
| That said, a background in mathematics helps with
| category theory. Things like group theory, topology
| (particularly algebraic topology), Galois theory and set
| theory can be useful in motivating a lot of category
| theory. I'm yet to see much of a strong motivation from
| programming (where is there a functor that isn't an
| endofunctor?)
| inopinatus wrote:
| Tautological sufficiency/necessity relativities for an
| absolute measure are a pet peeve:
|
| "How much salt should I add?"
|
| "Oh, not too much."
|
| Practically guarantees a withering glare from me.
| mcguire wrote:
| "Sufficient mathematical maturity":
| https://c8.alamy.com/comp/HY1PD9/elderly-math-teacher-
| HY1PD9...
| [deleted]
| gnufx wrote:
| I think I got more appreciation of abstraction from physics
| and programming than what mathematical education I had; I'm
| weak at maths -- experimental physics doesn't need much :-/
| -- but I do understand that weakness, and am quite
| comfortable with abstraction.
| LockAndLol wrote:
| This doesn't work at all with HTTPS Everywhere. Just get a page
| about DreamHost site not found.
| hawkice wrote:
| In my experience, Monad, Applicable, and Monoid are probably the
| only ones I'd use in Haskell, and maybe none of them in languages
| without good inference and general support.
|
| Pretty wild ideas, though. Fair chance they'd be more confusing
| than using more specifically named instances, but solid ideas
| where the class instance documents that you're using the pattern,
| instead of describing the preferred interface.
| smabie wrote:
| You've definitely used Functors or Semigroups as well, you just
| didn't realize it.
| madhadron wrote:
| I wish semilattices got more play. They're so ubiquitous when
| talking about distributed systems. I remember a keynote on
| eventual consistency in databases that could have been replaced
| with "make your merge operation the join of a semilattice."
| infogulch wrote:
| Any resources for semilattices that you do like? I'm also
| finding them mentioned around CRDT & distributed systems
| threads.
| dan-robertson wrote:
| I think it isn't often said that one reason a lot of these
| classes work in haskell is the lazy evaluation (or arguably the
| pure functions allowing the compiler to inline things and skip
| evaluation).
|
| You can write monoid and foldable interfaces in java but in
| haskell finding the head of a list with a monoid and foldmap is
| constant time (and the first or last element of a tree is
| logarithmic) but a java implementation would be linear.
| Ericson2314 wrote:
| There is sort of a "jump" from those to the ones less oriented
| around (->) but truer to the math, but I can assured I have in
| fact used https://hackage.haskell.org/package/categories (a
| prime example of the latter sort) in production and it was
| genuinely useful.
| random3 wrote:
| Wow, what a combo! I'd be interested in anything from each of the
| lecturers, but all 3 at the same course, is amazing.
|
| Category Theory could be the rosetta stone of many things(this is
| relevant https://arxiv.org/pdf/0903.0340.pdf).
| linkdd wrote:
| I've read a lot about Category Theory, and I'm amazed at the
| abstraction level that lets you compose with different
| mathematical domains (geometry, topology, arithmetic, sets, ...).
|
| And yet, the current mathematics relies heavily on the ZFC set
| theory. Why is that ? (Is that assumption even correct ?)
|
| From what I've learned so far, the set theory suffers from
| Russel's Paradox[0] (does the set of all sets that does not
| contain itself, contains itself ?). That's what motivated the
| formalization of Type Theory and the invention of Type Systems in
| programming languages.
|
| According to wikipedia[1], __some __type theories can serve as an
| alternative to set theory __as a foundation of mathematics __.
|
| It seems to me that the Category Theory fits the description. So
| why don't we see a huge "adoption" in math fields ?
|
| Thank you in advance for your clarifications :)
|
| [0] - https://en.wikipedia.org/wiki/Russell%27s_paradox [1] -
| https://en.wikipedia.org/wiki/Type_theory
| tombert wrote:
| ZFC Set Theory avoids Russell's paradox by having a few
| fundamental axioms that preclude it. It's actually mentioned in
| your wiki link in the `Set-theoretic responses` section.
|
| ZFC is a bit messy sometimes, but it's actually kind of nice in
| its simplicity. I am a big fan of TLA+, for example, and it's
| really kind of beautiful how easily you can define incredibly
| precise invariants by using the set theory predicate logic.
| mindcrime wrote:
| IANAM, but...
|
| 1. I thought mathematics _was_ moving more towards a category
| theory based foundation, as opposed to the set theoretical
| stuff.
|
| 2. Isn't it in part because we have over 120 years of results
| and proofs that are based on set theory, and people aren't just
| going to throw that out for something newer? Granted, Category
| Theory has been around in some form since about the 1940's, but
| it's still newer than set theory.
|
| 3. Russell's Paradox hasn't stopped people from using Set
| Theory to achieve useful results, and the axiomatization of Set
| Theory and the advent of ZFC is why (or at least part of why)
| that was possible, no?
| spekcular wrote:
| 1. It's not. The work on "category-theoretic foundations,"
| say HoTT, is (sociologically speaking) a highly niche topic.
| Most professional mathematicians who work on the foundations
| of mathematics do so in the framework of set theory.
|
| 2. ZFC is fully adequate for all the mathematics 99% of
| professional mathematicians do (and probably more than
| adequate in terms of strength.) Also, all the mathematics 99%
| of mathematicians do is insensitive to foundational issues,
| so if you swapped ZFC for another axiomatization of similar
| strength, no one would notice.
|
| 3. I don't believe ZFC was the first to avoid the paradox,
| but yes, it does not suffer from Russell's Paradox.
| johncolanduoni wrote:
| ZFC does not suffer from Russel's paradox, since it doesn't
| allow a "set of all sets". If it did, the search for new
| foundations would be much more widespread. New foundations are
| usually only considered seriously once they can be shown to be
| relatively consistent with ZFC or the slightly stronger but
| still uncontreversial TG set theory.
|
| There are people working on categorical foundations, but the
| main reason for lack of broader popularity or drive is that
| most mathematicians don't do work that is "foundational" in
| that sense. For example, if you're an analyst, you generally
| don't care exactly how your real numbers are built (dedekind
| cuts, Cauchy sequences, etc.). You only care that they satisfy
| a certain set of properties, you can define functions between
| them, and that's about it. Most mathematical reasoning at this
| level is insensitive to differences in proposed foundations,
| except "constructive" foundations that don't have the law of
| excluded middle (that are unpopular since they make many proofs
| harder and some impossible).
|
| What is very popular in mathematics is using category theory at
| a high level; basically every field uses its concepts and
| notation to some degree at this point. New foundations are only
| really relevant to this program in that they may make automated
| proof checking easier, which is also not a widespread practice
| in mathematics.
| spekcular wrote:
| It is not true that "basically every field uses its concepts
| and notation to some degree at this point." In particular
| this is false for mainstream combinatorics, PDE, and
| probability theory, to give a few examples.
|
| In fact, I would suggest that most mathematicians don't care
| about category theory at all.
| bitdizzy wrote:
| This all hinges on "mainstream". For example, in
| combinatorics, combinatorial species are a vast
| organization of the all-important concept of _generating
| function_. They were developed by category theorists and
| are most tidily organized along categorical lines. If you
| don 't think this is close enough to mainstream, I can't
| dispute that. It's a value judgment.
|
| There is often an undercurrent of category theory within a
| subject that maybe most people are not privy to. Anything
| to do with sheaves or cohomology (which I know factors into
| some approaches to PDEs) are using categorical ideas.
|
| Every generation, it seems, has some contingent of serious
| mathematicians who consider category theory marginal in
| their field of interest. But every generation, that
| contingent grows smaller as more mathematics as practiced
| is brought into the fold. Maybe they're coming for you next
| :)
| spekcular wrote:
| Respectfully, I disagree. The question of what's
| mainstream and valued by the community is empirical and
| can be answered by looking at what's published in the
| leading combinatorics journals. And anyone can check
| those out and see that categories are basically absent.
| So as a sociological fact, I maintain it's far from the
| mainstream.
|
| Whether combinatorialists _ought_ to elevate certain work
| is of course of a question of value, but it 's also a
| different question.
|
| Also, in no way are sheaves or (co)homology essentially
| category-theoretic ideas. It's possible to develop and
| use these ideas without mentioning categories at all (and
| e.g. Hatcher's introductory textbook does just this,
| although he mentions in an appendix the categorical
| perspective later). In general I think it's good to
| remember that homological algebra and category theory are
| not the same subject. Sure, I can develop a theory of
| chain complexes over an arbitrary abelian category, but
| most of the time you just need Hom and Tor over a ring.
| (Again, see Hatcher.)
|
| Finally, I'm not sure there has been a serious uptake in
| category theory in the mainstream of some field of
| mathematics since, I don't know, at least 50 years ago?
| We've understood for a while now what it's good and not
| good for. This hasn't stopped people from trying to
| inject it in fields where it doesn't do any good (e.g.
| probability), but for that reason those attempts are
| mostly ignored.
| Koshkin wrote:
| > _most mathematicians_
|
| Agree, but only on the level on which they do not care
| about the abstract math (algebra, topology, etc.) in
| general. As soon as you step into the territory of the
| abstract math, especially where different disciplines
| blend, such as homology and cohomology, category theory
| (and its diagram language) helps a lot to clarify things.
| (Incidentally, a lot of this stuff is now part of the
| "applied math" as well, having found its way into
| theoretical physics, for example.)
| spekcular wrote:
| I'm not sure I'm comfortable characterizing the fields
| where category theory is useful as "abstract math."
| Modern PDE is plenty abstract, for example. Probably it's
| better to say that the usefulness of category theory is
| proportional to the problem's distance from algebraic
| topology and algebraic geometry.
|
| I also am reluctant to characterize theoretical physics
| as "applied math." I haven't seen anyone who calls
| themselves an applied mathematician use category theory
| in a substantive way (where here I am thinking about
| numerical computing, mathematical biology, and so on).
| joe_the_user wrote:
| I have only an MA in math - but I have the impression
| mathematicians can be arranged on spectrum between ad-hoc
| theorem provers and giant machinery builders, between those
| like Paul Erdos and those Alexander Grothendieck.
|
| The thing to keep in mind is that a mathematical structure
| can be expressed as instance of any number of more general
| mathematical structures ("mathematical machinery"). The
| structures that useful, however, are those that are
| "illuminating", a somewhat vague criteria but one which
| generally include a structure facilitates and unifies proofs
| of important theorems. Wiles' proof of Fermat's Last Theorem
| showed the value of many forms of this mathematical machinery
| [1], including category theory.
|
| At the same time, I think things like Godel theory of cutting
| down proofs and Chaitin's Omega constant give a suggestion
| that the some number of "important" theories within a given
| axiomatic system will have long proofs that don't necessarily
| benefit from the application of a given piece of mathematical
| machinery, whatever that machinery.
|
| And think that's related to efforts to apply category theory
| to programming via functional programming. I feel like it's
| an effective method for certain kinds of problems but that
| you get a certain problematic "it's the best for everything"
| evangelism that doesn't ultimately do the approach favors.
|
| [1] https://en.wikipedia.org/wiki/Wiles%27s_proof_of_Fermat%2
| 7s_...
| fractionalhare wrote:
| _> And yet, the current mathematics relies heavily on the ZFC
| set theory. Why is that ? (Is that assumption even correct ?)_
|
| Set theory is the de facto modern standard because it has
| straightforward notation and sufficient power to prove the
| things most mathematicians care about, both algebraically and
| analytically. Other foundations exist, it's just that most
| mathematicians work at a level where set theory is more of a
| communication and notation tool than a foundation for which the
| nuances matter.
|
| _> From what I 've learned so far, the set theory suffers from
| Russel's Paradox[0] (does the set of all sets that does not
| contain itself, contains itself ?)._
|
| No, naive set theory suffers from Russell's Paradox, but ZFC
| does not. ZFC was defined in order to avoid Russell's Paradox.
|
| _> That 's what motivated the formalization of Type Theory and
| the invention of Type Systems in programming languages._
|
| Russell's type theory, yes, which predates ZFC. But this has
| nothing to do with programming languages, which weren't a thing
| when this problem was being considered.
|
| As for why category theory isn't used as a foundation - that's
| not really what category theory's "charter" is about. As user
| johncolanduoni explained, category theory is more of a
| framework for describing things with convenient algebraic
| abstractions than it is a foundation for mathematics. Category
| theory as practiced today is mostly done at a higher level than
| the foundational set theory.
| aruss wrote:
| Category theory isn't a type theory (in the sense that you can
| have the category of categories, which correspond to different
| type theories).
|
| It's true that you can get away from Russell's paradox in
| category theory, but that's because categories are not sets and
| have different properties (there's less you can say about them
| because they're more general).
|
| Type theories, particularly homotopy type theory, are becoming
| popular among some mathematicians, but not because they escape
| Russell's paradox (I'm not sure that they can say anything more
| about sets than set theory), but because they are more useful
| when constructing automated proof systems.
|
| Edit: also, category theory is used a lot in very cutting edge
| math, like algebraic topology.
| mcphage wrote:
| > So why don't we see a huge "adoption" in math fields ?
|
| Because most math fields work at a higher level, and whether
| they consider set theory or category theory foundational
| doesn't matter. For instance, the defining property of ordered
| pairs is: `(a, b) = (c, d) iff a = c and b = d`. {a, {a,b}} is
| a (set-theoretic) model for ordered pairs, but it's not the
| only model. As long as a model exists, the question of "which
| model you're using" isn't relevant.
| Twisol wrote:
| > From what I've learned so far, the set theory suffers from
| Russel's Paradox
|
| So-called "naive set theory" does, but my understanding is that
| this paradox (and others like it) sparked a crisis in
| mathematics that led to the creation of ZFC and others. ZFC is
| not known to be inconsistent (due to deep and technical
| reasons, I can't claim positively that it _is_ consistent), and
| it was designed to avoid the paradoxes that plagued naive set
| theory.
|
| Russell's type theory was another early contender for a
| formalism. For whatever reason (I'm not aware of all the
| details), Zermelo-Fraenkel set theory (later extended with the
| Axiom of Choice) won the popular mindshare. Personally, I'm
| more a fan of the Elementary Theory of the Category of Sets
| (ETCS) [1], which is indeed drawn from category theory. But
| it's equivalent in deductive power to ZFC, so what you pick
| mostly only matters if you're doing reverse mathematics. (This
| is what really answers your question, I think.)
|
| Russell's type theory and modern type theories are distinct
| (and there is no single "type theory"). I'm led to believe the
| commonality is primarily with the usage of a hierarchy of
| universes, so that entities in one unverse can only refer to
| entities in a lower universe.
|
| [1] "Rethinking set theory", Tom Leinster:
| https://arxiv.org/abs/1212.6543
| mindcrime wrote:
| _but my understanding is that this paradox (and others like
| it) sparked a crisis in mathematics that led to the creation
| of ZFC and others. ZFC is not known to be inconsistent (due
| to deep and technical reasons, I can 't claim positively that
| it is consistent), and it was designed to avoid the paradoxes
| that plagued naive set theory._
|
| That was my understanding as well. Axiomatic Set Theory, with
| ZFC, doesn't suffer from the same problems as Naive Set
| Theory, which is why it was developed. Or so I've read.
| random3 wrote:
| I think the current fundamental structures are influenced by
| the Bourbaki group, however it has gaps. Category Theory is
| likely able to fill those gaps and I guess it will end up as
| the foundational layer of both mathematics, computer science,
| and pretty much everything else. David Aubin wrote about this
| in
| https://press.princeton.edu/books/hardcover/9780691118802/th...
| (VI.96) Some discussions too here https://math.stackexchange.co
| m/questions/25761/introduction-....
| apkallum wrote:
| David Spivak and other folks at Azimuth Forum[0] have been great
| at providing high quality discussions on ideas in this course and
| others. Many thanks.
|
| [0] https://forum.azimuthproject.org
| spinningslate wrote:
| Good point and strongly agree. John Baez [0] also merits
| mention as the originator of Azimuth and the creator of the
| Applied Category Theory course [1] on the back of Fong &
| Spivak's paper [2].
|
| [0]https://www.azimuthproject.org/azimuth/show/John+Baez
| [1]https://forum.azimuthproject.org/discussion/1717/welcome-
| to-...
| [2]http://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf
| read_if_gay_ wrote:
| Is this Spivak related to the author of the famous Calculus
| book?
| dan-robertson wrote:
| David and Michael Spivak are not related
| razster wrote:
| What an odd coincidence that this was posted and on my YT
| subscribe page: https://www.youtube.com/watch?v=NUBEB9QlNCM -
| Just posting the video for others to see.
| max68 wrote:
| These guys wrote "An Invitation to Applied Category Theory." It's
| an awesome book, and I'm super excited for these lectures.
| Myrmornis wrote:
| Will the course be taught live again and if so will those
| geographically elsewhere be able to attend?
| yearoflinux wrote:
| As someone who respects functional programming (because it
| removes geniuses from competing in my space) here's a nice video
| https://www.youtube.com/watch?v=ADqLBc1vFwI
|
| What is the beautiful monospace font in the pdf here
| http://brendanfong.com/programmingcats_files/cats4progs-DRAF...?
| CobrastanJorji wrote:
| > The number of elements of a set X is called its cardinality
| because cardinals were the first birds to recognize the
| importance of this concept.
|
| Alright, maybe I will keep reading this book.
| enriquto wrote:
| > What is the beautiful monospace font in the pdf
|
| t1xtt, from the txfonts package, freely available
| yearoflinux wrote:
| Thank you! No ttf/otf though :)
| infogulch wrote:
| Hitler: What's a monad anyway? No one who understands monads
| can explain what they are Underling (hurriedly): A
| monad is just a monoid in the category of endofunctors
|
| This caused me to choke on my coffee.
| sloucher wrote:
| You just made those words up right now!
| madhadron wrote:
| The last line. Oh god, the last line. I haven't cackled that
| loudly in months.
| mortdeus wrote:
| you are my hero for this comment.
| [deleted]
| marcosdumay wrote:
| Oh, another Haskell can't do IO joke.
| mumblemumble wrote:
| Yes, but this time it was a funny one. I laughed, and not
| just at AbstractSingletonProxyFactoryBean.
|
| Gotta be able to laugh at yourself sometimes.
| marcosdumay wrote:
| Thanks for replying. I gave up on the beginning because
| those jokes tend to always be the same.
|
| (And to be fair, half of them are the same overused ones.
| But the others are good.)
| tsimionescu wrote:
| "Thank god you haven't found Prolog..."
| mumblemumble wrote:
| It's true, and it starts off with the very worst one. I
| almost closed the tab like 30 seconds into the video.
| dllthomas wrote:
| But the important takeaway is that if you don't like
| Haskell, you might as well be Hitler.
| roflc0ptic wrote:
| I think the joke was that Haskell can do IO but haskellers
| can't
| mindcrime wrote:
| > here's a nice video
| https://www.youtube.com/watch?v=ADqLBc1vFwI
|
| OMG. That might just be the funniest god-damned thing I've ever
| seen in my life. Thanks for sharing that!
|
| On a separate note: does anyone know where this footage is
| originally from? Some WWII movie, I would guess?
| Tainnor wrote:
| https://en.wikipedia.org/wiki/Downfall_(2004_film)
|
| Probably one of the best "WWII movies" (it's really only
| about the final days in the bunker) ever.
| mindcrime wrote:
| Thanks. I will check that out.
| cgh wrote:
| > here's a nice video
| https://www.youtube.com/watch?v=ADqLBc1vFwI
|
| This made me laugh way more than it should have. "Why don't you
| pattern match my fist all over your faces!"
| mcguire wrote:
| "Don't worry, Haskell transpiles to Java now."
|
| And the last line....
| sideeffffect wrote:
| If you're interested in how Category theory and Algebra can
| inform the design of software, have a look at ZIO Prelude.
|
| https://github.com/zio/zio-prelude
|
| It's a brand new library for Scala that contains reusable
| mathematical structures. Still based on algebra and category
| theory, but it expresses them more or less differently than how
| they've been expressed in Haskell (and similar languages). For
| example, unlike Haskell (and Scala's own cats and ScalaZ), it
| doesn't present the "traditional" Functor -> Applicative -> Monad
| hierarchy. Instead, it presents the mathematical concepts in a
| more orthogonal and composable way.
|
| One example out of many, you don't have a Monad. You have two
| distinct structures:
|
| * Covariant functor, with typical map operation `map[A, B](f: A
| => B): F[A] => F[B]`
|
| * IdentityFlatten which has a flatten operation `flatten[A](ffa:
| F[F[A]]): F[A]` and an identity element `any: F[Any]`
|
| When combined together (Scala has intersection types), you get
| something equivalent to the traditional Monad.
|
| The project is in its infancy, so it may still change
| significantly, though. Look here for more detailed explanation:
|
| https://www.slideshare.net/jdegoes/refactoring-functional-ty...
|
| https://www.youtube.com/watch?v=OwmHgL9F_9Q
___________________________________________________________________
(page generated 2020-09-02 23:00 UTC)