Category theory & Programming language theory

interesting, thanks for the article.

How does Category Theory relate to the Lambda Calculus?
I saw something about the "Lambda cube" which seemed like a CT construct.
Also how does it relate to real-life languages, particularly LISP?
Thanks friends.
Oh also, how does Homotopy Type Theory relate to all of this? this one I don't know jack shit about.

This might be a little bit too formal, but maybe this helps
ncatlab.org/nlab/show/relation between type theory and category theory

Lisp is has very few core language construct and afaik not that much of an explicit typing.

I've made some notes on the Haskell type system from a category perspective here
axiomsofchoice.org/haskell_type_system
and here
ncatlab.org/nlab/show/Haskell

>user learns about Category Theory for the first time

>Huh, never heard of that before... let me read about it...

>Hmmm... fibered product, pointed sets, schemes, sheaves, topoi, ..., Hmmm.. those are interesting... names for terms... I know what they all mean outside of math... and some of those just seem like poetry and not math... funny... I hope they don't literally mean the same thi- ...Oh...okay. Well maybe I just don't understand what they really mean let me look up some other people using them to see if I just misinterpreted their mea- ... god dammit... Well, maybe I'm just reading the wrong interpretations, I'm sure there are experts in the field who can give better explanations than grad students on math overflow...

>100s of experts and historical contextualizations later...

>...

You're doing it wrong. Pick up conceptional mathematics. It explains category theory to an advance high schooler.

I don't get what you're talking about.

You know "topoi" outside of math? A sheave in math is a sheave on a farm?

I see this as an experiment.
Do you think a single person under 18 gained something something from starting their tour into somewhat higher, with this book, on their own?

I'm a first year maths undergrad, anyone can understand it.

Speaking of type theory and cats...
The nLab discusses the definition of the product and pair type [math] \prod [/math] and [math] \sum [/math] arising as adjoints to the pullback functor in all it's abstract generality.
The case for categories of sets and types ought to be much more straight forward. Does anybody know a reference to such a more concrete and simpler elaboration on those topics?

1. Yes, I know "topoi" outside of math because like anyone else who went through a private high school I had to take an ancient language class so the first time I saw the term I immediately recognized it as the plural form of topos. Unfortunately, not many people have to learn ancient greek and thus the origin of terms like "topoi" are lost, and the term must suffer a whirring mystical glow hanging around its necks at all times. i.e. "It's in Greek! We better take him seriously! We'll do anything you say! Please don't hurt us, all-powerful wielder of Gammas and Epsilons!"

2. The point of the story is that to an outsider, or at the very least, someone not an expert in all the various offshoots of Invariant Theory, Category Theory looks like a parody of mathematics, in that it looks like someone is looking at mathematics from the outside, and trying to describe it with these funny qualitative, concrete terms, rather than someone who is busy actually "doing" mathematics (cue: "but category theory IS doing mathematics!"). Many terms end up being different variations of "relation" which is always an abstract noun but, "noses", "sheaves", "hearts", "nerves", and "fibers" are all usually concrete nouns, and not ever used to talk about abstract relations explicitly, so it sounds funny. And other terms like, "pointed", "pushout", "pullback", "thin", "thick", "skeletal" are words/phrases you would also usually find in concrete, or qualitative contexts, not quantitative ones. So it's just funny because as we all know Category Theory gets a lot of heat for being "abstract nonsense", and yet you have all these terms which are usually concrete or only used in a concrete or qualitative settings.

3. To be fair, it's not just Category Theory- Set Theory at least in it's modern forms, also has some funny names for concepts- "meagre" and "immune" sets being the first that come to mind.

topos has a wide spectrum of meanings in Ancient Greek, nowadays it is used akin to theme or trope.

I like the naming convention from 1800 onwards better than the old (but sometimes still used) habbit of merging lating or greek words etc.
I.e. I think
"Polynomial" is gross, "Ring" is nice. Assuming you don't know greek and lating, of course.
The first is like in medicin, where you get words you have to remember. Like "Isomorphism". The word "Bundle" is much nicer.
But sure, now one might also argue that the latter brings false intuition.
The third convension would be to use peoples name, e.g. in "Hausdorff space", which is I guess a variant of the first one.
And yes, set theory is almost more autistic. With names like
en.wikipedia.org/wiki/Zero_sharp
And
en.wikipedia.org/wiki/Mouse_(set_theory)
is odd too

On another topic, which however also has to do with naming things, there is this cute nLab article

ncatlab.org/nlab/show/red herring principle

Naming conventions don't actually bother me too much in practice, because, obviously it's the objects you're thinking about, not their names... although if we stopped naming things after people or stopped describing spatial things as lists and listy things as spaces, I wouldn't lose any sleep.

>mouse (set theory)

Hah! How could I forget! DST is so dense.

Thanks for the nLab article.
>examples
>non-examples
>semi-non-examples

Very cute, pic related.

>Do you think a single person under 18 gained something something from starting their tour into somewhat higher, with this book, on their own?

Yes. If they do the exercises and read the book then they will learn category theory. But I would think at some point the exercises would get too hard on their own and would have to consult stackexchange or something to get help with proofs they don't fully understand.

Hello,
my DEAR friends!
I like to give you good link to the good site,
thriftbooks.com/share/?code=X0t%2bWcnCZPswOsuCcEHBmw%3d%3d
WHERE you could buy great chip books on
ALGEBRAIC GEOMETRY
and
CATEGORY THEORY.
The LINK gives you a small
discount. Good luck!!!

i'm taking a class about the semantics of programming languages. the topics are - among others - the operational, axiomatic and denotational models for determining or defining the meaning of a program or language. Most of the math behind it is set theory and things like fix points and partial orders.
does that have anything to do with what you mean?

From Type Theory and Formal Proof:

It's also programming language theory, so yes.