![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Dec. 24th, 2013
и ещё раз об одной полоумной бабке
Dec. 24th, 2013 07:35 amКоторая простила Тьюринга, что он был гей.
Могла бы и прощения попросить, между прочим.
Могла бы и прощения попросить, между прочим.
call/cc question
Dec. 24th, 2013 08:08 amRecently I saw a guy showing that call/cc is the function (natural transformation):
((X → Y) → X) → X
Any comments? Does it even exist? E.g. for Y=0. etc.
There's a meetup called "Lambda Gets Fancy"; people write stuff like
"So far I've seen two kinds of examples where CH isomorphism was used to prove something useful. In the first kind of examples, a polymorphic lambda-calculus was used or implicitly intended. For instance, you can prove that the sum and product types cannot be defined through lambda-calculus, you can prove that there cannot be a function with type alpha -> beta fully polymorphic in alpha and beta, and so on. These proofs all involve statements about polymorphic lambda-calculus."
Which looks pretty weird to me; half of it looks totally wrong to me - but I may be wrong as well.
((X → Y) → X) → X
Any comments? Does it even exist? E.g. for Y=0. etc.
There's a meetup called "Lambda Gets Fancy"; people write stuff like
"So far I've seen two kinds of examples where CH isomorphism was used to prove something useful. In the first kind of examples, a polymorphic lambda-calculus was used or implicitly intended. For instance, you can prove that the sum and product types cannot be defined through lambda-calculus, you can prove that there cannot be a function with type alpha -> beta fully polymorphic in alpha and beta, and so on. These proofs all involve statements about polymorphic lambda-calculus."
Which looks pretty weird to me; half of it looks totally wrong to me - but I may be wrong as well.
