chas

This is likely what he is referring to: http://math.andrej.com/2007/09/28/seemingly-impossible-funct...

In particular, you can search compact infinite spaces by only considering a finite number of steps: "What is going on here is that computable functionals are continuous, which amounts to saying that finite amounts of the output depend only on finite amounts of the input. But the Cantor space is compact, and in analysis and topology there is a theorem that says that continuous functions defined on a compact space are uniformly continuous. In this context, this amounts to the existence of a single `n` such that for all inputs it is enough to look at depth `n` to get the answer (which in this case is always finite, because it is an integer). I’ll explain all this in another post. Here I will illustrate this by running the program in some examples."

This is the follow-up post mentioned in the quote: http://math.andrej.com/2008/11/21/a-haskell-monad-for-infini...

While sleeping well, exercising regularly, and eating good food will massively improve your mental health, chemical help can be extremely useful for establishing those habits when just trying harder hasn’t worked.

I usually see it when people are comparing two tools and can't come to an agreement. In that context, I feel it ends up being tautological in a way that stops people from digging into the real differences that make something the right or wrong tool.

"Use the right tool for the job"

In addition to CT's application to commutative algebra, it's pretty nice for reasoning about programs and logic.

Programs: http://cseweb.ucsd.edu/~rtate/publications/proofgen/proofgen..., https://blog.sumtypeofway.com/posts/introduction-to-recursio..., the Functor/Applicative/Monad hierarchy in Haskell et al

Logic: https://publish.uwo.ca/~jbell/catlogprime.pdf

CT as a bridge between programs and logic: https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...

