Making sense of TypeScript using set theory

https://blog.thoughtspile.tech/2023/01/23/typescript-sets/

by hrafnstrom • 3 years ago

140 91 3 years ago

blog.thoughtspile.tech

scotty793• 3 years ago

Why does 0 | 1 extends 0 ? true : false evaluate to false?

Because 'extends' really means 'is assignable to'.

I feel like most of the questions from the post might be answered fairly easily by using reasoning of 'is assignable to'.

Things assignable to A&B are things assignable to both A and B.

Things assignable to A|B are things assignable to A or to B.

'never' means a type that nothing is assignable to and is assignable to everything (bit weird because it usually doesn't have any values but you can create value of type never with the use of 'as').

'unknown' means a type that everything can be assigned to but it's not assignable to anything (except itself and any).

'any' means a type that everything is assignable to and that is assignable to everything (except never).

Ok. Ok. {} types is bit weird way to denote interfaces. :-)

thoughtspile13• 3 years ago

Fair enough, "is assignable to" is another synonym for "is subset of". I find it much easier to reason about things I can visualize, like sets, which is why I love my set interpretation.

Edit: besides, it's quite unintuitve that "never" is assignable to anything. How can never be something?

scotty793• 3 years ago

It's harder for me to make that connection but thank you for your write up. It's really great.

Danoha• 3 years ago

Because "never" is an empty set and empty set is a subset of all sets.

scotty793• 3 years ago

it's quite unintuitve that "never" is assignable to anything

Yeah, at first I was mislead by this.

Initially I thought never is opposite of any while, it turns out, it's opposite of unknown. And any is just super weird, dynamic wildcard thing that is as large or as small as needed for any given operation (but not as small as never).

lmm3• 3 years ago

Fair enough, "is assignable to" is another synonym for "is subset of".

Only if you're happy to conflate members and sets, which is pretty confusing IMO. If I write a = b I don't generally think of b as being a set, even though in some sense it is; "b is an expression with this type" is a much more natural way of thinking to me.

LudwigNagasena4• 3 years ago

Yeah, `extends` seems like a misnomer that confuses people.

maxfurman• 3 years ago

The difference between `any` and `unknown` is that `any` is an escape hatch from the type system. `any` can be used anywhere and will satisfy any type constraint. `any` is how the developer says to the type system "trust me, I know what I'm doing, don't worry about this particular value." Unknown, on the other hand, is for untyped code from an imported JS library, JSON data received from the network that may or may not match the API spec, etc. Code that does have a type, but that type needs to be confirmed at runtime and can be narrowed through type guards.

thoughtspile13• 3 years ago

I think "unknown" is more than that! Basically it's a way to say you don't care about the type, as in Record<string, unknown> or P extends Promise<unknown>

jax_the_dog2• 3 years ago

How is unknown better than any in this case? If you do not care about the data type, wouldn’t you say that “any” data type is acceptable? If you say “unknown” that means that there is possibly some data type that would break your function.

edgyquant• 3 years ago

But you have to care about the type with unknown? For instance calling this on an unknown

    obj.value

Will return a type error that value doesn’t exist on unknown. While calling it on an ant is valid typing

sirmarksalot3• 3 years ago

This is technically correct, but I suspect it's pretty rare that you would choose "unknown" over a generic parameter. Even if you're writing an algorithm that doesn't care about the data type, it's still probably going to be used by application code that does care, and you'll want to support that need by passing the type through, otherwise the application will be forced to downcast.

piyh• 3 years ago

I went through my code base and found one use of `any` that was worth keeping around, the rest could be changed to `unknown` and better code resulted from it.

theonething• 3 years ago

I know what I'm doing

`any` can also be an indicator of the exact opposite.

mrbombastic• 3 years ago

It certainly is for me :)

joshfee• 3 years ago

`any` should really be called `every` to match the semantics, it says "this value is an instance of every type, and therefore you can do anything with it".

And you might read that and thing "but that's crazy, its not possible for a value to be an instance of everything!" and you'd be right - the `any` type in TS is in fact crazy and you should not use it.

consilient3• 3 years ago

The intersection of all typescript types is `never`. `any` is approximately equivalent to `unknown` in contravariant positions and `never` in covariant ones.

dclowd9901• 3 years ago

That’s a convenient way of thinking about it. A more logically correct way of thinking about it is:

“any” can be any possible type

“unknown” is a specific stand-in type. It does not represent all types but is a subset of all types, which allows you to narrow its definition from nothing.

Unknown in practice is closer to a generic in terms of usage and semantics than “any”. It’s like a generic generic except it’s not useful until you direct it. It basically lets you kick the can down the road in your code of having to make a type decision, which is very useful for writing composable and uncoupled code.

jakelazaroff• 3 years ago

I might be missing something, but isn't this line backwards?

Subtype of type A is a subset of type A. Supertype is a superset. Easy.

Subtype of type A is actually a superset of type A, since it contains at least all the properties of A.

