> For instance, the Vector type in Idris has two type parameters (not sure that's the correct term to use in this case): the first is the type of the element contained by the vector, and the second is the length of the vector.

In case anyone's wondering, only the first of these (the element type) is a type parameter, since it has a constant value in all sub-expressions (ie. the cons cells all contain elements of the same type).

The second is a 'type index', which is a more general term (type parameters are a special case of type indices), since its value changes in the sub-expressions (the cons cells have different lengths).

The difference is that we don't need to pattern-match parameters on every recursive call, since they're guaranteed to be constant (although we can if we like).

I didn't know this until I asked http://cs.stackexchange.com/questions/20100/what-are-the-dif...