6 ms·

Are void functions not considered functions in functional programming? I guess in math they're not. Functions have to have a codomain and map some things into

Are void functions not considered functions in functional programming? I guess in math they're not. Functions have to have a codomain and map some things into it.

brianberns 6y ago
> Are void functions not considered functions in functional programming? There's usually a "Void" type that's inhabited by a single value to handle that case. In a void function, all inputs are mapped to that value.
- kazinator 6y ago
  In C and C++, where this void kludge from, the void type is an incomplete type which cannot be completed and contains no values.
- ramshorns 6y ago
  Cool. So `void f (double a, double b)` is like `f : R^2 -> R^0`, where R^0 is a singleton set.
- lokedhs 6y ago
  Kotlin made this explicit by calling the void type Unit, where it is a class that has a single instance with the same name. So when you define a function: fun foo(a: Int): Unit { ... } You can actually assign a value to the result: val x = foo() // x now contains the value Unit There is another type which does not have any instances, called Nothing. Declaring a function to return Nothing indicates that the function will never return. Other than that, Nothing is a regular type, but code that uses it will be unreachable (and flagged as such by the IDE) because you can never create an instance of it. fun foo(): Nothing { throw SomeException() } This leads me to the question. Unit is obviously the mathematical Unit type, but is there a way to model the Nothing type in mathematically?
  - Tyr42 6y ago
    Yeah, it's called Bottom (⊥) fun foo(): ⊥ { return foo(); } In Rust it's called !, and you can write fn will_panic() -> ! { panic!("uh oh"); } This is actually useful for some embedded systems, where the main function isn't allowed to return, and gets declared with the Nothing / Bottom / ! type. The compiler is also smart enough to say that an infinite loop has type !, so you can have fn main() -> ! { let setup = ...; loop { blink_led(); sleep(100); } } and it'll complain if you put a break statement in the loop.
Jtsummers 6y ago
Regarding terminology, this is something I find frustrating in some languages. C functions aren't all functions. Java's methods aren't really all methods on objects (is it really accurate to call a static method, which is called using the class name and not an object instance, a method?). Some languages do make these distinctions, though. Playing around with SPARK/Ada at home lately, it makes a strong distinction between procedures (no return) and functions (have a return value). Procedures look like: procedure Put_Line (A : Integer) is begin Put(A); New_Line; end Put_Line; Functions look like: function Square (A : Integer) return Integer is begin return A * A; end Square; Similarly, in Common Lisp there's a clear distinction between functions and methods (really multimethods) by way of how they're declared. Functions are singular, have no multiple dispatch based on type, where as you can have many implementations of the same method dispatched on type. Though, again, a function may not really be a function and could be more accurately called a procedure. However, it probably makes sense for most people to think of everything as functions or everything as methods. At least it doesn't leave them asking "Which syntax do I use to declare this?"
- kazinator 6y ago
  In Common Lisp, methods are the bits of code which specialize a generic function. defgeneric most certainly defines a function. The symbol becomes fbound and can be used like function: (mapcar #'mygeneric ....) and so on. defmethod defines specializations for it. If you write a defmethod without a matching defgeneric, then the generic function gets implicitly defined.
- touisteur 6y ago
  I almost burned all my Ada books, my Ada-u-akbar t-shirt, my 'in strong typing we trust' Lady Lovelace medallion, when 'they' added the 'in out' access mode to functions in AdaFucking2005. I mean you wait ten years and then add 'that'? Y'all are going to PL HELL for that...
  - Jtsummers 6y ago
    For others, here's [0] the Ada rationale writeup on this. I suppose because I've been trying to learn SPARK more than Ada proper, this hasn't bitten me. Since SPARK's version of functions are closer to pure functions. But reading the rationale, I sort of get why they did it. Functions were already impure, but couldn't be marked as explicitly changing their inputs (access types could be altered and you'd never know by the function signature), so changing it to allow explicit `in out` parameters made some sense (as the Ada language has a preference for more explicit rather than implicit behavior). Though that kind of defeats my case since I used Ada as an example, and its functions may as well be procedures. [0] https://www.adaic.org/resources/add_content/standards/05rat/html/Rat-9-3-9.html https://www.adaic.org/resources/add_content/standards/05rat/...
