5 ms·

void is kind of strange in C, because it looks like an empty type, but it still behaves as though it has a single instance (a unit type). For example, a functio

void is kind of strange in C, because it looks like an empty type, but it still behaves as though it has a single instance (a unit type). For example, a function with an empty return type can’t return (it’d have to supply a value of it); a void function can. You can’t cast things to an empty type (otherwise you’d get a value of it), you can cast things to void. Void a unit type, not an empty type, it’s just a bad one.

formerly_proven 2y ago
It would be somewhat more cohesive and less weird if we'd argued that the "void" return type means that a return value cannot be constructed which is taken to mean that the function has no return value, and simply returns without providing a value.
- mananaysiempre 2y ago
  Try as I may, I can’t make sense of that. I’ve read something like it in books on C, but I still can’t. Maybe I’m infected with set theory too deeply. In my mind, a computation (a “function”) must either return a value or hang/crash. If it appears as though it returns a member of ∅, it must hang/crash, because there are no members of ∅. If it returns a member of the single-element set, [1], it can return one, there’s just no use inspecting it afterwards (you know what it is already). (For what it’s worth, if you use a prover-adjacent language such as Agda or Idris, this is exactly how things are going to work there.)
  - Joker_vD 2y ago
    > a computation (a “function”) must either return a value or hang/crash. It can also simply return control, without returning anything. It's equivalent to invoking a continuation with zero arguments. Do you allow for zero-argument functions, at least? Of course, if a function can't return no value whatsoever, you suddenly need new syntactical categories to support it: you need to prohibit using such functions in an expressions (only call statements are allowed), you need a way to return from such a function (naked "return", which is prohibited from taking any expressions), and it's also severely strains your generics/templates because you can't treat such functions uniformly etc.
    - lmm 2y ago
      > It can also simply return control, without returning anything. It's equivalent to invoking a continuation with zero arguments. Do you allow for zero-argument functions, at least? There's nothing weird about a function taking 0 arguments, any more than there's anything weird about a function taking 3 or 5 arguments. A function can't take an argument of type void, so functions shouldn't be allowed to return void either. > Of course, if a function can't return no value whatsoever, you suddenly need new syntactical categories to support it: you need to prohibit using such functions in an expressions (only call statements are allowed), you need a way to return from such a function (naked "return", which is prohibited from taking any expressions), and it's also severely strains your generics/templates because you can't treat such functions uniformly etc. Or you do what sensible languages do: all functions return a value (if they return at all), functions that don't want to return anything in particular can return a unit value but that value is just a normal value that behaves normally in expressions etc., you don't make naked return a special case (you can make it syntax sugar for "return unit" if you really want), and you can treat those functions uniformly in generics, much more easily than with C++ templates where you have to make special cases for void functions.
      - Joker_vD 2y ago
        I don't argue with any of that, you know. But we do have a historical (stupid in retrospect) split between functions and procedures, dating a-a-a-all the way back to ALGOL 60 at least.
    - shiandow 2y ago
      You encounter the same problem with zero argument functions. A function on a zero type would be unable to return any value, since there's no value you could apply it to. To have a function of zero arguments you should use the unit type (which means the function effectively picks out a single value). This is also related to how a function with multiple arguments is a function of the product type, and an empty product is 1 not 0.
      - Joker_vD 2y ago
  - formerly_proven 2y ago
    It doesn't make sense from a strict type and set theory point of view because it doesn't make sense from a strict type and set theory point of view. Neither C nor C++ are rigorous languages. We also have "void foo(void)" and here void takes on two entirely different meanings, while type theory would suggest this is a function that diverges if it were called, which you can't.
  - masfuerte 2y ago
    It's not a function. A C function "returning" void is just C's syntax for writing a procedure. C doesn't call it a procedure, but that's what it is semantically.
    - moefh 2y ago
      The distinction between "function" and "procedure" doesn't map very well to whether the return type is void in C's syntax: - On one hand, a lot of "functions" are actually procedures that just happen to return a value: think for example `write(2)`, which is clearly used for its side effect, not to compute how many bytes could be written -- even though that's what it returns. - On the other hand, you can have a "procedure" (i.e., a function "returning" void) that actually has no side effects other than storing a computed value in a specified location (e.g. void square(int x, int *ret) { *ret = x*x; }). That's clearly a function in the mathematical sense, even though it "returns void".
      - simiones 2y ago
        The difference between a function and a procedure is strictly whether they can be used as a value or not in the syntax of the language, not the semantics. A function is a subroutine that can be used as either a value or a statement, a procedure is a subroutine that can only be used as a statement. That is, if x = foo(); is valid syntax, then foo() is by definition a function. If x = foo(); is invalid syntax, then foo() is a procedure.
  - simiones 2y ago
    C functions (and in fact the "functions" of most mainstream programming languages) are not computations, they are algorithms. An algorithm doesn't necessarily have a result of any kind, at least not in the way that a (mathematical) function has. The result of the algorithm can be the state in which it leaves the World (e.g. an algorithm for cleaning a house doesn't have a return value, it changes the state of the house). In fact the traditional programming name for what we mostly call functions today was "(sub)routine" - you call a subroutine, and when it finishes, it returns to where it originally started. Consider also that at the assembly level (and below it), subroutines don't have return values, nor arguments. The program counter simply jumps to the beginning address of the subroutine, and the `return` instruction jumps back to the address right after that jump. The subroutine may read values from certain locations in memory, and possibly write some others back, but none of this is necessary or enforced in any way. C functions, and the corresponding keywords, are much closer to this conception of assembly subroutines than they are to the mathematical notions of functions or computations.
    - MobiusHorizons 2y ago
      The calling convention does say where to look for the return value. So in a sense the return value always exists, but would not be meaningful if the function has a void return type.
      - simiones 2y ago
        The calling convention is part of the abstraction, it's not part of the processor's logic. Different languages often have different calling conventions, on the same OS and processor family. Different OSs have different calling conventions for their system calls.
  - Measter 2y ago
    > (For what it’s worth, if you use a prover-adjacent language such as Agda or Idris, this is exactly how things are going to work there.) You don't even have to go that far, Rust supports this concept. The built-in empty type is called `!`, and cannot be constructed. It's partially unstable, and there's a bunch of things you can't do yet, but you can use it as a return type.
  - jerf 2y ago
    "If it appears as though it returns a member of ∅, it must hang/crash, because there are no members of ∅." If you want to go with math, think more group theory. I'm specifically thinking about how you can always create a monoid if you have an associative binary operation, because even if your associative binary operation doesn't have an identity element, you can just declare one. Similarly, if you have "functions" that "return nothing", you just declare that nothing right into existence. Then you can just think of the C language layer basically erasing away any attempt to examine that value returned behind the scenes, because as you say, why?
  - ackfoobar 2y ago
    > a prover-adjacent language No need to go that far, you just need an ML inspired language with subtyping. https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-nothing.html https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-nothing... https://www.scala-lang.org/api/2.13.6/scala/Nothing.html https://www.scala-lang.org/api/2.13.6/scala/Nothing.html https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-unit/ https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-unit/ https://www.scala-lang.org/api/2.13.6/scala/Unit.html https://www.scala-lang.org/api/2.13.6/scala/Unit.html
  - bregma 2y ago
    The word "function" in mathematics and the word "function" in C (and C++) are homonyms. Two words spelled the same and pronounced the same but with entirely different meanings. Any effort to conflate the two will just end in tragedy.

