Post #1846830
2026-04-27 22:52 UTC
@jpoiret @carloangiuli by the way, other branches of the thread pointed out that most of the motivations for “intensionality” of functions (like studying cost) are completely illusory. In a few POPL papers, my coauthors and I showed how you can study cost in terms of mathematical (extensional) functions very simply and elegantly, whereas nobody has ever managed to come up with a way to do so in terms of these illusory “intensional functions”.
This is one of those cases where I challenge anyone who thinks it is important that functions be intensional to give me literally one example of a positive thing you can do with that. This is separate from the point about terminology, of course.
Replies (1)
-
@mevenlennonbertrand@lipn.info 2026-04-28 06:28
@jonmsterling @jpoiret @carloangiuli Church Thesis, for synthetic computability theory. This is by now a well-installed topic, if maybe a bit niche, and imho a much more elegant way to formalise computability theory that all the other alternatives. Now I'm not saying that you should abandon funext in your standard mathematical life just to stay compatible with CT. But there is at least one non-hypothetical application for negating it.