TypeScript and Set Theory | Hacker News Reader

TypeScript and Set Theory

ivov.dev

112 pointstodsacerdoti24 comments

Conditional type expression are indeed very powerful and, little known fact, can be used to generate types recursively.

Here's a type signature from hell with its usage:

  type Component = { type: 'a' } | { type: 'b' };

  type FoundComponents<T extends any[]> = T extends [a: infer A] ? [Extract<Component, {type: A}>] :
  T extends [a: infer A, ...b: infer B ] ? [Extract<Component, {type: A}>, ...FoundComponents<B>] : never;

  export function findComponentSets<T extends Component['type'][]>(components: Component[], ...componentTypes: T ): FoundComponents<T>[];
  export function findComponentSets(components: Component[], ...componentTypes: Component['type'][] ): Component[][] { return [] }

It recursively picks outputs types based on the input parameters, so if you call e.g. findComponentSets([], 'a', 'b') the output type will be [{type: 'a'}, {type: 'b'}][].

I'm using it in an Entity Component System based game I'm writing to type check the function which receives a flat list of Components and type selectors and outputs a list of tuples with the selected Component types.

  findComponentSets(components, 'position', 'hit-box')
    .forEach(([position, hitBox]) => system.process(position, hitBox));

ohh that's really interesting. Any chance of open sourcing this as a library?

This is an example of Typescript kinda sorta have some of what Dependent Types will give you. The problem is that the Typescript team hasn’t fully embraced this. So instead of implementing Dependent Types (see Agda/Idris/LEAN), the team is kinda sorta implementing parts of it piece wise, inventing different syntax for each feature as they add it. A bit like templates in C++ ended up kinda sorta implementing a Turing complete functional programming language with the worlds worst syntax. It looks as if Typescript is going down the same road. It’s a bit of a mess compared with Dependently Typed languages (Agda/Idris/…)

