bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Reuben Thomas]

In semantic/bovine/c-by.el there’s the following description:

     ("void" summary "Built in typeless type: void")

Cute, but inaccurate: void is a type alright. I suggest changing
“typeless type” to “empty type”.


In GNU Emacs 23.3.50.2 (x86_64-unknown-linux-gnu, GTK+ Version 2.24.4)
 of 2011-06-16 on skwd
Windowing system distributor `The X.Org Foundation', version 11.0.11001000
Important settings:
  value of $LC_ALL: nil
  value of $LC_COLLATE: nil
  value of $LC_CTYPE: nil
  value of $LC_MESSAGES: nil
  value of $LC_MONETARY: nil
  value of $LC_NUMERIC: nil
  value of $LC_TIME: nil
  value of $LANG: en_GB.UTF-8
  value of $XMODIFIERS: nil
  locale-coding-system: utf-8-unix
  default enable-multibyte-characters: t

Major mode: Emacs-Lisp

Minor modes in effect:
  recentf-mode: t
  global-semanticdb-minor-mode: t
  global-semantic-idle-summary-mode: t
  show-paren-mode: t
  semantic-mode: t
  savehist-mode: t
  minibuffer-electric-default-mode: t
  iswitchb-mode: t
  icomplete-mode: t
  global-whitespace-mode: t
  global-auto-revert-mode: t
  desktop-save-mode: t
  mouse-wheel-mode: t
  file-name-shadow-mode: t
  global-font-lock-mode: t
  font-lock-mode: t
  blink-cursor-mode: t
  auto-encryption-mode: t
  auto-compression-mode: t
  column-number-mode: t
  line-number-mode: t
  transient-mark-mode: t

Recent input:
<down-mouse-1> <mouse-1> y <help-echo> C-x b f u n 
c s . c <return> C-x C-f C-g <help-echo> <help-echo> 
<down-mouse-1> <mouse-1> C-x C-f ~ / r e p o / e m 
a c s / l i s p / c e d <tab> s e m <tab> / b o v <tab> 
/ c - n b <tab> <backspace> b <tab> <backspace> <backspace> 
b <tab> <return> C-s t y p e l e s s C-a C-SPC C-n 
C-k C-_ M-x r e p o r t b <backspace> - e m a c s - 
b u g <return>

Recent messages:
Desktop: Can't load buffer c++config.h: Opening output file: permission denied, /usr/include/c++/4.5/x86_64-linux-gnu/bits/c++config_flymake.h
Note: file is write protected
Desktop: Can't load buffer dirent.h: Opening output file: permission denied, /usr/include/dirent_flymake.h
Lazy desktop load complete
Reverting buffer `funcs.c'.
Quit
Loading vc-bzr...done
Mark saved where search started
Mark set
Undo!

