Hacker News new | ask | show | jobs
by seanmcdirmid 3047 days ago
Conjunction and disjunction are more apt anologies that have the same properties. There is also no division types while subtraction is used very rarely.
2 comments

I didn't think to call it that at the time, but I think that I came across a division type in react-redux the other day: https://github.com/DefinitelyTyped/DefinitelyTyped/blob/8f8f...

Playing with that a little, if adding a property to an interface is a product, eg:

    interface Foo {
        foo: string;
        bar: number;
    }
where Foo is a product of string and number, then removing a property from an interface is division:

    type Diff<T extends string, U extends string> = ({ [P in T]: P } & { [P in U]: never } & { [x: string]: never })[T];
    type Omit<T, K extends keyof T> = Pick<T, Diff<keyof T, K>>;

    interface Foo {
        foo: string;
        bar: number;
    }

    interface Bar {
        bar: number;
    }

    type Out = Omit<Foo, keyof Bar>;
the output type Out is equivalent to:

    interface Out {
        foo: string;
    }
or phrasing it another way:

    Out = Foo / Bar = (string * number) / number = string
I can't think what a 1/number type would be used for other than to remove number from a a T*number, in other words I can't think what a rational type would be used for unless it simplified down to a "normal" type. But I wouldn't like to bet that there's no other use :-)
What is the set theory intuition of that? If product is intersection, division is...?
Product is not intersection. The equivalent to product types in set theory is the Cartesian product ( https://en.wikipedia.org/wiki/Cartesian_product ).

The closest thing to a division would be a quotient set ( https://en.wikipedia.org/wiki/Quotient_set ), but there you're dividing by an equivalence relation. It is however possible to define an equivalence that undoes set multiplication: (A × B)/~ ≅ A if (a₁, b₁) ~ (a₂, b₂) holds iff a₁ = a₂, ignoring the other component.

That isn’t how product (intersection) types work in typescript. If we are talking about typescript, of course.
Product and intersection are different things in TypeScript, as well. The product of string and number would be a type like { first: string; second: number }, which combines two different values into one; whereas the intersection string & number is the type of all values that are both strings and numbers.
Right, but if we are going to call union types as sum types, why aren’t interesection types called as product types? Anyways, this is why the whole sum type thing breaks down and Union is more apt, since we can describe A|B and A&B using the same terminology family.
> Conjunction and disjunction are more apt anologies that have the same properties.

Conjunction and disjunction also have other properties, like idempotence: A /\ A = A, which by analogy would suggest that a tuple of two integers is the same as a single integer. Similarly, A \/ A = A, which is exactly the problem mentioned by the featured article that is the difference between union types and proper sum types (aka tagged union types).

So while sum and product may not be great analogies, conjunction and disjunction seem worse.