If you had (contrived example) a Dog class that inherited from an Animal class, Dog would be a subtype of Animal, but its additional properties (say, a bark() method) mean that it actually has a superset of the properties in Animal. And vice versa: Animal is a supertype of Dog, but it's a subset because it contains only the properties that Dog inherits.

epolanski• 3 years ago

Subtype of type A is a subset of type A. Supertype is a superset. Easy.

I think it is correct.

Example:

type A = { a: number }

type B = { a: number, b: number }

B is not a superset of A, it's a subset and subtype of A. You can use B every time you want to use A.

In other words, of all types that can be assigned to A or used in functions and types expecting an A, B is one of those subsets.

type C = { a: number, c: number }

is another subtype of A.

A "subtype" C can be substituted in place of its "supertype" A.

Both C and B are subsets of A, in other words: in the infinite set of values of type A, some can be grouped in a type B or C. C itself is a subtype of A.

thoughtspile13• 3 years ago

You're making the same mistake as I sometimes do, thinking in terms of "object shape" or "functionality". Here, I use "subset" in a sense of "all values that belong to Sub also belong to Super", in line with a set-theoretic view of types in the post. Also see subsets on wiki: https://en.wikipedia.org/wiki/Subset

Try this one: A is subset of B iff all the values that belong to A also belong to B. In your example (and in real life), every dog is an animal, so dogs are a subset of animals.

hbrn8• 3 years ago

Types are not features, they are constraints.

"at least all the properties of A" means "all of the constraints of A and some more". Subtype of A is more narrow than A, even if it means that object of subtype A has to have more fields.

feoren• 3 years ago

In your case, dogs are only those animals that bark. That's a subset of animal. Think of it this way: can you think of an object that satisfies (is-a) Dog, but not Animal? No. Can you think of an object that satisfies Animal, but not Dog? Yes. So Dog ⊂ Animal.

hbrn has it right calling those properties constraints, not features. With anything but a sealed class, the properties that are not present are unspecified rather than missing.

And indeed sealed classes feel very "un-set-theoretic" to me.

RyanCavanaugh• 3 years ago

Nope. This is a common confusion.

The set of properties of objects and the sets of objects themselves have a complementary relationship when it comes to union / intersection and subset / superset.

Let's define a "property" as being a predicate that is true for all elements of a set. For example, a collection of red objects has the "red" property.

A subset of a set of objects can only have the same or more properties than the set you started with. If you take a bunch of marbles of varying colors, selecting a subset of those marbles can yield a set with a new property (such as them all being red), but they are guaranteed to have the "marble" property.

A superset of objects can only have the same or fewer properties than the set you started with. Adding marbles to an existing set of marbles can only make "they are all red" become false (if it was true to begin with).

Union and intersection have the same duality; the union of two sets has the intersection of its properties, and the intersection of two sets has the union of its properties.

These results come from logic, not TypeScript.

yitr• 3 years ago

maybe a dumb question, but why does wikipedia say typescript is a superset of javascript?

https://en.wikipedia.org/wiki/TypeScript

antihipocrat3• 3 years ago

In your example with marbles, the superset has the property of every element being comprised of a set of colors, let's say {black, red, blue}.

The subset is {red}.

Can't every possible property we can conceive of a subset be constructed in a similar fashion such that the superset contains at least the same number of elements and never less?

LudwigNagasena4• 3 years ago

I think that interfaces in TypeScript unfortunately contribute to that confusion. I can do

  interface Point2D {
    x: number
    y: number
  }

And then I can do

  interface Point3D extends Point2D {
    z: number
  }

And that "extends" really throws off many people because in reality the type of Point2D is implicitly

  {
    x: number
    y: number
    [anything_else in string]: unknown
  }

So Point3D actually narrows the type of Point2D even though the notation suggests that it widens it. Fortunately, the type notation is less misleading because I can do

  type Point3D = Point2D & {
    z: number
  }

Without any misleading "extensions".

It seems like it all stems from the tight coupling between types and classes in a typical OOP paradigm. When you create a class Animal you create a type Animal that should conform to specific rules, but when you instantiate that class you create an object that conforms to a narrower set of rules. E.g. an object instantiated from class Animal won't be able to woof() even though the type "Animal" easily allows it. This leads to the mental model of "extending" base class with new fields and methods. And even though it indeed extends the class Animal, it narrows the type Animal.

Tainnor3• 3 years ago

This depends on what you mean by "property".

Universal properties are preserved "downwards" i.e. in subsets (more properly, substructures). Existential properties are preserved upwards, i.e. in supersets (extensions).

For example, the property "there exists an element that equals itself when added to itself" is preserved in a superset.

If you have sentences that mix quantifiers (e.g. "for all epsilon, there is a delta ..." or even just "every element has an inverse"), then all bets are off.

The branch of mathematics where this is studied (and rigorously proven) is model theory.

edit: I guess by "property" (given the context of the discussion) you might just mean "function" or "method", in which case, yes, a function defined on a set is also defined on a subset but not necessarily vice versa, so there are in a certain sense "more" functions defined on the subset.

Koshkin• 3 years ago

4. A extends B ... can be read as "A is subset of B".

I agree, it is unnatural to think of a subset as "extending" the set it is part of.

