Hacker News Reader

Comment by ramshorns | Hacker News Reader

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.

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?"

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.

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

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

There's pragma pure and I sure would like it to be enforced and to allow lazy execution sometimes.

As for pointer types being undetectable on call sites I agree that it is annoying, but they could be hidden behind a private or limited private type so I'm not sure there's an easy way out. But I still feel this change was a lazy way to make some border cases 'nicer to look at' or 'easier to code' but not easier to read...

But don't take my word for it, I hate the dot notation with burning hatred... So...

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

In C and C++, where this void kludge from, the void type is an incomplete type which cannot be completed and contains no values.

Cool. So `void f (double a, double b)` is like `f : R^2 -> R^0`, where R^0 is a singleton set.

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?

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.

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.

> void is the unit type, which has a single inhabitant

Not in C. void is an incomplete type, with an empty domain. There is no value which is an instance of void.

The void type cannot be completed, and so there is no way to instantiate an object of void type. An object of type void cannot be defined or declared. There can be no array of void, nor a structure member of type void.

The void keyword in C and C++ just serves as a syntactic/semantic hack.

Casting an expression to (void) is a gesture which indicates that the value is deliberately being discarded (and is not an actual conversion).

A function declared as returning void returns nothing; and a return statement with a value must not be used in its body: even a value that has been cast to (void) type. Because, remember, that is not actually a conversion to a void type, and the function has no return type.

In ANSI C, (void) was introduced to distinguish the syntax of a declared-empty parameter list from that of an unspecified parameter list. That's a pure syntactic hack. It could easily have been something else, like (static) or (--).

There can be a pointer to void, and that is loaded with yet more hacks. Such a pointer can't be dereferenced or subject to arithmetic (that being possible is a GCC extension).

I enjoy pedantry too, so I guess I kind of understand why you keep making this point. However, it's not relevant to what the OP asked, which was about the mathematical modeling of C functions that return void, rather than trivia related to C syntax. In the two positions in C and C++ that I discussed, the domain and codomain of a function, void is functionally identical to unit, despite your protestations to the contrary (there is literally no semantic distinction between them). In Rust, none of these restrictions exist and we can freely use unit in all the ways you described, but in the domain and codomain of a function it still works just like void does in C (we can't cast from arbitrary types to void, but this is more because Rust takes a hard stance against stupid casts than because it would be difficult to implement, and it has other ways of representing deliberately throwing away a value).

The C standard, of course, may disagree, and claim that there is no value of type "void" and that void functions "have no return type." That I can call and successfully return from a void function, call a function taking void, and even cast a value to void, provide ample evidence (which would also be backed up by reading the standard) that what it means by "type" is not the same thing as what a mathematician means by "type" (and "completed" is a complete red herring here). The fact that you don't explicitly return a void value doesn't really mean anything--no return or return with no value are pure syntactic sugar for returning a void value, which is also how it's implemented in many other languages that enjoy explicit unit types.

What I can't do in C is bind one of the many values of type void to a variable (and do a few other things, like call `sizeof` on the type, or explicitly name the inhabitant of void as a literal, which again have pretty much nothing to do with the semantics of the thing). That is a much weaker restriction, for the same reason that defining a binding as `const` is much weaker than a guarantee that the underlying value isn't mutated; bindings are a largely syntactic artifact and don't affect the mathematical model of a C function in any way. This is especially true for unit types, since having an instance of one is completely uninformative as they both always exist and are all definitionally equal!

Of course, this doesn't apply to void * , which as you point out is really its own bizarre thing that is mostly unrelated to void itself (I'd like to call it a pointer to the top type, but I'm not certain even that would cover its semantics). I think it's fair to say that despite some degree of overlap, void * is an unrelated concept overloading the "void" keyword, and that the actual interpretation of bare "void" is indeed equivalent to unit, not that every other use of `void` in C is completely arbitrary and unprincipled. The reason, AFAIK, why C doesn't just add all those void-related features it's missing is because it has baked in decisions like "every type has a nonzero size" and "arrays are pointers" (conflicting with void * ) that make adding stuff like this after the fact very complicated, not because it wouldn't make sense semantically (in a proper semantic model, where void * was called something like any * and zero sized types were legal, many of these issues would go away, including--I'm pretty sure--all the reasons why C and C++ must insist that void values not be completed). In any case, none of this helps with or is relevant to reasoning about C functions as mathematical objects.

And just to be extra clear--even if C had no keyword at all for `void` functions and didn't have `void` as an option for argument lists, these functions would still be modeled as taking / returning values of type unit.

> What I can't do in C is bind one of the many values of type void to a variable

The type void has no values. It's similar to the nil type in Lisp (which also has no values), except that it doesn't form the bottom of a type spindle in terms of inheritance: whereas nil is the subtype of every other type including itself, void is no such thing.

The claim that void is a type which holds one element is like saying it's the null type/class of Common Lisp (which has one element, the object nil). That's a different beast.

> The C standard, of course, may disagree, and claim that there is no value of type "void"

Since there is actually such an abstract concept (a type with an empty set of values), the C definition holds water.

I just added Common Lisp to the Wikipedia page: https://en.wikipedia.org/wiki/Unit_type That kind of wrecks some of its claims.

The Wikipedia page on unit types is completely accurate with regards to what a unit type is, and a unit type is the correct model for the type that a void function returns in C. Sure, void can be interpreted in a few different ways, but void in function return or argument position definitely cannot be interpreted as the bottom type. As far as I know, C does not really have bottom as a first-class concept, however useful it might be. So while I agree with you that it would be theoretically possible for C's statement about void not having any inhabitants to coincide with the type theoretic defintion of void, in practice it does not (for all the reasons I mentioned earlier).