formerly_proven 2y ago

It would be somewhat more cohesive and less weird if we'd argued that the "void" return type means that a return value cannot be constructed which is taken to mean that the function has no return value, and simply returns without providing a value.

mananaysiempre 2y ago
Try as I may, I can’t make sense of that. I’ve read something like it in books on C, but I still can’t. Maybe I’m infected with set theory too deeply. In my mind, a computation (a “function”) must either return a value or hang/crash. If it appears as though it returns a member of ∅, it must hang/crash, because there are no members of ∅. If it returns a member of the single-element set, [1], it can return one, there’s just no use inspecting it afterwards (you know what it is already). (For what it’s worth, if you use a prover-adjacent language such as Agda or Idris, this is exactly how things are going to work there.)
- Joker_vD 2y ago
  > a computation (a “function”) must either return a value or hang/crash. It can also simply return control, without returning anything. It's equivalent to invoking a continuation with zero arguments. Do you allow for zero-argument functions, at least? Of course, if a function can't return no value whatsoever, you suddenly need new syntactical categories to support it: you need to prohibit using such functions in an expressions (only call statements are allowed), you need a way to return from such a function (naked "return", which is prohibited from taking any expressions), and it's also severely strains your generics/templates because you can't treat such functions uniformly etc.
  - lmm 2y ago
    > It can also simply return control, without returning anything. It's equivalent to invoking a continuation with zero arguments. Do you allow for zero-argument functions, at least? There's nothing weird about a function taking 0 arguments, any more than there's anything weird about a function taking 3 or 5 arguments. A function can't take an argument of type void, so functions shouldn't be allowed to return void either. > Of course, if a function can't return no value whatsoever, you suddenly need new syntactical categories to support it: you need to prohibit using such functions in an expressions (only call statements are allowed), you need a way to return from such a function (naked "return", which is prohibited from taking any expressions), and it's also severely strains your generics/templates because you can't treat such functions uniformly etc. Or you do what sensible languages do: all functions return a value (if they return at all), functions that don't want to return anything in particular can return a unit value but that value is just a normal value that behaves normally in expressions etc., you don't make naked return a special case (you can make it syntax sugar for "return unit" if you really want), and you can treat those functions uniformly in generics, much more easily than with C++ templates where you have to make special cases for void functions.
    - Joker_vD 2y ago
      I don't argue with any of that, you know. But we do have a historical (stupid in retrospect) split between functions and procedures, dating a-a-a-all the way back to ALGOL 60 at least.
  - shiandow 2y ago
    You encounter the same problem with zero argument functions. A function on a zero type would be unable to return any value, since there's no value you could apply it to. To have a function of zero arguments you should use the unit type (which means the function effectively picks out a single value). This is also related to how a function with multiple arguments is a function of the product type, and an empty product is 1 not 0.
    - Joker_vD 2y ago