Load-path shadows:
/home/rrt/.emacs.d/elpa/dictionary-1.8.7/dictionary-init hides /usr/local/share/emacs/23.3.50/site-lisp/dictionary-el/dictionary-init
/home/rrt/.emacs.d/elpa/dictionary-1.8.7/dictionary hides /usr/local/share/emacs/23.3.50/site-lisp/dictionary-el/dictionary
/home/rrt/.emacs.d/elpa/dictionary-1.8.7/link hides /usr/local/share/emacs/23.3.50/site-lisp/dictionary-el/link
/home/rrt/.emacs.d/elpa/dictionary-1.8.7/connection hides /usr/local/share/emacs/23.3.50/site-lisp/dictionary-el/connection
/home/rrt/local/share/emacs/site-lisp/dict hides /usr/local/share/emacs/23.3.50/site-lisp/emacs-goodies-el/dict
/usr/share/emacs-snapshot/site-lisp/ruby1.8-elisp/ruby-mode hides /usr/local/share/emacs/23.3.50/lisp/progmodes/ruby-mode
/usr/local/share/emacs/23.3.50/site-lisp/auctex/tex-style hides /usr/share/emacs/site-lisp/auctex/tex-style
/usr/local/share/emacs/23.3.50/site-lisp/auctex/tex-mik hides /usr/share/emacs/site-lisp/auctex/tex-mik
/usr/local/share/emacs/23.3.50/site-lisp/auctex/multi-prompt hides /usr/share/emacs/site-lisp/auctex/multi-prompt
/usr/local/share/emacs/23.3.50/site-lisp/auctex/tex-jp hides /usr/share/emacs/site-lisp/auctex/tex-jp
/usr/local/share/emacs/23.3.50/site-lisp/auctex/tex-info hides /usr/share/emacs/site-lisp/auctex/tex-info
/usr/local/share/emacs/23.3.50/site-lisp/auctex/latex hides /usr/share/emacs/site-lisp/auctex/latex
/usr/local/share/emacs/23.3.50/site-lisp/auctex/tex hides /usr/share/emacs/site-lisp/auctex/tex
/usr/local/share/emacs/23.3.50/site-lisp/auctex/texmathp hides /usr/share/emacs/site-lisp/auctex/texmathp
/usr/local/share/emacs/23.3.50/site-lisp/auctex/context-nl hides /usr/share/emacs/site-lisp/auctex/context-nl
/usr/local/share/emacs/23.3.50/site-lisp/auctex/tex-font hides /usr/share/emacs/site-lisp/auctex/tex-font
/usr/local/share/emacs/23.3.50/site-lisp/auctex/toolbar-x hides /usr/share/emacs/site-lisp/auctex/toolbar-x
/usr/local/share/emacs/23.3.50/site-lisp/auctex/tex-buf hides /usr/share/emacs/site-lisp/auctex/tex-buf
/usr/local/share/emacs/23.3.50/site-lisp/auctex/tex-fptex hides /usr/share/emacs/site-lisp/auctex/tex-fptex
/usr/local/share/emacs/23.3.50/site-lisp/auctex/bib-cite hides /usr/share/emacs/site-lisp/auctex/bib-cite
/usr/local/share/emacs/23.3.50/site-lisp/auctex/context-en hides /usr/share/emacs/site-lisp/auctex/context-en
/usr/local/share/emacs/23.3.50/site-lisp/auctex/tex-fold hides /usr/share/emacs/site-lisp/auctex/tex-fold
/usr/local/share/emacs/23.3.50/site-lisp/auctex/tex-bar hides /usr/share/emacs/site-lisp/auctex/tex-bar
/usr/local/share/emacs/23.3.50/site-lisp/auctex/context hides /usr/share/emacs/site-lisp/auctex/context
/usr/local/share/emacs/23.3.50/site-lisp/auctex/font-latex hides /usr/share/emacs/site-lisp/auctex/font-latex