I am very fond of using graphviz (https://graphviz.org/) to draw the finite state machines that my programs interact with. For example, this is a description of the state machine inside the Linux kernel audio subsystem, as it was several years ago: https://source.chromium.org/chromium/chromium/src/+/master:c... You can draw it using ‘xdot’ for something interactive or with ‘dot’ for a static png or svg file.

A handwired QMK keyboard would work fine: https://docs.qmk.fm/#/hand_wire

If you have only one or two switches, you can use the DIRECT_PINS configuration to directly put one switch per input pin rather than the more conventional switch matrix approach. You can use the XD002 code as a starting point (https://github.com/qmk/qmk_firmware/tree/master/keyboards/xd..., https://github.com/qmk/qmk_firmware/blob/master/keyboards/xd...). It uses a DigiSpark rather than the more common Arduino Pro Micro. The DigiSpark is a bit fiddly and has very little program memory, but it is very cheap and simple.

I'm happy to hear that you found the first paper interesting!

While I agree that it is unlikely C and Python programmers will take up categorical abstractions any time soon, there is some interest from the JavaScript world. As an example of how this manifests this is a concurrency library (https://www.npmjs.com/package/fluture) and parser combinator library (https://www.npmjs.com/package/parsimmon) that are explicitly using built functors, applicatives and monads as programmatic abstractions. I don't think that this is going to be the mainstream of JavaScript in the near future, but it does suggest that some folks in the JavaScript world think that categorical abstractions are relevant to their practical work.

I also think it is the case that it is a bit strong to claim that Haskell was designed as a programming language for categorical abstractions because none of the ones that I mentioned were included in the initial design of the language. The Haskell 1.0 report[0] was published in 1990 and while it had typeclasses[1], the Functor and Monad typeclasses weren't added until the introduction of monadic IO for Haskell 1.3 in 1996[0]. Moggi's first paper on monads for computation[2] was in 1988, but to my knowledge no one involved in Haskell was introduced to it until several years later[4]. While applicative functors are in the middle of the popular hierarchy, they were the most recently introduced to functional programming. It took until 2008 for them to be explicitly identified as an interesting abstraction in "Applicative programming with effects"[3]. Making a language where programs compose nicely was an explicit design goal, so I don't think that it is a surprise that that's where category theory first landed as an explicit tool for programming abstractions. The categorical abstractions replaced non-categorical abstractions because they did a better job of solving the real problems that the people programming in these languages had, so I think it is a meaningful application of category theory to computing even if it hasn't happened yet in the mainstream of computer programming.

I agree with your assessment of HoTT as well. I'm not currently working on HoTT or on the use of homotopy and (co)homology as programming abstractions, so if they make some contributions to that on the way to their actual goals, I will be super happy.

[0] https://wiki.haskell.org/Language_and_library_specification [1] https://imgur.com/a/OS6yaSr [2] https://www.irif.fr/~mellies/mpri/mpri-ens/articles/moggi-co... [3] http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf [4] https://www.microsoft.com/en-us/research/wp-content/uploads/...

Programmer warning: this is the math jargon heavy version, you don't need to know the math jargon to make use of these tools for writing day-to-day programs.

There are too many applications for me to do justice in one message and it is a bit messy because all of these are related, but there are roughly three ways that category theory gets applied to computing:

- Reasoning about data within computer programs. In "Generating Compiler Optimizations from Proofs" they make a category where the objects are a representation of expressions in programming languages and the morphisms are expression substitutions. They use this to build general proofs of correctness of compiler optimizations (http://cseweb.ucsd.edu/~rtate/publications/proofgen/proofgen...)

- Looking at logics (and thus programming languages) as algebraic objects. Objects are propositions, morphisms are proofs that prove one proposition given assumed propositions. Similarly objects are types, morphisms are functions. That in some contexts these are the same thing is the famous (in programming language circles) Curry-Howard-Lambek correspondence. https://existentialtype.wordpress.com/2011/03/27/the-holy-tr... For way more, see https://ncatlab.org/nlab/show/relation+between+type+theory+a... A different version of this is specifying the mathematical meaning of program execution in terms of directed-complete partial orders which are fruitful to think of categorically. I think Category Theory for Computing Science is the most approachable starting place for that perspective (https://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf)

- As core abstractions for programming. While you can reason about programs and programming languages with categorical tools, you can also use algebraic abstractions within programs. Functors, strong lax monoidal functors (called Applicative Functors in this context), and monads feature prominently in Haskell's standard library. Basic overview is here (https://wiki.haskell.org/Typeclassopedia). The default ones that Haskell uses are all defined as endofunctors on Hask (category of Haskell types and functions between them), so they look a bit funky to a mathematician, but there are other libraries with more mathematically-legible categorical tools as well. (Elsewhere in the thread, Iceland_jack linked to a discussion of one of his proposals: https://www.reddit.com/r/haskell/comments/eoo16m/base_catego...) It is also useful to describe data structures as initial F-algebras in order to abstract over the fold/reduce operation (https://blog.sumtypeofway.com/posts/introduction-to-recursio...). There is a ton more on The Comonad.Reader (http://comonad.com/reader/). For an extremely practical application of non-trivial categorical abstractions see: https://kowainik.github.io/posts/2018-09-25-co-log While I am heavy on the Haskell here because that's what I know best, people also use these abstractions in Ocaml, Scala, and other languages with enough functional and type-level infrastructure for them to be ergonomic to explicitly identify and abstract over.

Joseph Goguen also did a ton work applying category theory to computation that spans several of the above application types. A Categorical Manifesto is probably a good place to start and he cites a ton of papers in it that are good next steps. (https://cs.fit.edu/~wds/classes/cdc/Readings/CategoricalMani...)

I think it's fairly misleading to think of impure computation as a core part of the `Monad` abstraction in Haskell[0]. Most of the places I use monads in Haskell are pure e.g. error handling, parsers, working with DSLs. `IO` is where the impurity lives and the monad abstraction just makes it a bit more fun to use, but it isn't essential to the impurity. Haskell had IO before it had monads. I also feel like the emphasis on the Monad abstraction really sells Functor and Applicative short as they are fantastic abstractions in their own right in addition to being important building blocks for the Monad abstraction.

[0] https://news.ycombinator.com/item?id=20112333

While I'm not an expert in any of this, I'm primarily interested in Homotopy Type Theory (HoTT) because so many tools originally developed for algebraic geometry and algebraic topology have been successfully applied to logic and programming languages (e.g. categories, functors, natural transformations, monads, comonads, topoi) but homology and homotopy--core tools in algebraic geometry and algebraic topology--haven't been investigated to nearly the same degree in logic and computing. So even if HoTT isn't particularly compelling from the standpoint of pure foundations, I'm still excited for the work they are doing exploring these core tools in geometry in the context of logic and programming languages.

The first thing that got me really enthusiastic in category theory was seeing the definition of the categorical product in terms of universal properties. It's a very simple, but very different way of defining objects that makes it easy to see the relationships between similar objects in different contexts. For example, multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming are all products in particular categories* and the universal property definition unifies them very nicely. There isn't really enough space here to spell it out in detail, but this[0] is a good explanation. There is also a very natural way to manipulate the definition (categorical duality) to get coproducts which unify things like logical disjunction (||), greatest common divisor, and disjoint union of sets. This extremely unified view is also nice because if you have an unfamiliar mathematical or computational object, but you know that it has a categorical product, you suddenly know a ton about what you can do with it as well as some interesting questions to ask and properties to go looking for.

This genre of abstraction is all over the place in category theory and it gets way more interesting, but seeing products defined like this and how incredibly unifying of an abstraction it is was the first place that I really saw what the categorical perspective brought to the table.

*Cartesian product within the category of sets and functions between them (amounting to multiplication of cardinals, if one just cares about the action on objects), least common multiple within the category of positive integers ordered by divisibility (a partial ordering being just a special kind of category), logical conjunction within the category of truth values (which can be thought of as sets with at most one element), and structs or record types in the category whose objects are the types of your favorite programming language and morphisms are the programs between them. (From Chinjut, last time I brought up categorical products on hn: https://news.ycombinator.com/item?id=8780786)

[0] https://rnhmjoj.github.io/category-theory-for-programmers/sr...

If you'd to see how this applies more directly to programming, work like this is a direct application of the same definitional strategy for abstraction: https://blog.sumtypeofway.com/posts/introduction-to-recursio...

It’s all over the place in embedded software. If your software needs to run for a year on a coin cell battery, you basically have to turn off large sections of your processor and peripherals except when they absolutely need to run.

The control systems for airplanes often have a significant number of mathematical proofs.

Even in languages where the concepts can be encoded, it can be hard to determine what aspects of a given library are the encoding and which parts are the fundamental ideas if you haven't seen the ideas used in well-suited language. For instance, I didn't really understand the use of functools.reduce[0] or itertools.starmap[1] in Python until I was familiar with zipWith[2] and foldl [3] in Haskell.

The ideas themselves are not particularly complicated, but I hadn't previously worked with abstractions where the default was to operate on whole data structures rather than on individual elements, so I didn't see how you would set up your program to make those functions useful. In addition, for abstract higher-order functions, type signatures help a lot for understanding how the function operates. I found `functools.reduce(function, iterable, initializer)` significantly more opaque than `foldl :: (b -> a -> b) -> b -> [a] -> b` because the type signature makes it clear what sort of functions are suitable for use as the first argument.

It's now easy for me to use the same abstractions in any language that provides it because I only have to learn the particular encoding of this very general idea. While I couldn't figure out why functools.reduce was useful or desirable, I couldn't figure out many parts of C++'s standard template library at all. But if you already know the core concepts and the general way that C++ uses iterators and the fact that functools.reduce, Data.Foldable.foldl, and std::accumulate[4] are all basically doing the same thing for the same reasons is a lot more readily apparent.

[0] https://docs.python.org/3/library/functools.html#functools.r...

[1] https://docs.python.org/3/library/itertools.html#itertools.s...

[2] https://hackage.haskell.org/package/base-4.14.0.0/docs/Data-...

[3] https://hackage.haskell.org/package/base-4.14.0.0/docs/Data-...

[4] https://en.cppreference.com/w/cpp/algorithm/accumulate

What’s the application of super high-quality earth cable?

I don't think this builds right now, but it's my favorite example of a project really leveraging the expressivity of Clash to do hardware design: https://github.com/cbiffle/cfm

It turns out that CS folks with distributed systems and functional programming experience can be super productive hardware designers because distributed systems have very similar design-level tradeoffs as ASIC design e.g. how many copies of this processing-element do we use?, what's the correct ratio between storage and compute?. They both have pretty rough verification and correctness related to not being able to instantaneously-sharing state, so things like clock-domain-crossing aren't that foreign to the distributed systems folks.

You don't have a notion of clock cycles, making timing, or fan-out load in distributed systems, so if you are going to try this you definitely need some extremely experienced digital logic designers and chip architects around to keep everyone on the rails, but in turn the CS folks are really good at producing useful abstractions that make architecture exploration easy while maintaining correctness.

TL;DR: I've found it easier to teach folks that know Haskell and distributed systems design about hardware constraints than to teach RTL designers about functional abstractions and been really productive with a mix of both groups.

Bluespec is still around and actually got open-sourced recently! [0] The Bluespec company is focused on using their tools to build RISC-V cores: https://bluespec.com/

[0]: https://github.com/B-Lang-org/bsc

“append”* is the name chosen for the binary operator in the Haskell standard library’s monoid abstraction and “concat” seems like the same genre, so I would expect people would be fine with the intuition for “concat” as well.

Given that this is a thread on functional jargon, it might be interesting to note list metaphors as being useful for thinking about monoid might derive from lists being free monoids (in many contexts). This means that all functions from a collection elements to a monoid can be thought of as functions from that collection into a list with the appropriate type of elements and then a fold (also called a reduction) over that list. This knowledge can be super useful for thinking about program structure e.g. conceptually mapreduce is a general tool for large-scale distributed computation over monoids.

*it’s actually called “mappend”[0], short for monoid append, but I think the point still stands (and there is, in fact, a function called “mconcat”[1] but folds of a list of monoidal values using “mappend” to combine them.)

[0] http://hackage.haskell.org/package/base-4.14.0.0/docs/Data-M...

[1] http://hackage.haskell.org/package/base-4.14.0.0/docs/Data-M...

I think Matt Might's intro is relatively beginner-friendly depending on your familiarity with Scheme: http://matt.might.net/articles/intro-static-analysis/

Principles of Program Analysis isn't the Cousot's text, but it does make significant use of abstract math. In particular, it uses tools from order theory[0] to describe many program analysis algorithms as finding fixpoints of functions between lattices[1].

This is useful because it reduces many program analysis design questions to questions of which lattice to use. It also allows you to compare algorithms by comparing their lattices, which makes it easier to see how algorithms are related.

The cost is that this approach will be pretty alien if you don't have experience with abstract algebra or related fields. If you do have that experience, I don't think it requires mathematical maturity beyond an undergraduate level.

[0] http://matt.might.net/articles/partial-orders/

[1] https://en.wikipedia.org/wiki/Lattice_(order)

This article gets more into actual analysis of program state and execution: http://matt.might.net/articles/intro-static-analysis/

If you want to go deeper, Principles of Program Analysis is a popular reference: Principles of Program Analysis https://www.amazon.com/dp/3540654100/

Under what circumstances to non-contiguous data structures run faster? I know of circumstances where structures with pointers make it easier to get better asymptotic behavior with a large amount of data, but none where a linked structure out-performs the analogous contiguous one on moderate amounts (a few cache lines) of data.

While this is true for many process nodes, it is not true in general. For instance, the transition to FinFETs greatly reduced leakage power in TSMC 16nm in comparison to their 28nm processes.

If “placebo-resistant depression” and “treatment-resistant depression” were synonyms, we would expect that excluding treatment-resistant depression from your study would result in the studying showing precisely no difference between treatment and placebo. The fact that the meta-analysis shows any difference at all suggests that “treatment-resistant depression” might be a meaningful category.

The “or” makes it a sum type.

This sort of homology[1] or this sort[2]? It looks like this is about the first one and proteins usually involve the second one. If they are more related than I expect, I would love to find out.

[1] https://en.wikipedia.org/wiki/Homology_(mathematics)

[2] https://en.wikipedia.org/wiki/Sequence_homology

This breakthrough is only a big deal from a practical perspective in that it very strongly suggests that further research on engineering large quantum computers will provide the exponential performance improvements predicted by quantum complexity theory. That is to say that this is a strong “go” signal in a go/no-go test.

In terms of where I am personally excited about quantum computing, it has the potential to greatly speed up simulations of chemical and material science properties that are currently hard to simulate accurately at all. This will be great for, for example, semiconductor development and medicine. These applications are a ways off though, but if we weren’t hitting milestones like today, it would suggest they were not worth vigorously pursuing.

Disclaimer: I work at Google, not on quantum computers. Not an expert in quantum computation.

In a Haskell context, that function’s type would be something like ‘(Num x, Num y) => a -> b -> (a, b)’ where ‘Num’[0] is the type class of types with defined numerical operators. If there is no fat arrow (=>), you can only perform operations which don’t depending on any aspects of the types in question.

There is, however, a gotcha along these lines: Haskell has a value called ‘undefined’ (along with some other issues collectively called “bottom” for CS theory reasons[1]) which can take any type. So ‘foo x y = (x, undefined)’ is a legal implementation of that function will will compile, but crash if you try to do anything with the ‘undefined’ result.

In practice, knowing your function has essentially one implementation because it’s sufficiently polymorphic (no concrete types), is still a great trick for getting the compiler to enforce certain kinds of correctness.

[0] https://www.haskell.org/tutorial/numbers.html

[1] https://andre.tips/wmh/brief-note-undefined/