- formerly_proven 2y ago
  It doesn't make sense from a strict type and set theory point of view because it doesn't make sense from a strict type and set theory point of view. Neither C nor C++ are rigorous languages. We also have "void foo(void)" and here void takes on two entirely different meanings, while type theory would suggest this is a function that diverges if it were called, which you can't.
- masfuerte 2y ago
  It's not a function. A C function "returning" void is just C's syntax for writing a procedure. C doesn't call it a procedure, but that's what it is semantically.
  - moefh 2y ago
    The distinction between "function" and "procedure" doesn't map very well to whether the return type is void in C's syntax: - On one hand, a lot of "functions" are actually procedures that just happen to return a value: think for example `write(2)`, which is clearly used for its side effect, not to compute how many bytes could be written -- even though that's what it returns. - On the other hand, you can have a "procedure" (i.e., a function "returning" void) that actually has no side effects other than storing a computed value in a specified location (e.g. void square(int x, int *ret) { *ret = x*x; }). That's clearly a function in the mathematical sense, even though it "returns void".
    - simiones 2y ago
      The difference between a function and a procedure is strictly whether they can be used as a value or not in the syntax of the language, not the semantics. A function is a subroutine that can be used as either a value or a statement, a procedure is a subroutine that can only be used as a statement. That is, if x = foo(); is valid syntax, then foo() is by definition a function. If x = foo(); is invalid syntax, then foo() is a procedure.
- simiones 2y ago
  C functions (and in fact the "functions" of most mainstream programming languages) are not computations, they are algorithms. An algorithm doesn't necessarily have a result of any kind, at least not in the way that a (mathematical) function has. The result of the algorithm can be the state in which it leaves the World (e.g. an algorithm for cleaning a house doesn't have a return value, it changes the state of the house). In fact the traditional programming name for what we mostly call functions today was "(sub)routine" - you call a subroutine, and when it finishes, it returns to where it originally started. Consider also that at the assembly level (and below it), subroutines don't have return values, nor arguments. The program counter simply jumps to the beginning address of the subroutine, and the `return` instruction jumps back to the address right after that jump. The subroutine may read values from certain locations in memory, and possibly write some others back, but none of this is necessary or enforced in any way. C functions, and the corresponding keywords, are much closer to this conception of assembly subroutines than they are to the mathematical notions of functions or computations.
  - MobiusHorizons 2y ago
    The calling convention does say where to look for the return value. So in a sense the return value always exists, but would not be meaningful if the function has a void return type.
    - simiones 2y ago
      The calling convention is part of the abstraction, it's not part of the processor's logic. Different languages often have different calling conventions, on the same OS and processor family. Different OSs have different calling conventions for their system calls.
- Measter 2y ago
  > (For what it’s worth, if you use a prover-adjacent language such as Agda or Idris, this is exactly how things are going to work there.) You don't even have to go that far, Rust supports this concept. The built-in empty type is called `!`, and cannot be constructed. It's partially unstable, and there's a bunch of things you can't do yet, but you can use it as a return type.
- jerf 2y ago
  "If it appears as though it returns a member of ∅, it must hang/crash, because there are no members of ∅." If you want to go with math, think more group theory. I'm specifically thinking about how you can always create a monoid if you have an associative binary operation, because even if your associative binary operation doesn't have an identity element, you can just declare one. Similarly, if you have "functions" that "return nothing", you just declare that nothing right into existence. Then you can just think of the C language layer basically erasing away any attempt to examine that value returned behind the scenes, because as you say, why?
- ackfoobar 2y ago
  > a prover-adjacent language No need to go that far, you just need an ML inspired language with subtyping. https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-nothing.html https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-nothing... https://www.scala-lang.org/api/2.13.6/scala/Nothing.html https://www.scala-lang.org/api/2.13.6/scala/Nothing.html https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-unit/ https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-unit/ https://www.scala-lang.org/api/2.13.6/scala/Unit.html https://www.scala-lang.org/api/2.13.6/scala/Unit.html
- bregma 2y ago
  The word "function" in mathematics and the word "function" in C (and C++) are homonyms. Two words spelled the same and pronounced the same but with entirely different meanings. Any effort to conflate the two will just end in tragedy.