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

New answers tagged

2

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 ...


3

$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.


4

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.


2

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