I have a very confused question about programming. Is there an interpretation of arithmetic operations on types that goes beyond sum=or=either and product=and=pair? For example this paper proposes an interpretation of subtraction and division on types, but it seems a little strained to me.
A sub-question: which arithmetical operation corresponds to function types? On one hand, the number of functions from A to B is the cardinality of B raised to the power of the cardinality of A. That plays nicely with the interpretation of sum and product types in terms of cardinality, but doesn’t seem to play nicely with the logical interpretation, where “if A, and A implies B, then B”. For the logical interpretation to work, it seems that implication should correspond to division (B/A), not exponentiation (B^A).
Another sub-question: which arithmetical operation corresponds to negation? On one hand, the assertion that type A is uninhabited should probably correspond to 1-A, because “A is either inhabited or uninhabited” corresponds to A+(1-A)=1, which is trivially true. On the other hand, the assertion “A can’t be both inhabited and uninhabited at the same time” corresponds to A*(1-A), which doesn’t look like 0 to me. Something strange is going on here.
I have a very confused question about programming. Is there an interpretation of arithmetic operations on types that goes beyond sum=or=either and product=and=pair? For example this paper proposes an interpretation of subtraction and division on types, but it seems a little strained to me.
A sub-question: which arithmetical operation corresponds to function types? On one hand, the number of functions from A to B is the cardinality of B raised to the power of the cardinality of A. That plays nicely with the interpretation of sum and product types in terms of cardinality, but doesn’t seem to play nicely with the logical interpretation, where “if A, and A implies B, then B”. For the logical interpretation to work, it seems that implication should correspond to division (B/A), not exponentiation (B^A).
Another sub-question: which arithmetical operation corresponds to negation? On one hand, the assertion that type A is uninhabited should probably correspond to 1-A, because “A is either inhabited or uninhabited” corresponds to A+(1-A)=1, which is trivially true. On the other hand, the assertion “A can’t be both inhabited and uninhabited at the same time” corresponds to A*(1-A), which doesn’t look like 0 to me. Something strange is going on here.