The Coq mailing list

[Xuanrui Qi <xqi01 AT cs.tufts.edu>]

Adding to Adam's comment:

> There should be a high standard of justification for any 
> explicit dependent types (which are sometimes the right tool for a 
> job).  It tends to be painful to define and reason about such
> programs.  
> Experts generally avoid it.

Adam is definitely the expert here, and his words are very true. 

I tend to use dependent types in Coq when (1) I want to encode
something using dependent types (usually just a type indexed by a few
nat's) and (2) the invariants are too complex to prove without tactics.

Subset types are difficult to reason with even with `Program Fixpoint`
or `Function`! Sometimes, you can't even define the functions you want
with `Program Fixpoint`, which makes it just a total mess. There are
various workarounds (like defining your program using tactics), but
it's totally not worth the trouble to get into, unless absolutely
necessary.

Besides, if you want a certified ML program, dependent types will
extract to really dirty code with `Obj.magic` everywhere, which is not
ideal. So, Coq is really not designed for dependently-typed programming
(although you can do it), and avoiding it would be the wise thing to
do. In my opinion, this is a serious flaw in the design Coq.

-Ray 

On Sat, 2018-12-08 at 20:57 +0100, Klaus Ostermann wrote:
> Hi Adam,
> > It actually isn't idiomatic to program with subset types in Coq! I
> > recommend avoiding explicit dependently typed programming whenever
> > possible.  There should be a high standard of justification for any
> > explicit dependent types (which are sometimes the right tool for a
> > job).  It tends to be painful to define and reason about such
> > programs.  Experts generally avoid it.
> > 
> thanks for your advice. I actually guessed that much by now. However,
> my
> intention here was to experience and understand the nature of the
> pain :)
> 
> Klaus