From: Stefan Monnier <monnier@iro.umontreal.ca>
To: Lars Magne Ingebrigtsen <larsi@gnus.org>
Cc: Reuben Thomas <rrt@sc3d.org>, 9222@debbugs.gnu.org
Subject: bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)
Date: Sun, 11 Sep 2011 00:56:51 -0400 [thread overview]
Message-ID: <jwvk49fsmyn.fsf-monnier+emacs@gnu.org> (raw)
In-Reply-To: <m3sjo3ycvj.fsf@stories.gnus.org> (Lars Magne Ingebrigtsen's message of "Sun, 11 Sep 2011 05:30:24 +0200")
> I was thinking more of functions that take void* as a parameter. What's
> usually expressed by that is "here's some memory that we're not actually
> telling you what the type of is explicitly", so it's (sort of) a pointer
> to something typeless. It's not a pointer to something of an empty
> type. :-)
That still fits within the definition of "unit type" to me: basically
the unit type is the type of everything (the set that contains all
possible values), and for that reason the type gives no information
about the value and you can't do anything with a value of that type
because you don't even know if it's an int or a struct so you can't even
begin to choose which kinds of operations might be applicable.
Again, in type theory, the void (aka empty) type is encoded typically as
"forall t . t" which means something like "this object has type t, no
matter what that t is" (kind of like the intersection of all types)
whereas the unit type is encoded as "exist t . t" which can be read as
"all I can say is that this object does have a type" (kind of
like the union of all types).
> So calling "void" a "typeless type" makes some sense. At least to me --
> in a C context.
It's still not typeless: it's just that the type you get gives you no
information about the data.
Stefan
next prev parent reply other threads:[~2011-09-11 4:56 UTC|newest]
Thread overview: 12+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-08-02 13:12 bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!) Reuben Thomas
2011-09-11 1:59 ` Lars Magne Ingebrigtsen
2011-09-11 3:25 ` Stefan Monnier
2011-09-11 3:30 ` Lars Magne Ingebrigtsen
2011-09-11 4:56 ` Stefan Monnier [this message]
2011-09-11 8:13 ` Reuben Thomas
2011-09-11 8:45 ` Andreas Schwab
2011-09-11 14:38 ` Drew Adams
2011-09-12 12:39 ` Stefan Monnier
2019-10-14 16:08 ` Stefan Kangas
2019-10-14 19:01 ` Stefan Monnier
2019-10-14 19:38 ` Stefan Kangas
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=jwvk49fsmyn.fsf-monnier+emacs@gnu.org \
--to=monnier@iro.umontreal.ca \
--cc=9222@debbugs.gnu.org \
--cc=larsi@gnus.org \
--cc=rrt@sc3d.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/emacs.git
https://git.savannah.gnu.org/cgit/emacs/org-mode.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.