The Coq mailing list

[Ulf Norell <ulf.norell AT gmail.com>]

On Wed, Mar 4, 2020 at 5:33 PM <mechvel AT scico.botik.ru> wrote:

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.

This will certainly not be a hard type checking problem for Agda. Depending on how

you define _*_ and Z computing with G can of course blow up.

/ Ulf

> 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
>>

_______________________________________________
Agda mailing list
Agda AT lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda