Remix.run Logo
Remix clone Hacker News
new | show | ask | jobsGithub
▲ thechao 3 days ago

Right. So, there's a unit type: the type that the sum of returns the other type, i.e.,

    a + () = a
So that means there's an identity type for the product type operator:

    a * 1 = a
I.e., the type that you can "multiply" by that doesn't give you a two-field tuple, but just returns the single-field tuple. If "1" is a type, then we can build a sum-type with it:

    a + 1 = (a, 1)
Ok. Cool. But! If we can "add 1", then we should be able to remove "1", right? That kinda implies that "-1" exists:

    (a, 1) -1 = (a,) # don't shoot the messenger, I'm just riffing
But, that also implies that we can allow a product type whose result is the "-1" type?

    (i, i) = -1
OH NOES!