[lnkForumImage]
TotalShareware - Download Free Software
Confronta i prezzi di migliaia di prodotti.
Asp Forum
 Home | Login | Register | Search 


 

Forums >

comp.lang.c

Does C99 have dependent types?

Johannes Schaub (litb)

4/9/2011 10:41:00 PM

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

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

Am I wrong with that observation?

2 Answers

Keith Thompson

4/10/2011 1:50:00 AM

0

Johannes Schaub <schaub.johannes@googlemail.com> writes:
> I was reading http://en.wikipedia.org/wiki/Depe..., and it made me
> think why they are missing C99 from that list. It seems to have dependent
> types:
>
> int i = 4;
> int a[i];
> int (*p)[i] = &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".

--
Keith Thompson (The_Other_Keith) kst-u@mib.org <http://www.ghoti.ne...
Nokia
"We must do something. This is something. Therefore, we must do this."
-- Antony Jay and Jonathan Lynn, "Yes Minister"

Michael Press

4/11/2011 8:35:00 PM

0

In article <lnd3ku6fk9.fsf@nuthaus.mib.org>,
Keith Thompson <kst-u@mib.org> wrote:

> Johannes Schaub <schaub.johannes@googlemail.com> writes:
> > I was reading http://en.wikipedia.org/wiki/Depe..., and it made me
> > think why they are missing C99 from that list. It seems to have dependent
> > types:
> >
> > int i = 4;
> > int a[i];
> > int (*p)[i] = &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.

--
Michael Press