Features:
(shadow sort mail-extr message sendmail ecomplete rfc822 mml mml-sec
password-cache mm-decode mm-bodies mm-encode mailcap mail-parse rfc2231
rfc2047 rfc2045 qp ietf-drums mailabbrev nnheader gnus-util netrc
time-date mm-util mail-prsvr gmm-utils mailheader canlock hashcash
mail-utils emacsbug multi-isearch vc-bzr sha1 hex-util
semantic/bovine/make semantic/bovine/make-by make-mode semantic/bovine
semantic/db-typecache semantic/find semantic/tag-file eldoc
semantic/db-file cedet-files semantic/bovine/c semantic/decorate/include
semantic/db-find semantic/db-ref semantic/bovine/c-by semantic/lex-spp
semantic/bovine/gcc semantic/dep semantic/analyze semantic/sort
semantic/scope semantic/analyze/fcn inform-mode vc-git face-remap
filladapt flyspell completing-help recentf tree-widget wid-edit
semantic/mru-bookmark semantic/db-mode semantic/db eieio-base
semantic/idle semantic/format semantic/ctxt semantic/decorate/mode
semantic/tag-ls semantic/decorate pulse uniquify warnings paren
semantic/util-modes semantic/util semantic semantic/tag semantic/lex
semantic/fw eieio byte-opt bytecomp byte-compile mode-local cedet
savehist minibuf-eldef iswitchb icomplete whitespace autorevert time
desktop cus-start cus-load server ropemacs pymacs php-mode etags
cc-langs cc-mode cc-fonts cc-menus cc-cmds cc-styles cc-align cc-engine
cc-vars cc-defs speedbar sb-image ezimage dframe lua-mode regexp-opt
go-mode-load change-mode ffap ispell flymake compile comint ring
smart-quotes auto-dictionary-autoloads c-eldoc-autoloads
dictionary-autoloads diff-git-autoloads dired-isearch-autoloads
full-ack-autoloads guess-style-autoloads kill-ring-search-autoloads
magit-autoloads mv-shell-autoloads tumble-autoloads
http-post-simple-autoloads package reporter advice advice-preload
yasnippet help-fns derived edmacro kmacro easymenu assoc cl cl-19
muse-autoloads emacs-goodies-el emacs-goodies-custom
emacs-goodies-loaddefs easy-mmode preview-latex tex-site auto-loads
tooltip ediff-hook vc-hooks lisp-float-type mwheel x-win x-dnd
font-setting tool-bar dnd fontset image fringe lisp-mode register page
menu-bar rfn-eshadow timer select scroll-bar mldrag mouse jit-lock
font-lock syntax facemenu font-core frame cham georgian utf-8-lang
misc-lang vietnamese tibetan thai tai-viet lao korean japanese hebrew
greek romanian slovak czech european ethiopic indian cyrillic chinese
case-table epa-hook jka-cmpr-hook help simple abbrev loaddefs button
minibuffer faces cus-face files text-properties overlay md5 base64
format env code-pages mule custom widget hashtable-print-readable
backquote make-network-process dbusbind system-font-setting
font-render-setting gtk x-toolkit x multi-tty emacs)

-- 
http://rrt.sc3d.org/

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Lars Magne Ingebrigtsen]

Reuben Thomas <rrt@sc3d.org> writes:

> In semantic/bovine/c-by.el there’s the following description:
>
>      ("void" summary "Built in typeless type: void")
>
> Cute, but inaccurate: void is a type alright. I suggest changing
> “typeless type” to “empty type”.

I don't quite think that "empty type" is more meaningful than "typeless
type".  At least to me, "typeless type" makes more sense, even if it is
somewhat humorous.

-- 
(domestic pets only, the antidote for overdose, milk.)
  bloggy blog http://lars.ingebrigtsen.no/

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Stefan Monnier]

>> In semantic/bovine/c-by.el there’s the following description:
>> ("void" summary "Built in typeless type: void")
>> Cute, but inaccurate: void is a type alright. I suggest changing
>> “typeless type” to “empty type”.
> I don't quite think that "empty type" is more meaningful than "typeless
> type".  At least to me, "typeless type" makes more sense, even if it is
> somewhat humorous.

I beg to disagree: to a large extent, a type can be thought of as a set
of values.  So a type can be empty (meaning that there is no value of
that type).  But a "typeless type" is rather meaningless (in type
theory, types have themselves a type, so for example "1" has type "Int"
and "Int" has type "Type", but then a type can't be "typeless" since the
"definition" of a type is then basically "has type Type").


        Stefan


PS: Of course, in C the "void" type is more like the "unit" type than
like the empty type, i.e. a type with a single value which hence doesn't
carry any information.  E.g. a function that returns a type void can
return, tho its return value carries no information ("it returns
nothing") whereas a function that returns the empty type is a function
that will never return (since there is no value in the empty type, the
function can never return a value of the right type).

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Lars Magne Ingebrigtsen]

Stefan Monnier <monnier@iro.umontreal.ca> writes:

> PS: Of course, in C the "void" type is more like the "unit" type than
> like the empty type, i.e. a type with a single value which hence doesn't
> carry any information.  E.g. a function that returns a type void can
> return, tho its return value carries no information ("it returns
> nothing") whereas a function that returns the empty type is a function
> that will never return (since there is no value in the empty type, the
> function can never return a value of the right type).

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

So calling "void" a "typeless type" makes some sense.  At least to me --
in a C context.

-- 
(domestic pets only, the antidote for overdose, milk.)
  bloggy blog http://lars.ingebrigtsen.no/

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Stefan Monnier]

