The Coq mailing list

[mechvel AT scico.botik.ru]

On 2020-03-04 19:06, Ralf Jung wrote:
> My first guess would that this has something to do with the exponential 
> blow-up
> that I discussed in
> <https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html>.


It looks like this.
Following this paper, we can define a direct product of rings, denote it 
_*_,
and put
    G = Z * Z * Z * Z * Z * Z * Z * Z             (I)

for the ring Z for Integer.
And it may occur that this will be a hard type checking example for 
Agda.

If so, this will be just a toy example, Jason asked for.
This needs testing.

Thanks,

------
Sergei



> On 04.03.20 00:04, Jason Gross wrote:
> > I'm confused by this.  Are you saying that in Agda typechecking is 
> > exponential
> > in the number of files?  Or exponential in the number of nested 
> > abstractions? 
> > Or something else?  Do you have a toy example demonstrating this 
> > behavior?
> >
> > On Tue, Mar 3, 2020, 17:42 
> > <mechvel AT scico.botik.ru
> > <mailto:mechvel AT scico.botik.ru>>
> >  wrote:
> >
> >     On 2020-03-04 00:31, Jason Gross wrote:
> >     >> Which bottlenecks are you referring to? Are they intrinsically 
> > tied
> >     > to dependent types, or they are related to the treatment of
> >     > propositions and equality in systems such as Coq?
> >     >
> >     > The main bottleneck that I'm referring to here (though not the 
> > only
> >     > one of my thesis) is the one that is due to the fact that 
> > arbitrary
> >     > conversion problems can happen during typechecking.  This is 
> > used to
> >     > great advantage in proof by reflection (where all of the work is 
> > done
> >     > in checking that a proof of "true = true" has the type 
> > "some-check =
> >     > true").  But it also causes performance issues if you're not 
> > careful.
> >     > To take a toy example, consider two different definitions of
> >     > factorial: n! = n * (n - 1)!, and n! = (n - 1)! * n.  Suppose 
> > you have
> >     > two different ways of computing a vector (length-indexed list) 
> > of
> >     > permutations, one which defines the length in terms of the first
> >     > factorial, and the other one which defines the length in terms 
> > of the
> >     > second factorial.  Suppose you now try to prove that the two 
> > methods
> >     > give the same result on any concrete list of length of length 
> > 10.
> >     > Just to check that this goal is valid, Coq is now trying to 
> > compute
> >     > 10! as a natural number.  This example is a bit contrived, but 
> > less
> >     > egregious versions of this issue abound, and when doing verified
> >     > engineering at scale, these issues can add up in hard-to-predict 
> > ways.
> >     >  I have a real-world example where changing the input size just 
> > a
> >     > little bit caused `reflexivity` to take over 400 hours, rather 
> > than
> >     > just a couple of minutes.
> >     >
> >     > On Tue, Mar 3, 2020, 16:00 Viktor Kunčak 
> > <vkuncak AT gmail.com
> >     
> > <mailto:vkuncak AT gmail.com>>
> >  wrote:
> >     >
> >     >> I would be also curious to hear answers to this questions!
> >     >> ("Lots of people do it" seems like a very compelling answer.)
> >     >>
> >     >> Which bottlenecks are you referring to? Are they intrinsically 
> > tied
> >     >> to dependent types, or they are related to the treatment of
> >     >> propositions and equality in systems such as Coq?
> >     >>
> >
> >     There is a problem of the type checking cost in Agda, and probably 
> > in
> >     Coq too.
> >     I do not know of whether it is fundamental or technical. And I 
> > have not
> >     seen an answer to this question, so far. On practice, it looks 
> > like
> >     this:
> >     Agda can type-check only a small part of the computer algebra 
> > library of
> >     methods (with full proofs). With implementing it further, with
> >     increasing the hierarchy level of parameterized modules, the type
> >     check cost seems to grow exponentially in the level.
> >     So, after implementing in Agda an average textbook on computer 
> > algebra
> >     (where is known a constructive proof for each statement), say, of 
> > 500
> >     pages, it will not be type-checked in 100 years.
> >
> >     Probably, this is a difficult technical problem that will be 
> > practically
> >     solved during several years.
> >
> >     Regards,
> >
> >     -----
> >     Sergei
> >
> >
> >
> >     >> There are type systems overlayed on top of initially untyped
> >     >> languages (e.g. the language of Alloy Analyzer) and there are
> >     >> gradual types and designs like TypeScript for to initially 
> > untyped
> >     >> programming languages. ACL2 theorem prover for pure LISP, SPASS
> >     >> theorem prover for first-order logic, and "TLA+ model checking 
> > made
> >     >> symbolic" model checker for TLA+ all include techniques to 
> > recover
> >     >> types from an initially untyped language.
> >     >>
> >     >> Best regards,
> >     >>
> >     >> Viktor
> >     >>
> >     >> On Tue, Mar 3, 2020 at 8:44 PM Jason Gross 
> > <jasongross9 AT gmail.com
> >     
> > <mailto:jasongross9 AT gmail.com>>
> >     >> wrote:
> >     >>
> >     >>> I'm in the process of writing my thesis on proof assistant
> >     >>> performance bottlenecks (with a focus on Coq), and there's a 
> > large
> >     >>> class of performance bottlenecks that come from (mis)using the
> >     >>> power of dependent types.  So in writing the introduction, I 
> > want
> >     >>> to provide some justification for the design decision of using
> >     >>> dependent types, rather than, say, set theory or classical 
> > logic
> >     >>> (as in, e.g., Isabelle/HOL).  And the only reasons I can come 
> > up
> >     >>> with are "it's fun" and "lots of people do it"
> >     >>>
> >     >>> So I'm asking these mailing lists: why do we base proof 
> > assistants
> >     >>> on dependent type theory?  What are the trade-offs involved?
> >     >>> I'm interested both in explanations and arguments given on 
> > list,
> >     >>> as well as in references to papers that discuss these sorts of
> >     >>> choices.
> >     >>>
> >     >>> Thanks,
> >     >>> Jason
> >     > _______________________________________________
> >     > Agda mailing list
> >     > 
> > Agda AT lists.chalmers.se
> >  
> > <mailto:Agda AT lists.chalmers.se>
> >     > https://lists.chalmers.se/mailman/listinfo/agda