Andrej Bauer

Honestly, the entire part of the post before getting to categories is what I think is most useful for the broadest range of people. We often look at "logic" and "mathematics" as one thing, and even more than that, we look at them as absolutes - if something is mathematically proven, it is certainly a fact, no?

Well, it turns out even here there are still shades of gray, and the difference between classical and intuitionistic logic is the perfect example. Not everyone even agrees on the foundation of what logic and math are. And, each has their own benefits and strengths (intuitionistic logic tends to go hand in hand with type theory as the basis for theorem provers / proof assistants for mostly practical reasons).

Classical logic has always made the most sense to me, because accepting the law of excluded middle leads to a neater world of arguments to me. If you can't prove something, it is treated as false. Might be harsh, but that harshness yields simplicity.

I have come to at least understand the intuitionistic perspective though, because of how prevalent it is in the verification space - I have been super into F* recently (https://www.fstar-lang.org/), and this comes from a line of logics and programming languages that owe their life to intuitionistic logic. I like Andrej Bauer's position of being a "mathematical relavist," where he says "we cannot ignore the many worlds of mathematics" (http://math.andrej.com/2012/10/03/am-i-a-constructive-mathematician/).

Math and…

As someone who studies both CS and pure math, it's quite interesting when I see posts that take a very operational reading of functors and monads, instead of its shorter and more precise categorical definition (as a mapping from one category to another that acts homomorphically over morphisms). That's not necessarily wrong, but it's an important thing to keep in mind when learning category theory through a programming context (e.g. Category Theory for Programmers by Milewski). When I tried to learn category theory in this way, past a certain point the abstractions felt too unnatural and arbitrary (e.g. lack of examples for adjunctions and free objects), whereas a good mathematical treatment of category theory would provide plenty of examples across different areas of mathematics such as algebra, topology and logic.

I strongly agree with valenterry's comment[1] here, that post gives is an approximate definition of functors, even omitting the functor law. In particular, it is explaining what an endofunctor is (in the context of FP, you mostly deal with one category anyway). Furthermore, even in Haskell, there is no such thing as the category of Haskell types[0] (because of things like divergence and partiality).

For the curious, I've recommended Program Design By Calculation[2] to a number of people to show how category theory can be used as a powerful tool to reason about programs in an FP context while not compromising on the mathematics (the target audience is…

> I would like to see -- hint, I'm probably going to have to get my hands dirty! -- an implementation in either a dynamically typed language like Ruby/Python/Perl/PHP/Javascript/… or a non-functional language like C/C++/Obj-C/…

I understand where you're coming from. I'm working on a mini-ML in Python as a learning exercise for myself and possibly as a tutorial for others; will open source it soon.

As such, I've come across a few good resources:

check out Robert Small's Hindley-Milner in Python[0], as well as alehander42's Hermetic language in Python[1].

I also just found out about Hask, an implementation of many Haskell language features in Python. Looking at the source code, it's well-commented and clear, so I suspect I'll learn a lot from it as well [2].

Finally, even though it's not in a dynamic or non-functional language like you request, I highly recommend Andrej Bauer's Programming Language Zoo[3], which contains very simple and easy-to-understand implementations of various type systems in OCaml. Very elucidating.

0. http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hindley-milner-type-inference-implementation-in-python

1. https://github.com/alehander42/hermetic

2. https://github.com/billpmurphy/hask

3. http://andrej.com/plzoo/

Edit: Oh, and one more resource that's been extremely helpful has been "Introduction to Functional Programming through Lambda Calculus" by Michaelson. Well worth the cost of the book.

Thanks for articulating this.

https://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradiction/

also

"It’s fine to use a proof by contradiction to show something doesn’t exist. When the assumption that it does exist leads to a contradiction, then that shows it can’t exist.

It’s not so fine to use a proof by contradiction to show something does exist. Here’s the situation. The assumption that it does not exist leads to a contradiction. What can you conclude from that? You would like say “therefore it exists”. But you haven’t got any idea what it is. You may know it’s out there somewhere, but you have no idea how to find it. It would be better to have a proof that tells you what it is.

That’s a difference between what’s called “classical logic” and “intuitionistic logic”. In classical logic, proof by contradiction is perfectly accepted as a method of deductive logic. In intuitionistic logic, proof by contradiction is accepted to show something doesn’t exist, but is not accepted to show something does exist."

David Joyce, https://www.quora.com/In-math-are-there-any-proofs-that-can-only-be-completed-by-contradiction-If-so-how-would-someone-go-about-proving-that

You are right that for a particular formula p, the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) is an intuitionistic tautology and that the reverse implication is not (in general).

However the situation is different when you quantify over all formulas. If you have (¬¬p ⇔ p) for _any_ formula p, you also have (~q ∨ q) for any formula q (written with a different letter to not get lost in variable capturing issues).

This is because, for any formula q, we have the intuitionistic tautology ~~(~q v q). (Proving this is a fun exercise. If you get stuck, see page 26 of https://github.com/iblech/talk-constructive-mathematics/raw/master/negneg-translation-notes.pdf or elsewhere on the Internet.) So, if you assume the principle of double negation for all formulas, then in particular you assume that, for any formula q, the implication ~~(~q v q) ⇒ (~q v q) holds. Since the antecedent is unconditionally valid, the consequent is as well. Thus you have the law of excluded middle for q.

I highly recommend Andrej Bauer's blog for such matters. The post http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/ is a good starting point.

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

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-infinite-search-in-finite-time/