The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

In my opinion, it is a quite bad idea to suggest that, just because Coq 
has dependent types, they should be used to constrain sizes or shapes of 
everything where we can come up with a simple scheme for doing so.  
Newcomers will tend to get lost down rabbit holes, when they start off 
in that direction.  It also seems to be at least a pretty bad idea to 
encourage experts to use dependent types, rather than writing ML-style 
programs and proving things about them.  Almost all of the Coq projects 
I have been involved in have needed significant refactoring to remove 
dependent types that were included too eagerly in early stages.

On 12/17/2017 11:20 AM, Emilio Jesús Gallego Arias wrote:
> Adam Chlipala 
> <adamc AT csail.mit.edu>
>  writes:
>
> > In my opinion, it is a very handy feature to make out-of-the-box
> > vectors difficult to work with, since almost no one should be using
> > dependently typed vectors for anything.
> What should then the proper alternative recommended alternative for
> sized lists in the standard library?