As the creator of a library that lets you import Markdown into Typst directly in the Typst build process, without the use of external tools like Pandoc, I confess I find it this all a little inconvenient!
It seems more advantageous to me to have only one build step and no intermediary files. We don’t support all the exotic features of Pandoc Markdown, but support much more customization in other areas.
Related is the paper [What is a closed-form number?], which explores the field E, defined as the smallest subfield of ℂ closed under exp and log. I believe the set of numbers that can be generated using exp-minus-log is a strict subset of this.
In a similar vein to this post, the paper points out that general polynomials do not have solutions in E, so of course exp-minus-log is similarly incomplete.
What is intriguing is that we don’t even know whether many simple equations like exp(-x) = x (i.e. the [omega constant]) have solutions in E. We of course suspect they don’t, but this conjecture is not proven: https://en.wikipedia.org/wiki/Schanuel%27s_conjecture
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 can claim that “learning disability” should mean whatever, but this does not change the fact that medical experts define “learning disability” such that they do not inherently impede intelligence: https://ehvi.org/learning-vs-intellectual-disabilities/. This isn’t my definition, it’s the definition used by medical experts. A quote from that article:
> Learning disabilities don’t affect intelligence and are different from intellectual disabilities. People with LDs have specific issues with learning but have an average or above-average IQ (intelligence quotient).
I acknowledge that I was including autism as a learning disability, but I see this isn’t the case. Still, however, I hope you would acknowledge that autistic people are not inherently less intelligent than others, and neither are people with depression nor anxiety.
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.
In type theory, all singleton types are isomorphic and have no useful distinguishing characteristics (indeed, this is true of all types of the same cardinality – and even then, comparing cardinalities is always undecidable and thus irrelevant at runtime). So your Nine type doesn’t really make sense, because you may as well just write Unit. In general, there is no amount of introspection into the “internal structure” of a type offered; even though parametricity does not hold in general (unless you postulate anticlassical axioms), all your functions that can run at runtime are required to be parametric.
What about DEI makes it an “ideological” movement as opposed to other movements who are presumably not ideological?
And I’m not sure what “most people”, is supposed to mean; you do realize you’re talking about 49% – that is, under half, so definitively not “most” – of the US of A’s population?[0]
Ferrocene is a specification but it’s not a formal specification. [Minirust](https://github.com/minirust/minirust) is the closest thing we have to a formal spec but it’s very much a work-in-progress.
English alternatives like “The staff enjoyed it later” or “The staff had the pleasure of eating it later” I would expect come across more euphemistic than normal to the average English-speaking viewer. So the question is whether the original was intentionally trying to come across euphemistic, or whether the original was using formal/polite language solely because of its position as being on TV.
No, because you only have to choose _one_ s for the proof to work, and a finite number of choices is valid in intuitionistic and constructive mathematics.
> Addressing your issue directly, the Axiom of Choice is actively debated:
The axiom of choice is not required to prove Cantor’s theorem, that any set has strictly smaller cardinality than its powerset.
Actually, I can recount the proof here: Suppose there is an injection f: Powerset(A) ↪ A from the powerset of a set A to the set A. Now consider the set S = {x ∈ A | ∃ s ⊆ A, f(s) = x and x ∉ s}, i.e. the subset of A that is both mapped to by f and not included in the set that maps to it. We know that f(S) ∉ S: suppose f(S) ∈ S, then we would have existence of an s ⊆ A such that f(s) = f(S) and f(S) ∉ s; by injectivity, of course s = S and therefore f(S) ∉ S, which contradicts our premise. However, we can now easily prove that there exists an s ⊆ A satisfying f(s) = f(S) and f(S) ∉ s (of course, by setting s = S), thereby showing that f(S) ∈ S, a contradiction.
> For example, the idea that there are the same number of integers as even integers is a stupid one that in the end does not lead anywhere useful.
I am not sure what you are arguing here. We’ve been teaching this to all undergraduate mathematicians for the last century; are you trying to make the point that this part of the curriculum is unnecessary, or that mathematics has not contributed to the wellbeing of society in the last hundred years? Both of these seem like rather difficult positions to defend.
It seems more advantageous to me to have only one build step and no intermediary files. We don’t support all the exotic features of Pandoc Markdown, but support much more customization in other areas.
The library: https://github.com/SabrinaJewson/cmarker.typ