You will note that all the differences mentioned between void and unit in the Wikipedia article are syntactic, not semantic; this is because semantically there is no real distinction between them.

What is bizarre to me, though, is that you didn't read the Wikipedia article you just carelessly edited, which already mentions Common Lisp and explicitly tells you not to confuse the NULL type (which has single inhabitant NIL--i.e. you agree with me that it is the same as void, and they are both unit types) with the NIL type (bottom). Firstly, the existence of a subtyping relationship that lets you upcast values of type unit to values of type symbol (or indeed, any other type) does not somehow make it not a unit type (only subtyping in the other direction would accomplish such a thing), and certainly does not invalidate any of the article's claims as you assert. Secondly, no implementation detail of Common Lisp will affect the definition of a unit type, regardless of how many edits one makes to a Wikipedia page, any more than the C standard claiming void functions don't have a return type changes how they are modeled mathematically. Notions as fundamental as unit types are defined semantically and aren't really tied to specific language syntax.

Fun fact, in C++ void(); is a syntactically valid statement.

I think the best way to sum up the discussion is. void in c has no values. But the most straightforward way of modeling void mathematically is a type with one value.

A type with no values is not any less straightforward.

ISO C already provides a mathematical model, and one in which void is a type with no value.

Neither concept extends well to functions that return multiple values. The proper generalization which covers that case is that a function has an ordered list of return types. A function returning nothing has an empty such list: a zero-length list of return types.

Under this model, we don't require any unit type or bottom type or anything of the sort in connection with functions that don't return anything.

Note that this is similar to a parameter list: an empty return value list is similar to an empty parameter list, in which there are no parameters and hence no parameter types at all.

This model can be applied to single-value return languages like C, if we pretend that functions return multiple values, restricted to the zero or one plurality.

For what I hope is the last time, whatever the merits of a type with no values, that does not describe the semantics of void in argument and return position in C. ISO's definition is not relevant at all here, since they are using definitions specific to C rather than type-theoretic ones, and given that you haven't addressed any of the points I've made except to cite various standards bodies, I'm not really sure how else to explain this to you.

You are correct that it is possible to forego unit in exchange for defining vectors of length N as a fundamental type. This is the solution used by Rust, for example, in defining its tuple types, and in Rust indeed the empty tuple and unit are equivalent. Personally, I do not find this simpler than defining unit as a base type and pairing as a fundamental operation on types, since you are effectively just hiding the same cons/nil definition in the definition of natural numbers used for the list length. In any case, unit is not intended to automatically generalize to multiple types, and the rule for product types is a completely orthogonal feature that is useful by itself, so this seems like a bit of an aside. It also seems a bit pointless to introduce a general type like tuples of arbitrary length if you are going to restrict "arbitrary" to 0 or 1 (well, not pointless in some contexts, but in this one it seems strictly more complicated than just having a unit type, since any type you could use with a 1-tuple already has to exist in the first place).

I don't know why you assert that we don't need bottom under this model, however. A list of length zero is not the same as bottom, it is the same as unit (I believe you may have a fundamental misunderstanding about this?). To model bottom in an equivalent fashion, you would want a mechanism for defining sum types with N constructors--0 constructors represents bottom. And just like with the tuple case, this functionality is effectively equivalent to providing the bottom type plus a two-constructor sum type (although depending on the strength of your type theory, a more elaborate construction may be preferred, generally speaking you don't need to be able to define more than two constructors at a time).

Just to reiterate (and close the door on my end of this conversation): bottom and unit are not the same, and your proposed solution does not allow you to represent bottom. It allows you to represent void because void is not semantically bottom, it is semantically unit. I am extremely confident that whatever solution you come up with for representing void, whatever its individual merits, will either be interpretable as unit, or not reflect the actual semantics of C.

> void in argument and return position in C

void in the argument position in C is just a punctuation that was added by ANSI C to denote a prototyped empty parameter list. This is because () already had the meaning of "unspecified parameter list".

C++ fixed this issue from the beginning by banning the concept of an unspecified parameter lists and so initially it had no (void). In C++, () means "empty, fully declared parameter list". C++ added (void) for ANSI C compatibility.

Note that a parameter list like (void, void) or (void, int) and other possibilities is not allowed. It really is just a syntactic hack for that special case and not a parameter type declaration.

The (void) spelling could instead have used some other token. ANSI C could plausibly have chosen, say, the token sequence (!) to distinguish a prototyped empty parameter list from (). The shape is certainly available because (!) is a syntax error. Would ! then denote the unit type, even though it's not a type specifier?

> I don't know why you assert that we don't need bottom under this model, however.

That's nothing compared to the question of where I assert such a thing.

(Still, why would we need to represent a bottom type in describing a language that doesn't have it as a concept? It's handy for "internal use" in the model. Every type system should have a bottom type.)

> your proposed solution does not allow you to represent bottom

We can easily establish the existence of more than one empty type, and stipulate that they are all distinct and incompatible, even though their domain is the same empty set. So if we have used one such type U for a specific purpose which somehow makes it unsuitable as bottom, we can invent another type V very similar to it, and call that one bottom. We endow V (and only V) with the required property that it's the subtype of every type, including itself. Since U is not endowed that way, it's not the bottom type, but U does not hinder the existence of V in any way.

As long as we don't create a conflict in a system, giving rise to a contradiction, we are not prevented from adding anything.

I understand that if the role for U is to represent something like the C void, then it could be a unit type. A unit type will do everything we need in the model. Yet, it's not elegant; the unit type carries a useless value which has no manifestation in the system being modeled.

Reply on news.ycombinator.com