[Agda] [Coq-Club] Why dependent type theory?
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Wed Mar 4 17:33:23 CET 2020
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
>>
More information about the Agda
mailing list