Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Exponential types are functions [1]. The type A -> B could be written B^A. Interestingly, if you take functions to be lookup tables, then that's related to the number of possible unique lookup tables. First, notice that the type A + B has |A| + |B| values, the type A × B has |A| + |B| values and then we can see that A -> B has |B|^|A| values by remembering that functions can be seen as binary relations with the property of being functional. This means that there are |B|^|A| possible unique functions. Try an example by counting the number of functions from the set { 0, 1 } to { 2, 3, 4 }. You will see that there are 3^2 = 9 possible unique functions.

1. https://en.wikipedia.org/wiki/Function_type



Interesting! Now I wonder what "tetrated" types correspond to [1]

[1] https://en.wikipedia.org/wiki/Tetration


Well, I don't know of any type theory that has that but you could make something up. C^(B^A) = (B^A) -> C = (A -> B) -> C. So you'd get nested higher-order monomorphic functions like if the base is A and the height |B| = 5 then the result of tetration would be (((A -> A) -> A) -> A) -> A. I don't really know what that means though. Maybe an expert Haskeller could recognize a pattern.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: