# Talk:Unit type

WikiProject Mathematics (Rated Start-class, Low-priority)
This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
 Start Class
 Low Priority
Field: Foundations, logic, and set theory
WikiProject Computer science (Rated Start-class, Mid-importance)
This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Start  This article has been rated as Start-Class on the project's quality scale.
Mid  This article has been rated as Mid-importance on the project's importance scale.
To-do list for Unit type:
 Here are some tasks awaiting attention: Expand : Clarify relation to void type (Pierce, TAPL)

## Void type

Isn't the statment about the void type being the unit type not true? If unit is a mathmatical type that allows only one value, then void would not meet this qualification because, as is stated in the page, it contains no values. --NotQuiteEXPComplete 03:03, 9 August 2006 (UTC)

In the page it is stated that C++ and others don't provide any way to access the value of void, rather than void doesn't have any value at all :) 150.254.31.52 13:11, 11 December 2006 (UTC)
Hmm if the void type didn't have a value, it would not be an "inhabited type", which means that it would be judgementally equivalent to false. But in most programming languages, 'void' is not a synonym for 'false'. So, from the theoretical type theory point of view, the Void type does have a single value, the void value. Right? 99.153.64.179 (talk) 19:37, 26 June 2013 (UTC)

## Clean

There are no () in Clean. ~~ —Preceding unsigned comment added by 91.124.209.143 (talk) 06:46, 3 December 2007 (UTC)

## `void` in C is a bottom type.

The C standard (ISO/IEC 9899:1999) states:

### 6.2.5 Types

[...]

19 The `void` type comprises an empty set of values; it is an incomplete type that cannot be completed.

So it is clearly a bottom type, not a unit type. I don't know how to fix this, as it is also about C++, C# and Java which I don't know. --Army1987 (talk) 10:01, 13 March 2008 (UTC)

I think that just means you can't have a variable of `void` type or something, which as mentioned in the article is not that important. Regardless of what it says, `void` is used where the unit type would mostly be used in other languages; for example, as the return type of functions that don't return anything. In type theory, it's not possible to have a function that returns the bottom type, because there are no values of this type for it to get from anywhere, so you could never write it (unless the function also took in an argument of the bottom type, but then nobody could ever call it). (The bottom type corresponds to "false" in Curry-Howard correspondence; and it is impossible to prove "x -> false" unless "x" was also false.) Evaluating something of the bottom type would produce an error, e.g. in Haskell, which is completely different from a function that doesn't return anything in C. --Spoon! (talk) 20:45, 23 August 2008 (UTC)

I also think this is wrong. It's of course true that if we translate ML or Haskell then `int -> unit` becomes `void (*)(int)`, but the C way of thinking says that this function does not return a value, not that it returns a trivial value. (I wouldn't call this the bottom type either, though. There are no values of type void, but that's not what it means in this case. You can't write `void x = f()`. The C family just has a complicated function call system where functions types comprise a list (possibly empty) of arguments and an optional return type, where the omission of a return type is written `void`.) C does have a unit type, though: `struct {}`. It is not commonly used. 05:39, 2 March 2009 (UTC)

I agree with this too. It struck me as wrong as well, and made the same reasoning. I'll fix the article. Pcap ping 18:20, 17 August 2009 (UTC)

Pierce in TAPL notes that `void` corresponds to the Unit type, while Bottom would correspond to function which cannot return, e.g. `abort` or a continuation.

Type theory Imperative languages Inhabitants Storage requirements
Unit `void` 1 log2 1 = 0 b
Bottom `__noreturn__` 0 log2 0 = not defined

Ruud 22:49, 18 May 2011 (UTC)

Yes, I agree. (void)0 is (the only) inhabitant of the type void,. Even though this type has some limitations in C and C++ compared to other types, it's a limited version of Unit, and has nothing to do with Bottom. So the article should be fixed either to say that void=Unit and that there are some limitations, or that void is not Unit, but it's close. Anyway, saying void=Bottom is wrong. — Preceding unsigned comment added by Poletti.marco (talkcontribs) 16:34, 14 July 2012 (UTC)
Yes, from the point of view of theoretical type theory, the C standard is badly worded. That is, a type without a value is an "uninhabited type", and all uninhabited types are judgementally equal to false. Since void in C isn't a synonym for false, it can't actually be uninhabited -- it does have a value, and the value is void. BTW, we need an article for judegment (type theory) or judgement (logic) or judgement (sequent calculus) or something like that ... 99.153.64.179 (talk) 19:43, 26 June 2013 (UTC)

## Someone is competing with my writing and I leave this for open discussion

http://en.wikipedia.org/w/index.php?title=Unit_type&diff=309807458&oldid=309758990 --124.78.228.114 (talk) 13:44, 27 August 2009 (UTC)

I replied on your talk page. Pcap ping 19:56, 27 August 2009 (UTC)

## "return"ing a void function

```#include <stdio.h>

void f(void)
{
puts("in f.");
}

void g(void)
{
puts("in g.");
return f();
}

int main(void)
{
g();
return 0;
}
```

It compiles on gcc (last time I checked), and it works as expected. -- 92.229.73.235 (talk) 07:01, 8 March 2010 (UTC)

## Theory of unit type

A nice theoretical presentation, similar to unit+type in nLab would make a nice addition to this article.99.153.64.179 (talk) 19:55, 26 June 2013 (UTC)