If function has 1 of v outcomes taking 1 of n arguments, we can form vn distinct functions: first argument distinguishes v functions, applied second argument value, we can further resolve every of v functions into v other functions, yielding v2 distinct functions and so on up to vn distinct funcs.
→ | ⊥ | () | TF |
⊥ | 0⁰ = ? | 1⁰ = 1 | 2⁰ = 1 |
() | 0¹ = 0 | 1¹ = 1 | 2¹ = 2 |
TF | 0² = 0 | 1² = 1 | 2² = 4 |
You see that that there is always one func from bottom type ⊥ to any type T in your type system, x:T → ⊥, (and 0 inverse functions) making ⊥ the best candidate for initial object, as explained in chapter 5. It also suggests why unit type () has always one function from any user type to it, serving as terminal object.
The particular functions are
⊥ → ⊥ : def voidID (v: Void) = v ⊥ → (): def void2unit(v: Void) = {} ⊥ → TF: def void2Bool(v: Void) = true ⊥ → TF: def void2Bool(v: Void) = false Two last are vacuously identical. | () → ⊥: def u2Void = ??? () → (): def uID= {} () → TF: def u2True = True () → TF: def u2False = False |
TF → ⊥: def b2Nothing(b: Bool) = ??? TF → TF: def b2True(b: Bool) = True TF → TF: def boolId(b: Bool) = b | TF → (): def b2Unit(b: Bool) = {} TF → TF: def b2False(b: Bool) = False TF → TF: def boolNot(b: Bool) = !b |