Jweb_Guru 6y ago
void is the unit type, which has a single inhabitant, so those functions have a codomain; you can think of the unit type as the set containing the empty set. Sure, you don't explicitly write a return statement in C for `void` functions, but as long as the function still terminates, it can still be thought of as producing a value. Admittedly, not a very useful one, since all having a value of type void tells you is that whatever function produced it completed, but that mostly reflects the fact that `void` functions generally do other non-functional stuff; there's nothing inherently wrong with returning or having such a value, and it can be quite useful for generic code. For example, a map from keys to unit can be used to implement a set "for free." Even in non-generic, purely functional code, the unit type is still useful--as the domain for a constant function! In most C-like languages, this is of course just represented by a function that takes no arguments, but type theoretically it's equivalent to taking a single void argument (or any number of void arguments, of course, since the Cartesian product of two sets with one inhabitant produces another set with one inhabitant). In strict functional languages that insist that everything has a type, you will often use this encoding explicitly, to implement thunks (call-by-name evaluation). In partial languages (aka every language you're likely to practically use) or total languages which have the principle of explosion (which covers most of the remaining languages in existence), there is also the bottom type (the empty set) which has no inhabitants; this represents falsity or impossibility, which is computationally meaningful as a (perhaps not terribly informative) type for programs that can't return a value; for instance, nonterminating ones, or ones that always throw an exception. However, since in general you shouldn't be able to produce a closed value of that type, it can usually be freely cast to any other type you want, so many languages lack explicit syntax for it. That said, it can still be convenient at times to have a way of explicitly talking about the empty type; for example, in Rust (behind a feature flag currently), if you use a sum type where all but one of the variants includes the bottom type `!`, the compiler will recognize that only one variant is possible, and allow you to directly extract data from the inhabited variant (and can optimize out the tag, or at least that's the intent). This is useful when writing generic code that has to implement an API that returns (for instance) a `Result<T, E>`, but your implementation doesn't have an error condition; in such cases, you can set `E = !`. In total, dependently typed languages with the principle of explosion (which are certainly functional!), the type is also useful for another reason; a function from A to False is the equivalent (constructively anyway) of the negation of A, `~A`. Therefore, False ends up getting used quite a lot in type-level expressions, for the same reason as tests against the empty set occur a lot in set theory; even though strictly speaking you shouldn't be able to produce a closed value of type False (or else you should file a bug), when you're doing proofs by contradiction you can end up with one due to some false assumption in your context (which you can immediately use to prove that anything you wish derives from that context; this can be particularly useful to discharge impossible arms of pattern match expressions). This also happens implicitly in languages that perform flow-sensitive analysis of pattern match expressions; if they detect that one arm never returns (e.g. because it throws an exception or runs a loop that clearly doesn't terminate) they can implicitly assign it the bottom type, which can then be automatically cast to the type of the full expression. In short: not only are function types with void (and even empty!) domain and codomain functional, they are actually remarkably useful :) In fact, they are so fundamental, that almost all of (standard) dependent type theory can be constructed from just three base types: the empty type, the unit type, and bool! It's a bit unfortunate that two of these three fundamental types don't have direct syntax in a lot of languages, but as you can see this is mostly because they are so ubiquitous that they are largely hidden within other language features.

Are void functions not considered functions in functional programming? I guess in math they're not. Functions have to have a codomain and map some things into it.

brianberns 6y ago

> Are void functions not considered functions in functional programming? There's usually a "Void" type that's inhabited by a single value to handle that case. In a void function, all inputs are mapped to that value.

kazinator 6y ago
In C and C++, where this void kludge from, the void type is an incomplete type which cannot be completed and contains no values.
ramshorns 6y ago
Cool. So `void f (double a, double b)` is like `f : R^2 -> R^0`, where R^0 is a singleton set.
lokedhs 6y ago
Kotlin made this explicit by calling the void type Unit, where it is a class that has a single instance with the same name. So when you define a function: fun foo(a: Int): Unit { ... } You can actually assign a value to the result: val x = foo() // x now contains the value Unit There is another type which does not have any instances, called Nothing. Declaring a function to return Nothing indicates that the function will never return. Other than that, Nothing is a regular type, but code that uses it will be unreachable (and flagged as such by the IDE) because you can never create an instance of it. fun foo(): Nothing { throw SomeException() } This leads me to the question. Unit is obviously the mathematical Unit type, but is there a way to model the Nothing type in mathematically?
- Tyr42 6y ago
  Yeah, it's called Bottom (⊥) fun foo(): ⊥ { return foo(); } In Rust it's called !, and you can write fn will_panic() -> ! { panic!("uh oh"); } This is actually useful for some embedded systems, where the main function isn't allowed to return, and gets declared with the Nothing / Bottom / ! type. The compiler is also smart enough to say that an infinite loop has type !, so you can have fn main() -> ! { let setup = ...; loop { blink_led(); sleep(100); } } and it'll complain if you put a break statement in the loop.

Jtsummers 6y ago

Regarding terminology, this is something I find frustrating in some languages. C functions aren't all functions. Java's methods aren't really all methods on objects (is it really accurate to call a static method, which is called using the class name and not an object instance, a method?). Some languages do make these distinctions, though. Playing around with SPARK/Ada at home lately, it makes a strong distinction between procedures (no return) and functions (have a return value). Procedures look like: procedure Put_Line (A : Integer) is begin Put(A); New_Line; end Put_Line; Functions look like: function Square (A : Integer) return Integer is begin return A * A; end Square; Similarly, in Common Lisp there's a clear distinction between functions and methods (really multimethods) by way of how they're declared. Functions are singular, have no multiple dispatch based on type, where as you can have many implementations of the same method dispatched on type. Though, again, a function may not really be a function and could be more accurately called a procedure. However, it probably makes sense for most people to think of everything as functions or everything as methods. At least it doesn't leave them asking "Which syntax do I use to declare this?"

kazinator 6y ago
In Common Lisp, methods are the bits of code which specialize a generic function. defgeneric most certainly defines a function. The symbol becomes fbound and can be used like function: (mapcar #'mygeneric ....) and so on. defmethod defines specializations for it. If you write a defmethod without a matching defgeneric, then the generic function gets implicitly defined.
touisteur 6y ago
I almost burned all my Ada books, my Ada-u-akbar t-shirt, my 'in strong typing we trust' Lady Lovelace medallion, when 'they' added the 'in out' access mode to functions in AdaFucking2005. I mean you wait ten years and then add 'that'? Y'all are going to PL HELL for that...
- Jtsummers 6y ago
  For others, here's [0] the Ada rationale writeup on this. I suppose because I've been trying to learn SPARK more than Ada proper, this hasn't bitten me. Since SPARK's version of functions are closer to pure functions. But reading the rationale, I sort of get why they did it. Functions were already impure, but couldn't be marked as explicitly changing their inputs (access types could be altered and you'd never know by the function signature), so changing it to allow explicit `in out` parameters made some sense (as the Ada language has a preference for more explicit rather than implicit behavior). Though that kind of defeats my case since I used Ada as an example, and its functions may as well be procedures. [0] https://www.adaic.org/resources/add_content/standards/05rat/html/Rat-9-3-9.html https://www.adaic.org/resources/add_content/standards/05rat/...

Jweb_Guru 6y ago

void is the unit type, which has a single inhabitant, so those functions have a codomain; you can think of the unit type as the set containing the empty set. Sure, you don't explicitly write a return statement in C for `void` functions, but as long as the function still terminates, it can still be thought of as producing a value. Admittedly, not a very useful one, since all having a value of type void tells you is that whatever function produced it completed, but that mostly reflects the fact that `void` functions generally do other non-functional stuff; there's nothing inherently wrong with returning or having such a value, and it can be quite useful for generic code. For example, a map from keys to unit can be used to implement a set "for free." Even in non-generic, purely functional code, the unit type is still useful--as the domain for a constant function! In most C-like languages, this is of course just represented by a function that takes no arguments, but type theoretically it's equivalent to taking a single void argument (or any number of void arguments, of course, since the Cartesian product of two sets with one inhabitant produces another set with one inhabitant). In strict functional languages that insist that everything has a type, you will often use this encoding explicitly, to implement thunks (call-by-name evaluation). In partial languages (aka every language you're likely to practically use) or total languages which have the principle of explosion (which covers most of the remaining languages in existence), there is also the bottom type (the empty set) which has no inhabitants; this represents falsity or impossibility, which is computationally meaningful as a (perhaps not terribly informative) type for programs that can't return a value; for instance, nonterminating ones, or ones that always throw an exception. However, since in general you shouldn't be able to produce a closed value of that type, it can usually be freely cast to any other type you want, so many languages lack explicit syntax for it. That said, it can still be convenient at times to have a way of explicitly talking about the empty type; for example, in Rust (behind a feature flag currently), if you use a sum type where all but one of the variants includes the bottom type `!`, the compiler will recognize that only one variant is possible, and allow you to directly extract data from the inhabited variant (and can optimize out the tag, or at least that's the intent). This is useful when writing generic code that has to implement an API that returns (for instance) a `Result<T, E>`, but your implementation doesn't have an error condition; in such cases, you can set `E = !`. In total, dependently typed languages with the principle of explosion (which are certainly functional!), the type is also useful for another reason; a function from A to False is the equivalent (constructively anyway) of the negation of A, `~A`. Therefore, False ends up getting used quite a lot in type-level expressions, for the same reason as tests against the empty set occur a lot in set theory; even though strictly speaking you shouldn't be able to produce a closed value of type False (or else you should file a bug), when you're doing proofs by contradiction you can end up with one due to some false assumption in your context (which you can immediately use to prove that anything you wish derives from that context; this can be particularly useful to discharge impossible arms of pattern match expressions). This also happens implicitly in languages that perform flow-sensitive analysis of pattern match expressions; if they detect that one arm never returns (e.g. because it throws an exception or runs a loop that clearly doesn't terminate) they can implicitly assign it the bottom type, which can then be automatically cast to the type of the full expression. In short: not only are function types with void (and even empty!) domain and codomain functional, they are actually remarkably useful :) In fact, they are so fundamental, that almost all of (standard) dependent type theory can be constructed from just three base types: the empty type, the unit type, and bool! It's a bit unfortunate that two of these three fundamental types don't have direct syntax in a lot of languages, but as you can see this is mostly because they are so ubiquitous that they are largely hidden within other language features.