DEV Community

Discussion on: Sets, sets are everywhere

610yesnolovely profile image
Harvey Thompson • Edited on

Yes, I think so. I think you're talking about the construction of the properties of the Intersection Type C using the product operation on A and B to produce the state/record of C. This is probably valid for TypeScript (I'm guessing here, since I'm not super familiar with it).

It was confusing me because I tend to think about the type representing the set of possible instances of the types involved, so the names match: a Union Type has instances which are the union of each type's instances, similar for Intersection Type (the instances of C are by definition the intersection of A and B's instances).

For my language, at the type level, state is not directly modelled because it's hard to reason with and does not allow multiple inheritance (*). Thus when I deal with union and Intersection types the operations to implement these are always set-theoretic union and intersection (set of permissible methods, super-type, etc).

As you also mention, computation of union and intersection types (and different/not types, which I also will have because I want Flow Typing which pretty much requires all three), together with a rich type system including generics, tuples, functions and with a sound and complete sub-typing relationship makes for a complex type system.

(*) I have multiple type kinds, one of which is Class (a Type with ordered state), which is limited to single inheritance of another Class, but would eventually allow multiple inheritance of Traits (a Type without state). The state is not visible to the type system, and so reasoning about type operations is made a lot easier. A lot of languages have adopted this, but I'm guessing TypeScript (because it's on top of JavaScript) is not one of them.

NOTE: I could be talking complete nonsense because this stuff is freakingly complex, but it's working well so far.

FYI: You might like On Declarative Rewriting for Sound and Complete Union, Intersection and Negation Types - and some of the previous papers also by David J Pearce.

Thread Thread
610yesnolovely profile image
Harvey Thompson

Oh I forgot to respond to your question: "Do you have something in public already (link to a repo)?" - not currently, I'm at version 0.2 so it's early years yet - ask me again in about two years ;-) (Who knew writing a programming language could be so hard!)