Jtsummers• 3 years ago

Yeah, it's a common way of telling people how to read "A extends B", but it's not quite right. The two relationships are related (no pun intended) but they aren't the same relationship. `A extends B` means (in the OO world) that A adds fields, methods, or changes the behavior of methods to B. `A is a subset of B` means that all As are Bs, but some Bs may not be As.

It happens that `A extends B` introduces a subset relation between them, but it's not correct to describe it as the same as the subset relation.

jotaen• 3 years ago

I think what’s confusing here is that there are two mental models that use the word “type” in an opposing way: if you think of types in terms of set theory, then “subtype of type A is a subset of type A”. But if you think of types in terms of a class hierarchy (like in Java), then by saying “subtype of type A is a superset of type A” you actually mean “an inherited type (class) that is further down in the class hierarchy has the same or more properties than the parent type (class) that is further up”.

So I actually would agree that your original statement is valid, assuming that you refer to “types” as “classes” in the sense of Java class hierarchies.

clord2• 3 years ago

Having set types like this and refining them smaller is something I wish Haskell would learn from Typescript, especially the automatic inference side. I wonder if it would help with linear types? Are there any proposals? I know there are type level naturals in the type system, but this is more like wanting to deconstruct existing types like Int or String into subset types.

e.g.,

foo :: Int -> 3::Int | 4::Int

foo 4 = 4

foo _ = 3

bar :: 3::Int | 4::Int -> Bool

bar 4 = True

bar 3 = False

-- (bar 12) is a compiler error, and no need to handle other patterns

baz :: 3::Int | 2::Int -> Bool

bar 3 = True

bar x = False -- Type of x is 2::Int

consilient3• 3 years ago

Having set types like this and refining them smaller is something I wish Haskell would learn from Typescript, especially the automatic inference side

Haskell has far better type inference than Typescript in large part because it doesn't have subtyping.

There are libraries for open records and sums (e.g. https://hackage.haskell.org/package/vinyl) but they're almost always the wrong choice.

Tainnor3• 3 years ago

Haskell has far better type inference than Typescript in large part because it doesn't have subtyping.

That's a bit like saying "Go has a faster compiler because the language is so simple". It's true, but there's a genuine tradeoff here.

Haskellers have convinced themselves that subtypes are not worth it - and they may be right in many cases - but subtyping is a quite natural way of modeling many concepts (for example: mathematical expressions). Some of that can be recovered by typeclasses, existential types and other machinery (or you could go as far as dependent types), but that seems all more cumbersome and hard to understand than the way subtyping works in languages that support it out of the box.

nequo• 3 years ago

LiquidHaskell[1] implements refinement types for Haskell. Would that do what you'd like?

[1] https://ucsd-progsys.github.io/liquidhaskell/

clord2• 3 years ago

unknown is the set of all JS values. any is a paradoxical set that includes everything, but might also be empty.

Not really a paradox.

- `unknown` is the intersection (&) of all types, including an internal one that has no shape or characteristics. `unknown | {int: number}` should be `{int: number}`. `unknown & T` is always `unknown`, any characteristic T has will be discarded by the intersection.

- `any` is the union (|) of all types, including that internal one that can be anything, and yes, `unknown` too. `(any & {int: number})` should be `{int: number}`. also, `const x: any = 5 as unknown`. Union with `any` should always produce `any`.

thoughtspile13• 3 years ago

I'm afraid you're confusing something!

The intersection of all types is never, because, say, number and string don't intersect. The union of all types is unknown.

any doesn't show set-like properties and yields ternary logic in clauses like any extends T, which makes it a paradox.

bazoom422• 3 years ago

I think you have switched union and intersection. ’Unknown’ is a type which can be anything, so it is the union of all types. ‘Never’ is the empty set of types.

‘Any’ does not really fit into a set theoretical model because it can be assigned to anything and anything can be assigned to it, so it is both a supertype of anything and a subtype of anything. Basically it just disables type checking.

david-farr• 3 years ago

Great article!

Not entirely related to the post, but what app did you use to create your diagrams? They look fantastic.

thoughtspile13• 3 years ago

Thanks!

I use excalidraw: https://excalidraw.com/

I think most web-dev bloggers use it, makes me feel very boring

hot_gril2• 3 years ago

Unrelated set theory thing: They say Typescript is a "superset" of Javascript, but plenty of valid JS code won't work in TS. For example, `let foo = 4; foo = "4";`

goodoldneon2• 3 years ago

That isn't what "TS is a superset of JavaScript" means. That phrase means "TS syntax is a superset of JavaScript syntax". Your example is syntactically valid in TS -- it just fails a type checking

hot_gril2• 3 years ago

I see what you're saying about syntax and type-checking being separate stages, but they're both compile-time (or do we call it transpile-time?) errors enforced by the language. Either way, I can't copy-paste working JS code into TS, which is what matters.

There's probably another "asterisk" for this, but the other thing is how TS in Node by default won't allow `require` (vanilla NodeJS), only `import` (ESM).

Making sense of TypeScript using set theory

Related Stories