2 ms·
As long as you have ordered parameters, I'm not sure this is such a big issue. First, tuples are (morally, i.e. up to non-termination) associative in most reaso
by tel 12y ago
As long as you have ordered parameters, I'm not sure this is such a big issue. First, tuples are (morally, i.e. up to non-termination) associative in most reasonable languages, so the product/exponential adjunction can be shifted around however you like
-- all morally identical
a -> b -> c -> d
a -> (b -> c -> d)
a -> (b -> (c -> d))
(a, b) -> c -> d
(a, b, c) -> d
((a, b), c) -> d
(a, (b, c)) -> d
However, so long as you have parameter order (we're not allowed to commute our tuples, just reassociate nested tuples like ((a, b), c) <-> (a, (b, c)) and so on) then flip still morally works
flip (someFn :: (a, b, c) -> d)
:: (b, a, c) -> d
:: (b, a) -> c -> d
:: b -> a -> (c -> d)
The same story holds for partial evaluation. Of course, there have to be far more edge cases to handle all this tuple twiddling.
---
Really, I think it's pretty meaningful to blur the distinction between "curry (once)" and "curry repeatedly along with tuple reassociation". The later forms an equivalence class of function types which all have the same application behavior.
- tel 12y agoAlso to explain that strange "adjunction" comment, currying results from the notion that the things of type (a, b) -> c are exactly equivalent to the things of type a -> (b -> c) An adjunction (F, G) occurs when the things of type (F a -> c) are equivalent to things of type (a -> G c), so if we pick F x = (x, b) and G x = (b -> x) then we see that currying is an adjunction between (,b) and (b ->).
- evincarofautumn 12y agoOne intuition for this is that (a, b) is the product type (a × b) and the function arrow (a → b) corresponds to exponentiation (b^a), so you get the isomorphism for free from the identity c^(a × b) = (c^b)^a.