Re:Existential Haskell
by epsilonclose on Thursday November 26, 2020 @07:09PM
(#25224463)
What do you mean by "functions are exponentials"?
[ Parent
| on HN ]
A function with type A -> B is essentially equivalent to an object of type B^A. I can give you some relatively intuition for the case that A is finite. Imagine B^|A|, this is a list of B elements with one for every element in A. You can therefore interpret it as the return value for every possible input. Therefore it uniquely defines a function A -> B!
The type of pairs is just the cartesian product. Therefore (A×B)->C ~ C^(A×B) = (C^B)^A ~ A->B->C.
If you find this sort of thing, you might be interested in category theory :)
Re:Existential Haskell
by epsilonclose on Friday November 27, 2020 @11:28AM
(#25230001)
Thank you for clarifying. I was familiar with the notation A^B for the set of all f: A -> B, but this seemed like something more (and it does appear to be).
Putting some links I looked at here to save someone a few seconds of Googling: https://en.wikipedia.org/wiki/Exponential_object https://ncatlab.org/nlab/show/exponential+object
I'm not sure if the notation you'd encountered differed, but in this case the equivalence is between A^B and B -> A (note the order).
Interestingly, every identity you learned in grade school algebra which involved only addition, multiplication, and exponentiation holds here as an isomorphism. It can be a fun exercise to write the functions that take you back and forth. For instance:
A^(B+C) = A^B * A^C
to: (Either b c -> a) -> (b -> a, c -> a)
to f = (f . Left, f . Right)
fro: (b -> a, c -> a) -> (Either b c -> a)
fro (f, g) = \case
Left b -> f b
Right c -> g cgoogle keyword: "exponential object"
("exponential function" clashes pretty badly ;) )
Re:Existential Haskell
by epsilonclose on Friday November 27, 2020 @11:28AM
(#25230012)
Thank you, that helped!