I can write a function (T) -> () for an arbitrary type T, but () -> (T) requires constructing a new T or returning a bottom value. Why is there a fundamental asymmetry here?
-
-
Replying to @slava_pestov
In the Curry-Howard correspondence function types correspond to implication. "_ implies true" is satisfied whether _ is satisfiable or not. "true implies _" depends on _
3 replies 2 retweets 67 likes
Replying to @jckarter @slava_pestov
This is the right answer :)
1:01 PM - 19 Feb 2019
0 replies
0 retweets
6 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.