The section on how union & intersection types behave with interfaces (rather than primitives) has them flipped: a union of interfaces will allow access to only the intersection of the fields/methods of all the types (unless you do the work to distinguish between which type you're working with), while an intersection will allow access to the union of the fields/methods of the composed types.

i.e. `ICat | IDog` will only allow `pet.eat()`, and `ICat & IDog` will allow `pet.eat()`, `pet.meow()`, and `pet.bark()`.

Good article otherwise, though. The explanation of top/bottom types was more intuitive than most attempts.

That's incredibly interesting, because I've been using union types a while and didn't know this. I think a lot of people will get introduced to them via function signatures, and var: ICat | IDog not meaning "var could be an ICat or an IDog" is a bit unintuitive given the boolean math.

But ultimately more useful? As in, code should never test whether this thing is an ICat or IDog, and I guess it's interesting that I don't remember ever encountering an issue where I attempted to access a member that was only present on one interface.

Perhaps it would be too overloaded, but "ICat + IDog" instead of "ICat & IDog" feels more obvious, I suppose a better convention for "ICat | IDog" is difficult though. "ICat /\ IDog" for intersection and "ICat \/ IDog" for union doesn't roll off the tongue.

I think ICat | IDog is perfect. It means exactly that, the value can be of type ICat _OR_ IDog, so in that sense, we can only access properties that are in both of them until we know for sure if we are dealing with a ICat or a IDog specifically.

"+" is probably a bad choice: sum types are a separate thing. In TypeScript, they can be implemented as

     Sum<X, Y> = { tag: "left", data: X } | { tag: "right", data: Y }

Generally higher order types are named according to what they do to types, not terms. `x: ICat & IDog` means "x is in the intersection of ICat and IDog", not "x is the intersection of an ICat and an IDog". (The latter interpretation only even makes sense for record types and a few other special cases: what's the intersection of an integer and a string supposed to be?)

For anyone with trouble remembering/conceptualizing this - it follows the opposite convention as bitwise operators in javascript, so it is counter-intuitive.

https://developer.mozilla.org/en-US/docs/Web/JavaScript/Refe...

The naming of TypeScript Union and Intersection types, with respects to type theory, used to be terribly confusing/contradictory:

https://www.typescriptlang.org/docs/handbook/unions-and-inte...

See last paragram under «Unions with common fields»

Leading to terribly confusing TypeScript cheat sheets such as this (see the union and intersection venn-diagrams):

https://carltheperson.com/images/magic-typescript/magic-type...

Compare with: https://en.wikipedia.org/wiki/Intersection_(set_theory)

Luckily TypeScript recently updated their docs, and the issue has been clarified in posts such as this:

https://stackoverflow.com/questions/38855908/naming-of-types...

Turns out, naming things is really hard, because what you implicitly refer to when you unionize or intersect turns out to be of vital importance.

I agree. I wish the Typescript team had simply embraced Dependent Types from the beginning instead of adding a laundry list of ad-hoc solutions with special syntax. It’s already way more complicated than it needs to be. Solving a problem you can either use a simple but powerful solution or add patch after patch forever until you kinda sorta have covered everything that the simple powerful solution would have given you. It looks as if Typescript unfortunately is going down the patches route requiring cheat sheets and memorisation to work with. Exactly what happened with C++ templates.

TypeScript also lets you create subsets of infinite size. For example, a string template literal type can be a type with (theoretically) infinite string values matching a string template.

I've created a proposal for doing something similar with the number type that uses the relational operators (<, >, >=, <=) to narrow the types [1].

It may be not as useful as template literal types (which is why one could argue to not implement them), but it's interesting nonetheless.

[1]: https://github.com/microsoft/TypeScript/issues/43505

This is backwards: types (as in Type Theory) were invented because sets didn't quite work. So it's not accidental that it turns out types are quite like sets.

> Finally, be aware that for a conditional type to trigger distributivity, the checked generic must be by itself to the left of extends, that is, not passed into another generic or otherwise altered during the check.

Ah, this helped my brain click with a problem I’ve encountered several times. I think the most common reason I encounter this is when using generic memoized components in React. The generic parameters seem to be missed by the compiler completely, so something like a memoized polymorphic component becomes impossible to compose further into other components.

I guess the problem is that the memo function has inferred generic parameters which causes distributivity to be disabled on the nested generic parameters.

At least I think this is the case. I need to dig a little deeper, but I’m fairly sure this explains it.

This was a great read. I intuitively think in sets quite often, but it hadn’t occurred to me how overt the set theory is in TypeScript. This opened my eyes to the reason behind certain unintuitive behaviours (especially intersecting interfaces).

As an aside, a workaround for that case is:

  const Comp = React.memo(NonMemoComp) as typeof NonMemoComp

Yeah, this has been the approach I’ve used but the purist in me really goes crazy not having it “just work”. Admittedly it’s pretty hard to have casting in cases like this come back to bite you. I suppose you could even write a lint to ensure memoized component casting is correct.

Sets isn’t just “a branch of mathematics”. Sets is the foundation of traditional mathematics. However it has problems (paradoxes). Type theory was invented to solve those problem. And most modern proof assistants are based on some variation of type theory. Type theory is in many ways much simpler than Sets: The Set axioms are built on logic. While the (Martin Loff) type theory axioms aren’t. In other words, Type theory is much simpler than Set theory. The two theories look similar at the surface level. However they are fundamentally different. Values in type theory always comes with a type. That is not the case in Set theory. It makes a huge difference to how you use the two to prove things.

I just wanted to comment on the website, I really love this UI

That is very simple and beautiful website. Author did a great job both aesthetically and technically.

I wonder if its a Framework like hugo or is it custom built?

Looking at the DOM, it's Next.js with Tailwind.

I especially bookmarked it under "nice sites", too.

It looks remarkably (suspiciously) similar to Brian Lovin's website https://brianlovin.com

What an excellent read. I wish all technical articles were written this clearly.

I love these diagrams. Does anyone know what they were created with?

I think it's excalidraw

Reply on news.ycombinator.com