> Dependent types make all that stuff part of the type system, so now "list of 3 warehouse_t" and "list of 4 warehouse_t" are no longer equivalent. Dependent t

> Dependent types make all that stuff part of the type system, so now "list of 3 warehouse_t" and "list of 4 warehouse_t" are no longer equivalent. Dependent types allow you to make that stuff part of your type system. But of course, Idris (and any other dependently typed language) still has "List" as a datatype which does not encode the length as part of its type - and if it didn't, it would be trivial to define. And it's easy enough to convert between the two types, should there be any need to either increase or decrease the precision of your types at different points in your program, depending on the need. There may not be a need to know at a type level how many items are in your cart, but there's surely a value in knowing, for example, that sorting a list doesn't change the number of elements, or that matrix multiplication is well-defined. You may argue that merely having the capability to use dependent types will lead to people abusing and overcomplicating things - but somehow we're already doing a very good job overcomplicating things with much simpler languages, e.g. Java reflection magic, or Ruby metaprogramming, so I'm not sure the "we shouldn't give people the rope to hang themselves" argument is valid. This is a bit different from the monad example in that it's practically impossible to write Haskell without understanding monads, since you can't do IO without it.