Episode #125 of the Stack Overflow podcast is here. We talk Tilde Club and mechanical keyboards. Listen now

New answers tagged


The meaning of curry can be easier to be seen when the type signature is written as curry :: ((a, b) -> c) -> (a -> b -> c) that is, a function taking a single parameter of type (a, b) and yielding a result of type c is turned into a function taking two separate values of types a and b yielding the same result type c. We might define curry for ...


$C$-monoids and their variants is what you are looking for. You can find further references and an account of what is what in Martin Hyland's Towards a Notion of Lambda Monoid.


Well nevermind this has an easy answer. Let $r_n = \lambda x_1 ... x_n . \lambda p . p \: x_1 ... x_n$ Note that for $m < n$, $r_n\: A_1 ... A_m$ normalizes for any normal $A_1 ... A_m$. Then for any $f$, let $n$ be larger than the number of subterms in $f$. $f \:r_n$ normalizes, so therefore no $f$ exists which only normalizes for a specific input.


Here is a new paper that covers a similar topic. The idea is that by doing algebra in enriched categories (2-categories are like categories enriched in categories), you can talk about more fine grained semantic structure on the algebra. (I haven't read through the whole paper myself, but I know enough to see some of the ideas behind it.) The way it relates ...

Top 50 recent answers are included