re: Sets, sets are everywhere VIEW POST

TOP OF THREAD FULL DISCUSSION
re: Great article! This sort of understanding is becoming more and more useful - quite a few new programming languages include some or all of these con...
 

The code block when first introducing Cartesian product uses A ∪ B, should be A × B.

Yes it was a typo. FIxed. Thank you

This section does not seem to be correct

Why not?

I'm developing a new programming language

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 TypeScript can be explained with or corresponds to cartesian 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!)

code of conduct - report abuse