> > I think John means 'dependent' in the more prosaic C++ sense of 'dependent on generic type parameters', e.g. 'Array<T>' inside a function generic on <T>, not dependent types in the Coq/Agda/Idris sense. Thanks for the clarification. Makes sense now.