Constructivists are only interested in constructive proofs: if you want to claim "forall x in X, P(x) is true" then you need to exhibit a particular element of x for which P holds. As a philosophical stance this isn't super rare but I don't know if I would say it's ever been common. As a field of study it's quite valuable.
Finitists go further and refuse to admit any infinite objects at all. This has always been pretty rare, and it's effectively dead now after the failure of Hilbert's program. It turns out you lose a ton of math this way - even statements that superficially appear to deal only with finite objects - including things as elementary as parts of arithmetic. Nonetheless there are still a few serious finitists.
Ultrafinitists refuse to admit any sufficiently large finite objects. So for instance they deny that exponentiation is always well-defined. This is completely unworkable. It's ultrafringe and always has been.
> if you want to claim "forall x in X, P(x) is true" then you need to exhibit a particular element of x for which P holds
I don’t mean to be pedantic (although it’s in keeping with constructivism) but in the case you describe, you don’t have to provide a particular x but rather you have to provide a function mapping all x in X to P(x). It may very well be that X is uninhabited but this is still a valid constructive proof (anything follows from nothing, after all).
If instead of “for all” you’d said “there exists”, then yes constructivism requires that you deliver the goods you’ve promised.
It's likely: I purposefully stayed loose about the "infinite processes" to avoid going awry. I do however remembered him justifying his views as such though: he's not going into details, but he's making that point here[0] (c. 0:40). I assumed — perhaps wrongfully — that he got those historical "facts" correct.
There's not much connection. Typescript's record types aren't sound, but that's far from its only source of unsoundness, and sound structural typing is perfectly possible.
Soundness is also a highly theoretical issue that I've never once heard a professional TypeScript developer express concern about and have never once heard a single anecdote of it being an issue in real-world code that wasn't specifically designed to show the unsoundness. It usually only comes up among PL people (who I count myself among) who are extremely into the theory but not regularly coding in the language.
Do you have an anecdote (just one!) of a case where TypeScript's lack of type system soundness bit you on a real application? Or an anecdote you can link to from someone else?
> Do you have an anecdote (just one!) of a case where TypeScript's lack of type system soundness bit you on a real application?
Sure. The usual Java-style variance nonsense is probably the most common source, but I see you're not bothered by that, so the next worst thing is likely object spreading. Here's an anonymized version of something that cropped up in code review earlier this week:
I mean... yes, there's a footgun there where you have to know to spread first and then add the new properties. That's just a good practice in the general case: an intermediate type that fully described the data wouldn't have saved you from overwriting it unless you actually looked closely at the type signature.
And yes, TypeScript types are "at least these properties" and not "exactly these properties". That is by design and is frankly one reason why I like TypeScript over Java/C#/Kotlin.
I'd be very interested to know what you'd do to change the type system here to catch this. Are you proposing that types be exact bounds rather than lower bounds on what an object contains?
> That's just a good practice in the general case: an intermediate type that fully described the data wouldn't have saved you from overwriting it unless you actually looked closely at the type signature.
The issue isn't that it got overridden, it's that it got overridden with a value of the wrong type. An intermediate type signature with `updatedAt` as a key will produce a type error regardless of the type of the corresponding value.
> I'd be very interested to know what you'd do to change the type system here to catch this.
Like the other commenter said, extensible records. Ideally extensible row types, with records, unions, heterogeneous lists, and so on as interpretations, but that seems very unlikely.
Look into "Row types" and how PureScript, Haskell, and Elm (to a limited extent) do it.
'{foo :: Int | bar} is a record with a known property 'foo' and some unspecified properties 'bar'. You cannot pass a `{foo :: Int, bar :: Int}` into a function that expects `{foo :: Int}`.
A function that accepts any record with a field foo, changes foo, keeping other properties intact has the type
Ah someone else posted a link and I understand the unsoundness now.
The only time an issue ever came up for me was in dealing with arrays
let foo: number[] = [0, 1, 2]
// typed as number but it’s really undefined
let bar = foo[3]
But once you’re aware of the caveat it’s something you can deal with, and it certainly doesn’t negate the many massive benefits that TS confers over vanilla JS.
Yeah, that example is unsound in the same way that Java's type system is unsound, it's a compromise nearly all languages make to avoid forcing you to add checks when you know what you're doing. That's not the kind of problem that people usually are referring to when they single out TypeScript.
Informally, a sound type system is one that never lies to you.
Formally, the usual notion of soundness is defined with respect to an evaluation strategy: a term-rewriting rule, and a distinguished set of values. For pure functional programs this is literally just program execution, whereas effects require a more sophisticated notion of equivalence. Either way, we'll refer to it as evaluating the program.
There are two parts:
- Preservation: if a term `a` has type `T` and evaluates to `b`, then `b` has type `T`.
- Progress: A well-typed term can be further evaluated if and only if it is not a value.
> In Physics, entropy is a property of a bit of matter, it is not related to the observer or their knowledge. We can measure the enthalpy change of a material sample and work out its entropy without knowing a thing about its structure.
Enthalpy is also dependent on your choice of state variables, which is in turn dictated by which observables you want to make predictions about: whether two microstates are distinguishable, and thus whether the part of the same macrostate, depends on the tools you have for distinguishing them.
A calorimeter does not care about anyone’s choice of state variables. Entropy is not only something that exists in abstract theoretical constructs, it is something we can get experimentally.
> I dunno if this is the correct way of thinking about it, but I just imagine it as a particle that has mass but does not interact with other particles (except at big-bang like energy levels?).
Not even anything that extreme. What's ruled out is interaction via electromagnetism (or if you want to get really nit-picky, electromagnetic interaction with a strength above some extremely low threshold).
Constructivists are only interested in constructive proofs: if you want to claim "forall x in X, P(x) is true" then you need to exhibit a particular element of x for which P holds. As a philosophical stance this isn't super rare but I don't know if I would say it's ever been common. As a field of study it's quite valuable.
Finitists go further and refuse to admit any infinite objects at all. This has always been pretty rare, and it's effectively dead now after the failure of Hilbert's program. It turns out you lose a ton of math this way - even statements that superficially appear to deal only with finite objects - including things as elementary as parts of arithmetic. Nonetheless there are still a few serious finitists.
Ultrafinitists refuse to admit any sufficiently large finite objects. So for instance they deny that exponentiation is always well-defined. This is completely unworkable. It's ultrafringe and always has been.
Wildberger is an ultrafinitist.