5 ms·

I think f: X->Y could be fairly thought of as labeling the function X->Y with f.

by kian 3y ago

yakubin 3y ago
X->Y is not a function. f is.
- kian 3y ago
  label the function going from X->Y would be how I was intending that to be read. I'm well aware that X->Y is a type signature ;)
OJFord 3y ago
f: X->Y means f maps an input from domain X (set of all real numbers, say) to output range Y (set of all positive real numbers, say, f could be 'abs'). I think you might be thinking it's LX.Y (L for lambda)? But consider X=Y, LX.X is the identity function, some f: X->X could be the identity function, but it could also be anything else that returns a value of the same type as its argument - it could be 'add1' in this example of X being the reals, for example.
- kian 3y ago
  I'm not quite sure why this seems to be so controversial, except for the light abuse of notation in my english. Saying that f: X->Y means f maps an input from domain X to output in range Y is to say that we are defining a function -- and labeling it f, since it could just as easily be labeled g and still be the same function. Defining is naming -- naming is labeling [with scope].
  - OJFord 3y ago
    It's not defining a function though, it's describing (by one aspect) a whole class of functions. Take: f: ints -> ints f can be 'add1', 'identity', 'double', etc. If you know that, and calling it 'defining a function' is just loose English (you didn't mean completely defining) then fine, but that's what's confusing people. It read to me like you thought it was equivalent to a function definition in code, X & Y described what would actually happen over different inputs, so I was just trying to explain, didn't mean to offend if you knew already.
    - kian 3y ago
      Oooh, I see what you're saying. For want of an "s". Yes, in this context, I am aware that it is a whole class of functions -- and that f is a label being affixed to that class of functions. Sorry for the confusion -- that makes much more sense now. No offense received -- was just genuinely confused as to why it netted two comments and a few downvotes for a seemingly uncontroversial statement. But then again, we're talking mathematical logic here, so loose english is of course reasonably discouraged. Thanks for the clarification, and I hope you have a great evening!

I think f: X->Y could be fairly thought of as labeling the function X->Y with f.

by kian 3y ago

I think f: X->Y could be fairly thought of as labeling the function X->Y with f.

yakubin 3y ago

X->Y is not a function. f is.

kian 3y ago
label the function going from X->Y would be how I was intending that to be read. I'm well aware that X->Y is a type signature ;)

OJFord 3y ago

f: X->Y means f maps an input from domain X (set of all real numbers, say) to output range Y (set of all positive real numbers, say, f could be 'abs'). I think you might be thinking it's LX.Y (L for lambda)? But consider X=Y, LX.X is the identity function, some f: X->X could be the identity function, but it could also be anything else that returns a value of the same type as its argument - it could be 'add1' in this example of X being the reals, for example.

kian 3y ago
I'm not quite sure why this seems to be so controversial, except for the light abuse of notation in my english. Saying that f: X->Y means f maps an input from domain X to output in range Y is to say that we are defining a function -- and labeling it f, since it could just as easily be labeled g and still be the same function. Defining is naming -- naming is labeling [with scope].
- OJFord 3y ago
  It's not defining a function though, it's describing (by one aspect) a whole class of functions. Take: f: ints -> ints f can be 'add1', 'identity', 'double', etc. If you know that, and calling it 'defining a function' is just loose English (you didn't mean completely defining) then fine, but that's what's confusing people. It read to me like you thought it was equivalent to a function definition in code, X & Y described what would actually happen over different inputs, so I was just trying to explain, didn't mean to offend if you knew already.
  - kian 3y ago
    Oooh, I see what you're saying. For want of an "s". Yes, in this context, I am aware that it is a whole class of functions -- and that f is a label being affixed to that class of functions. Sorry for the confusion -- that makes much more sense now. No offense received -- was just genuinely confused as to why it netted two comments and a few downvotes for a seemingly uncontroversial statement. But then again, we're talking mathematical logic here, so loose english is of course reasonably discouraged. Thanks for the clarification, and I hope you have a great evening!