Hacker News Reader

Comment by logicchains | Hacker News Reader

Type theory (or more generally, constructive mathematics) has some really nice properties, for instance guaranteeing computability, and allowing the extraction of proofs to programs. A lot of recent developments in the area were in fact driven by the late and great Voevodsky, a Fields medalists who certainly qualifies as a "mathematician". In my experience a lot of mathematicians who care about foundations, such as logicians, also like constructive maths. It's just analysts who don't, because they care about how well their foundations supports doing analysis, not about nice it is in some abstract sense, and constructive analysis is harder (because of the lack of the law of the excluded middle, which makes it harder to make the real numbers "complete", as you can't just pull out an arbitrary number between a and b without some way to construct it).

View on HN

As someone whose education straddled the four-pillars pure topics, mathematical foundations, and computer science, I share a bit of a wariness about AC with the constructivists, but I cannot let go of LEM. It's a big part of how I reason, and a number of results that I consider important and illuminating hinge upon it.

My (not entirely informed) sense is that constructive mathematics would have more success if more of an effort was made to pose it as a readily instantiable, tagged embedding within the larger classical mathematical corpus. Less Brouwer-style dogma about LEM being "wrong", more emphasis on streamlining a pathway for results to travel from the mathematical journal literature into software design specs.

Note that axioms are usually added, removing is weird. As such i see it mostly the other way around: there is a classical fragment inside constructive logic (this should not contradict what you said tho). In constructive logic, for a proposition `P \in Set` the proposition "P is in the classical fragment" is `dec(P) := P \/ P -> 0` (`0` being the empty type). As such we can define the set of classical propositions: `CL := exists P \in Set, dec(P)`, eg couples of sets together with either an element of it or a function that maps its elements to an inexistent thing (absurdity).

LEM is not wrong, it's just not always true. You must be familiar with the fact that AC is not provable in ZF, as such isn't LEM kinda philosophically wrong for AC? Not forcing LEM to be true is useful to have a better (more generic) understanding of complicated things. In general restricting logics (eg linear logic, constructive logic, etc) is only making them more powerful: we are able to express more propositions and we can internally (or externally as in linear logic with `!`) define the fragment for which the old axioms were valid. Pure languages enable explicit talk about computation, linear languages enable explicit talk about memory. Restriction are about increasing expressivity and most of we time we build them in the way that they retain the same proof-theoretic power.

Didn't you mean "implicit" here instead of "explicit"? Because I have no trouble at all to talk explicitly about memory and computation in full-blown set theory.

>It's a big part of how I reason, and a number of results that I consider important and illuminating hinge upon it.

How many of these results require applying the LEM to undecidable propositions? The LEM works fine in constructive logic for provably-decidable propositions.

It's just that I usually don't care about the decidability of propositions I apply LEM to, so I don't want to have to prove something first I don't care about.

This. I would also add that a substantial part of the type theory crowd are category theorist (or have developed acquaintance as category theorists are taking over type theory), which also do qualify as mathematicians (even tho they probably also qualify as haskell programmers). Discrete maths (graph stuff, algorithmic, algebra) and logic (languages, computability, crypto) pretty much are the definition of what constitutes theoretical computer science.

> even tho they probably also qualify as haskell programmers

For what it's worth, Haskell has very little to do with actual category theory. Even though terminology like "monad" is used, Haskell doesn't have much more overlap with higher mathematics than any other programming language. Mathematicians working on category theory and software engineers working on Haskell don't have much overlap at all.

This is kind of frustrating because it's a meme that Haskell is very mathematical. It borrows concepts from category theory, yes. But it's not anymore mathematical than calling a GET request "idempotent" is mathematical.

Common logic mistake, you inverted my arrows.

I didn't say haskell is mathematical (and i do agree to your point), i said category theorists probably know haskell of all languages because of the deeper understanding/intuition they will naturally have for it. There is no denying that haskell is laid on category theory foundation and that understanding these will help you. But of course well designed things do not require you to understand their foundations to build intuition/understanding.

No, I understand what you're saying. I am saying category theorists will not have any special affinity for Haskell or vice versa. I also don't agree that Haskell is built on top of category theory. That's why I mentioned the example of idempotence.

The idea that Haskell has much to do with mathematical category theory is a meme that arises from the cargo cult of functional abstraction. It's an example of terminology overloading. There is this pattern of taking terminology from abstract algebra and category theory and using it to describe design patterns in functional programming or certain paradigms of engineering. "Monad" is one you see in Haskell which ostensibly makes it related to category theory. Another example is the idea of an "isomorphism" in web development, which doesn't mean the same thing as it does in algebra.

There's no problem with using terminology borrowed from mathematics for design patterns in engineering (and vice versa), but it should be transparent about the fact that it doesn't confer any special relation to the underlying mathematics. A category theorist and a Haskell programmer have different conceptions of what a "monad" is, and any functional design pattern modeled after an idea in category theory is going to be covered in the introduction or first chapter to a textbook. The language has more to do with lambda calculus than it does anything in actual category theory.

Reply on news.ycombinator.com