Last Updated: September 02, 2018
·
40
· beezee

type algebra, or how much can the compiler help

The number of inhabitants for a given type is a computation based on the number of inhabitants for each involved type (eg (A, B) => C involves Product, A, B and C). coproduct is sum because you use an additive reduction on the number of inhabitants for each type in the coproduct to compute total possible inhabitants (and b/c void is 0), product is multiplication because you use a multiplicative reduction of the number of inhabitants for each type in the product to compute total possible inhabitants (and b/c unit is 0). function application is exponent because you raise number of inhabitants for return type to the power of number of inhabitants of the input type to compute total possible inhabitants (no unit for exponent? operation is not associative)

() -> Void = 0 ^ 1 = 0
Void -> () = 1 ^ 0 = 1
() -> () = 1^1 = 1
Bool -> () = 1 ^ 2 = 1
() -> Bool = 2 ^ 1 = 2
Bool -> Bool = 2 ^ 2 = 4

Either () () = 1 + 1 = 2
Either () Bool = 1 + 2 = 3
((), ()) = 1 * 1 = 1
((), Bool) = 1 * 2 = 2
(Bool, Bool) = 2 * 2 = 4

Either (Bool, Bool) () -> Bool = 2 ^ (2 * 2 + 1) = 2 ^ 5 = 32

etc etc.

lower those numbers, more compiler can help