Comment by gettingoverit | Hacker News Reader

Comment by gettingoverit | Hacker News Reader

Parent Full thread

That's because you can consider categories of preorders and formulas where these operators will be morphisms.

(b >= c) && (a >= b) -> (a >= c) is a composition.

The more interesting consequence is that function types and implications are different names for the same thing. This is a Curry-Howard-Lambek correspondence.

This means that in order to prove

(b -> c) -> (a -> b) -> (a -> c)

it's enough to implement a function

f g h x = g (h x)

Another consequence is that exponentiation a^b can be considered the same thing as b -> a.

a^(bc) = (a^b)^c

(b && c) -> a = c -> b -> a

Another consequence is that exponentiation a^b can be considered the same thing as b -> a.

In the case where a and b are not strictly boolean (supposing they are instead probabilities for example) you could even generalize it somewhat in terms of "pure" mathematical operations.

  double implies(double a, double b) {
    double dif = a - b;
    double abx = sqrt(dif * dif);
    return 1 + pow(0, abx - dif) - pow(1, abx + dif);
  }

Kind of silly, I know, but it does work.

Nice to know!

I thought about it in terms of cardinalities of types. If A and B are types with |A| and |B| values correspondingly, there are |B|^|A| possible functions A -> B.

Another funny thing is that if you consider

forall a. (a -> a) -> (a -> a)

the type of natural numbers (weird, I know, but basically we encode numbers in unary with number of times we compose (a -> a) to itself), then exponentiation on such numbers will be

a ^ b = b a

Reply on news.ycombinator.com