[Agda] [Coq-Club] Why dependent type theory?

Ulf Norell ulf.norell at gmail.com
Wed Mar 4 17:52:59 CET 2020 

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200304/94268780/attachment.html>

More information about the Agda mailing list