@pervognsen@mastodon.social @corbin@defcon.social i have a computer question—tagging per because the question was catalysed by a comment you made on the red website like a month ago, and corbin because i think you’re likeliest to have an answer if no one else does. a pair can be encoded as a dependent function type (viz. the comment in question https://lobste.rs/c/e8gib1). the thing i notice about that function is that it’s lower-order, where the other function encoding i know for pairs (church encoding) uses a higher-order function. but at the same time, the dependent function feels a bit like an interpreter for a vm with only two instructions (‘return left’ and ‘return right’). so it’s almost like a particular constrained higher-order function, where instead of actually passing in a function, you pass in a (suitably restricted and specialised) form of source code. (of course the dependent function encoding and the higher-order function encoding work very differently and do very different things! but at the end of the day they’re encoding the same concept, and can be interconverted and used in similar ways)
i feel like i see this kind of pattern come up a fair amount in general. feels like a bit of this in cps (which i’m thinking about here as something that can be applied selectively in interface design) and also continuations in general (see: first-class support for one-shot continuations in some languages, mainly intended for i/o scheduling, vs what we did in c making the continuations by hand). is there any kind of general isomorphism to be found here? maybe something between classes of higher-order functions and lower-order functions? or where dependent typing (or other expressive type system features) extends the expressivity of such an isomorphism (so that a larger class of higher-order functions have lower-order counterparts)? any lit references? is this actually just something extremely basic?