Dependent types

So, why are you not using dependent types yet? Do you like your programs randomly crashing?

>>7

The idea is basically that types may depend on values, so you can have something like List 50 Int for the type of a list with 50 elements.

Then C got dependent types:
typedef int dependent_type[50];
dependent_type A;

That way you basically can't do things like int sussman[10]; sussman[90] = 100;

gcc -Wall -pipe -O3 dep.c
typedef int dependent_type[50];
dependent_type A;
#include <stdio.h>
int main(){A[90]=100;printf("%d",A[90]);;}
dep.c: In function ‘int main()’:
dep.c:4:16: warning: array subscript is above array bounds [-Warray-bounds]
int main(){A[90]=100;printf("%d",A[90]);;}