I've been reading about this thing called dependent types.

So for example imagine a function firstNPrimes(int n) which returns an array of length n. In other words the type it returned would be int[n]. (In normal programming languages without dependent types all we can say is it returns int[] where the type doesn't specify the array length.)

I'm not entirely sure how useful this is though. I suppose if you had a cross product:

int[3] Cross(int[3] A, int[3] B){..}

which only worked on 3 dimensional vectors then maybe the compiler could type check this and avoid pointer issues.

Are there any real practical uses of dependent types that would be useful in everyday programming? Or are they mainly just useful for abstract logic?

I've been reading about this thing called dependent types.

So for example imagine a function firstNPrimes(int n) which returns an array of length n. In other words the type it returned would be int[n]. (In normal programming languages without dependent types all we can say is it returns int[] where the type doesn't specify the array length.)

I'm not entirely sure how useful this is though. I suppose if you had a cross product (into which that first function could be sent as arguments):

int[3] Cross(int[3] A, int[3] B){..}

which only worked on 3 dimensional vectors then maybe the compiler could type check this and avoid pointer issues.

Are there any real practical uses of dependent types that would be useful in everyday programming? Or are they mainly just useful for abstract logic?