SabrinaJewson

In Rust, `loop {}` is an expression of type `!`, which means that from a type-theoretic perspective it is inhabited. This means that the Curry–Howard correspondence fails for Rust.

You’re going to hate when you learn that the never type is inhabited

Do you have an example of a piece of code that behaves in a surprising way because of this rule?

You’re using “subtype” in two distinct, but related, senses here, and I think this should be clarified.

From a more category-theoretic perspective, a type A is a “subtype” of a type B when there is an embedding of A inside B. In this sense, `!` is a subtype of every type (which is its universal property). But this definition also grants you that `String` is a subtype of `BigInt`, because strings can be coded as bit sequences which can be coded in `BigInt`, which may or may not be what you expect.

From a programming languages perspective – and this is the terminology generally used in Rust – a type A is a “subtype” of a type B when `a: A` implies that `a: B`. In this sense, `!` is only a subtype of itself; although it coerces to any other type, it’s not _literally_ of that type, the coercion is just invisible in syntax. Importantly, if A is a subtype of B then `Vec<A>` is a subtype of `Vec<B>` – but `Vec<!>` is definitely not a subtype of `Vec<T>`, since they may have totally different layouts in memory (the former not allocating at all, while the latter potentially allocating).

How does that relate at all? Classical logic is not any less rigorous than other kinds of logic.

I do not think this parallel works, because I think you would struggle to find a discipline for which this is not the case. It is trivial to enumerate all the possible scientific or historical hypothesis, or all the possible building blueprints, or all the possible programs, or all the possible recipes, or legal arguments…

The fact that the domain of study is countable and computable is obvious because humans can’t really study uncountable or uncomputable things. The process of doing anything at all can always be thought of as narrowing down a large space, but this doesn’t provide more insight than the view that it’s building things up.

In general in Rust, “length” refers to “count”. If you view strings as being sequences of Unicode scalar values, then it might seem odd that `str::len` counts bytes, but if you view strings as being a subset of byte slices it makes perfect sense that it gives the number of UTF-8 code units (and it is analoguous to, say, how Javascript uses `.length` to return the number of UTF-16 code units). So I think it depends on perspective.

You’re ignoring the obvious reason, aside from the network effect: there are no alternative solutions. Some people are building Discord alternatives but they are far from production-ready, often lacking critical features (e.g. Matrix not being able to delete rooms, or still having trouble with decrypting messages). It is simply the case at this point in time that Discord is factually the least bad option for many many use cases.

You know that “learning disability” isn’t a synonym for “stupid”, right? We neither call people who are less academically able “disabled”, nor are disabled people necessarily less able to work academically (apart from some more debilitating mental disorders, which would be a disability). In fact, it’s quite the opposite: the word “disability” exists _precisely_ to distinguish “intelligence” – which is what the university is selecting for – and other characteristics, so in theory intelligence and disability are entirely orthogonal (apart from the exception I mentioned).

Of course, understanding what disability actually is requires considering each learning disability separately, which is something this article unfortunately fails to do. We can do this though:

- Anxiety and depression: I see no reason why this should decrease somebody’s intelligence, so the fact that there are elevated rates of such people at top universities does not seem odd. Since these are treatable conditions, they won’t necessarily affect the ability for a student to become an effective researcher.

- ADHD: This condition is marked by a lack of ability to focus, which is a property unrelated to intelligence. Some very famous mathematicians like Paul Erdős likely had ADHD, demonstrating that it’s not necessarily true this condition makes one a worse researcher.

- Autism: Does not necessarily reduce intelligence. We can look at professional mathematicians and see that a lot of them are autistic.

- Chronic pain, migraines, etc: Unrelated to intelligence. It’s possible this will decrease one’s ability to be a researcher, but if one is able to complete University at all, it’s likely not that severe.

I mean, I could go on, and of course there will be a couple of counterexample. However, it is still the case that generally speaking, “learning disability” and “stupid” are different things, and therefore there is no reason to expect that there would be lower rates of learning disabilities among those who are highly academically skilled.

I don’t know why you’re so angry at this statement, because it’s factually true. Do you truly believe that the proportion of families who stigmatize mental health care is negligible?

100%. The school and the Internet are the two places children can encounter opinions different from their parents’ for the first time. With an increase in homeschooling and recent pushes to ban social media for children, it’s clear that critical thinking is going to suffer most. I still have not met someone who was homeschooled who was remotely thankful for it.

Honestly, support for these policies that benefit, more than anyone else, abusive parents, makes me suspicious of people’s motives.

This comment contains a lot of false information. I’m first going to point out that there is a model of Lean’s type theory called the cardinality model, in which all types of equal cardinality are modelled as the same set. This is why I say the types have no useful distinguishing characteristics: it is consistent to add the axiom `Nine = Unit` to the type theory. For the same reason, it is consistent to add `ℕ = ℤ` as an axiom.

> So a Nine type with a single constructor is indeed isomorphic to Unit but it's not the same type, it carries different syntactic and semantic meaning and the type system preserves that.

It carries different syntax but the semantics are the exact same.

> Type theory is usually intensional not extensional so two types with the same number of inhabitants can have wildly different structures

It is true that type theory is usually intensional. It is also true that two types equal in cardinality can be constructed in multiple different ways, but this has nothing to do with intensionality verses extensionality – I wouldn’t even know how to explain why because it is just a category error – and furthermore just because they are constructed differently does not mean the types are actually different (because of the cardinality model).

> Cardinality is a set-theoretic notion but most type theories are constructive and syntactic, not purely set-theoretic.

I don’t know what you mean by this. Set theory can be constructive just as well as type theory can, and cardinality is a fully constructive notion. Set theory doesn’t have syntax per se but that’s just because the syntax is part of logic, which set theory is built on.

> most type theories don't enforce full parametricity at runtime

What is “most”? As far as I know Lean does, Coq does, and Agda does. So what else is there? Haskell isn’t a dependent type theory, so it’s irrelevant here.

---

Geniune question: Where are you sourcing your information from about type theory? Is it coming from an LLM or similar? Because I have not seen this much confusion and word salad condensed into a single comment before.