> 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

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Reuben Thomas]

On 11 September 2011 05:56, Stefan Monnier <monnier@iro.umontreal.ca> wrote:
>
> It's still not typeless: it's just that the type you get gives you no
> information about the data.

Moreover, in C, in which types are not first-class objects, no type
has a type, so every type is a typeless type.

I agree, BTW, that "unit type" is a better description of void than my
original "empty type".

-- 
http://rrt.sc3d.org

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Andreas Schwab]

Reuben Thomas <rrt@sc3d.org> writes:

> I agree, BTW, that "unit type" is a better description of void than my
> original "empty type".

Ceci n’est pas un type.

Andreas.

-- 
Andreas Schwab, schwab@linux-m68k.org
GPG Key fingerprint = 58CA 54C7 6D53 942B 1756  01D3 44D5 214B 8276 4ED5
"And now for something completely different."

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Drew Adams]

> Ceci n'est pas un type.

Ce type Andreas est le gagnant.

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Stefan Monnier]

>> It's still not typeless: it's just that the type you get gives you no
>> information about the data.
> Moreover, in C, in which types are not first-class objects, no type
> has a type, so every type is a typeless type.

Actually, you don't need types to be "first class objects" for them to
have a type.  From type theory's point of view, C types all have the
same type, which you could call "Type" or * or ω, i.e. the type
of types.  It's also often called a kind.

To be more precise, in C you could consider "struct" as a type-level
function which takes a descriptor and returns a type.  And "{ int a,b;
char c; }" would then be a structure-descriptor.  I.e.:

   struct has type "StructureDescriptor -> Type"
   { int a,b; char c; } has type "StructureDescriptor"

From that point of view "struct" is a valid expression in the type
language, but it does not describe a set of values: only types who
have type "Type" describe values.

> I agree, BTW, that "unit type" is a better description of void than my
> original "empty type".

From a theoretical point of view, yes, but most people are unfamiliar
with "unit type" and its name doesn't lend itself to a good intuitive
understanding of it.


        Stefan

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Stefan Kangas]

Stefan Monnier <monnier@iro.umontreal.ca> writes:

>>> In semantic/bovine/c-by.el there’s the following description:
>>> ("void" summary "Built in typeless type: void")
>>> Cute, but inaccurate: void is a type alright. I suggest changing
>>> “typeless type” to “empty type”.
>> I don't quite think that "empty type" is more meaningful than "typeless
>> type".  At least to me, "typeless type" makes more sense, even if it is
>> somewhat humorous.
>
> I beg to disagree: to a large extent, a type can be thought of as a set
> of values.  So a type can be empty (meaning that there is no value of
> that type).  But a "typeless type" is rather meaningless (in type
> theory, types have themselves a type, so for example "1" has type "Int"
> and "Int" has type "Type", but then a type can't be "typeless" since the
> "definition" of a type is then basically "has type Type").
>
>
>         Stefan
>
>
> PS: Of course, in C the "void" type is more like the "unit" type than
> like the empty type, i.e. a type with a single value which hence doesn't
> carry any information.  E.g. a function that returns a type void can
> return, tho its return value carries no information ("it returns
> nothing") whereas a function that returns the empty type is a function
> that will never return (since there is no value in the empty type, the
> function can never return a value of the right type).

This still says "typeless type" 8 years later, which makes no sense to
me either.

Since the C "void" type does not map perfectly to neither the unit
type nor the empty type, and also has the added confusion that "void*"
pointers are quite different from functions with return type "void",
perhaps we should just change it to:

    "Built in type: void"

That should avoid any confusion, yet be clear enough for any C programmer.

What do you think?

Best regards,
Stefan Kangas

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Stefan Monnier]

>     "Built in type: void"
>
> That should avoid any confusion, yet be clear enough for any C programmer.

Fine by me,


        Stefan

bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Stefan Kangas]

close 9222 27.1
quit

Stefan Monnier <monnier@iro.umontreal.ca> writes:

> Fine by me,

Thanks.  I've now done that on master in commit 6aa0e0c754 and I'm
closing this bug report.

Best regards,
Stefan Kangas