Talk:Unit type

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. — brighterorange (talk) 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 (talk • contribs) 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

What about this?

#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 at the nLab would make a nice addition to this article.99.153.64.179 (talk) 19:55, 26 June 2013 (UTC)

Bottom type or empty type?

In the line: "It should not be confused with the zero or bottom type, which allows no values and is the initial object in this category" should this not be referring to Empty type? Or is this a nuance of the category of types? --Gert7 (talk · contribs) 23:13, 14 December 2023 (UTC)

You're totally right! (I fixed it 2 hours ago, along other confusions between bottom and empty types.) — Ethaniel (talk) 08:21, 17 January 2024 (UTC)