Browse thread
Why doesn't ocamlopt detect a missing ; after failwith statement?
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2004-11-29 (00:02) |
From: | Jacques Garrigue <garrigue@m...> |
Subject: | Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement? |
From: Hendrik Tews <tews@tcs.inf.tu-dresden.de> > Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes: > > Note that void in C is definitely not zero. You cannot have variables > > C++ standard, 3.9.1.9: The void type has an empty set of values. ... > > So I would say void is zero. On the other side you have functions > returning void. Therefore I would conclude that the type theory > of C++ is unsound. Which is almost the same thing as saying that the definition contradicts itself... My point was just that, looking at the way void is used in C, it clearly does not have the usual proporties of zero, and among them the fact no function should be able to return zero, or that all pointers to void should be NULL. For this reason it seems to me at first that the actual semantics of void in C is that of (\exists a. a) aka unit (i.e. a value we know nothing about), not that of (\forall a.a) aka zero (the impossibility). You can safely cast any pointer to a void pointer, but not the opposite. Additionaly, for representation reasons, you cannot copy or allocate values of type void, so that they are non-existent in practice, but this looks more like a consequence than a definition. Another meaning of void seems to be the empty product, which again is unit, with the extract constraint that you cannot store such a value in C. This is just my personal take on the question. I just don't think that there is any serious model theory behind C's void, just a bunch of practical constraints. Jacques Garrigue