### Sets, sets are everywhere

#### stereobooster on April 20, 2019

I strongly believe that it is ok to learn on the go (unless you have a life-critical profession, like a doctor of medicine or you writing softwar...
[Read Full]

I strongly believe that it is ok to learn on the go (unless you have a life-critical profession, like a doctor of medicine or you writing softwar...
[Read Full]

Great article! This sort of understanding is becoming more and more useful - quite a few new programming languages include some or all of these concepts (such as TypeScript, Scala, Swift, Kotlin, Ceylon).

I highly recommend the Types and Programming Languages by Benjamin C. Pierce. It's somewhat math heavy, if you're not into such things, you can still get a lot of the concepts out of it.

Also I think there's a couple of minor mistakes:

I'm developing a new programming language which has these concepts, so this kind of thing really interests me.

Yes it was a typo. FIxed. Thank you

Why not?

wow, cool. Do you have something in public already (link to a repo)?

At least in Set Theory cartesian product and intersection are two separate concepts: product produces tuples, intersection produces a subset of common elements.

Ah, yes. Similar names - my favourite source of the confusion. Read this as following

intersection types in TypeScriptcan be explained with or corresponds tocartesian product in sets. If you would treat "intersection types" as proper noun (not as name with meaning) you can follow the logic of the article, right?Full picture: actually it is not coincidence that "intersection types" name collides with "intersection" operation in sets. Let's rewind a bit and see what we are doing here - we showed partial correspondence between types and sets. We didn't show full correspondence, for example how to encode lambda types (`a -> b`

), how to encode parametric types. We just show correspondence of some ideas in sets to some ideas in types in programming language. And it is up to us how we choose correspondence, it is not necessary one to one correspondence.So what they call "intersection types" can be explained with cartesian product (what I did, and what I have seen in some papers) or with intersection (what probably authors of TS did). If we take that

`type A = {a: number}`

corresponds to sets of all records (or objects in terms of JavaScript) which have property`a`

as number, but not limited to this property only, for example`{a: number, c: string}`

also counts as type A; and we take`type B = {b: number}`

, we can see that objects of type`{a: number, b: number}`

is of the type A and B simultaneously. We can say that`type C = {a: number, b: number}`

is the same as`A & B`

and in types this operation would correspond to intersection.I called it partial correspondence, other way to name is "modeling", the same way they build mathematical model of physical phenomenon (

`F = GM₁M₂/r²`

). We modeled types in programming language with sets from math. And some models work well in one cases, and don't work in different. Models are approximations, models are platonic representation of some phenomenon.Does it make sense now?

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.

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!)

I haven't seen set theory in a long time, and you remind me how much I miss math. What are the most common ways that you are using it to solve problems today?

Well, as I said as data structure I would use it to find unique values of the list (like a list of ids) or find the intersection of two lists, or check if the item already present in the list. Plus I use TypeScript - unions, intersections.