Edward Kmett

Well, there's not much to the basic idea--the λ-calculus just is the structure of a cartesian closed category. Exponential objects represent morphisms by objects, a.k.a. first-class and higher-order functions, the equivalence Hom(X * Y -> Z) ~ Hom(X -> Z^Y) is currying, a morphism ((Y^X) * X) -> Y is function application, and so on.

A basic cartesian closed category alone only gets you the simply-typed λ-calculus, though, which isn't much fun. The untyped λ-calculus is of course incoherent from the C-H perspective, since unrestricted recursion[0] gives you Turing-equivalence, which corresponds to an inconsistent logic; a categorical description would probably be easy but I don't think I've seen one.

More expressive typed λ-calculi such as System F are more interesting from a computer science perspective, but I've not been able to find much material discussing them from a logical or categorical perspective. Instead, most mathematicians would jump straight to something like Coquand's Calculus of Constructions[1], which is (if memory serves me) the internal logic of a topos.

Category theory also sees some use in computer science beyond just C-H stuff--for instance, describing recursive data types as fixed points of endofunctors on the category of types. This permits an elegant categorical description of operations on those types--e.g., the "fold" or "reduce" function on lists is represented by an initial F-algebra. The categorical habit of dualizing everything in reach also…

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_tate_popl10.pdf)

- 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-trinity/ For way more, see https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory#Overview 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…

The extent of my experience on the topic is in half-comprehending hobbyist's awe and the inclusion of okmij on my "personal heroes and demigods" list. The only word I could half-heartedly associate with this structure is the incredibly lame "hylomorphism"... which actually kinda generally expresses the pattern of much of computing. It's 5 AM and I'm going to sleep, but I'll leave you with the the most plausible leaves of a very brief search towards finding some recognized formal name for this structure:

http://blog.sigfpe.com/2009/07/monad-for-combinatorial-search-with.html
http://spivey.oriel.ox.ac.uk/mike/search-jfp.pdf
http://www.cs.au.dk/~gerth/papers/jfp96.pdf

If you really don't like yourself, try digging here:

http://hackage.haskell.org/packages/archive/pointless-haskell/0.0.1/doc/html/Generics-Pointless-RecursionPatterns.html
http://comonad.com/reader/2009/recursion-schemes/

Back when people-facing computer stuff worked more like computer-facing computer stuff, queries were simple: keywords to match. If you get too many results, add more keywords; if you get too few, remove* keywords (or change existing keywords to be more specific/more general respectively).

If you're not searching for literal occurrences of "what" and "is", why should they even be in a query?

* this is an instance of an adjunction, which is an important concept in informatics, but I understand that to actually admit the fact would probably be the kiss of death for anything claiming to be a "user" interface.

Lagniappe: marginalia, upon being queried with "precision" and "recall", came up inter alia with http://comonad.com/reader/2009/remodeling-precision/ , which I count as a win for it.

Perhaps the best way to think of it is that a Haskell program is a pure function from FFI outputs to FFI inputs. Something like

H out in = out -> (FFIOperation, in)

The `IO` monad is nothing more than how operating "inside of this function" feels. The runtime thus operates the pure Haskell program evaluating its FFI demands and returning their results.

The AST POV espoused by this article is quite good as well, but a little bit less obvious how to "step" things forward or operate nicely in parallel contexts.

Also, in reality the above perspective is a good way to embed Haskell into other contexts.

http://comonad.com/reader/2011/free-monads-for-less-3/

The talk he's defending was tiresome and dripping with condescension (I agree with Stephen Diehl: https://twitter.com/smdiehl/status/519160854517149696). Typed-language folks don't need advocates who waste breath talking about "incompetent Ruby developers moving to Clojure" and whatnot. There's enough positive stuff to talk about! I think the folks who gave that talk need to read Gershom Bazerman's (a person who has no trouble giving talks filled with excitement about type- and category-theoretic concepts with no condescension) excellent post here: http://comonad.com/reader/2014/letter-to-a-young-haskell-enthusiast/