5 ms·

> 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.

> 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.

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.