Does C99 have dependent types?

[Johannes Schaub]

I was reading http://en.wikipedia.org/wiki/Dependent_type, and it made me
think why they are missing C99 from that list. It seems to have dependent
types:

int i = 4;
int a;
int (*p) = &a;

Am I wrong with that observation?

 

[Keith Thompson]

I was reading http://en.wikipedia.org/wiki/Dependent_type, and it made me
think why they are missing C99 from that list. It seems to have dependent
types:

int i = 4;
int a;
int (*p) = &a;

Am I wrong with that observation?

No, but I'm not at all surprised that the article doesn't mention C99.

A "dependent type" is "a type that depends on a value", according
to the article. There are a number of languages that support array
types whose bounds can be determined at run time; C99's VLAs are
just one example. I'd say that C99 supports one very restrictive
example of dependent types, but VLAs just don't provide enough
theoretical interest to be discussed in the context of, for example,
"higher order dependently typed polymorphic lambda calculus".

 

[Michael Press]

I was reading http://en.wikipedia.org/wiki/Dependent_type, and it made me
think why they are missing C99 from that list. It seems to have dependent
types:

int i = 4;
int a;
int (*p) = &a;

Am I wrong with that observation?

No, but I'm not at all surprised that the article doesn't mention C99.

A "dependent type" is "a type that depends on a value", according
to the article. There are a number of languages that support array
types whose bounds can be determined at run time; C99's VLAs are
just one example. I'd say that C99 supports one very restrictive
example of dependent types, but VLAs just don't provide enough
theoretical interest to be discussed in the context of, for example,
"higher order dependently typed polymorphic lambda calculus".

And the third paragraph:

"Deciding equality of dependent types in a program may
require computations. If arbitrary values are allowed
in dependent types, then deciding type equality may
involve deciding whether two arbitrary programs produce
the same result; hence type checking becomes undecidable."

Cool.