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

[Jesper Cockx]

(I somehow only replied to coq-club)

---------- Forwarded message ---------
From: Jesper Cockx <Jesper at sikanda.be>
Date: Tue, Mar 3, 2020 at 10:37 PM
Subject: Re: [Coq-Club] Why dependent type theory?
To: coq-club Club <coq-club at inria.fr>


Hi Jason,

There's many reasons for me to choose a dependently typed language:

- From a philosophical point of view, dependently typed languages are the
only kind of language that have been given a meaning explanation (in the
sense of Martin-Löf). This is important because it means I can grasp the
meaning of each rule/axiom on a fundamental level, something that I never
managed for set theory.
- From a practical point of view, in a dependently typed language I don't
have to learn and use separate languages for writing programs and for
writing proofs about them. In fact, by giving the write types to my
programs I often do not need to give any proofs at all (i.e.
correct-by-construction programming).
- Dependent type theory is constructive so I do not have to assume
classical principles when I do not need them.
- Since expressions at the type level can compute in dependent type theory,
there are many equalities that I do not need to reason about explicitly but
just hold by definition/computation (although not as many as I would want).

As for other interactive theorem provers not based on dependent type
theory, such as Isabelle or HOL4, I am mainly jealous of their excellent
integration with automated theorem proving tools (e.g. sledgehammer) and
their huge mathematical libraries. In a dependently typed languages, it is
much harder to get everyone to agree on a definition because there are so
many different ways to encode a concept. This has the effect that libraries
are a lot more fragmented and everything is done in a more ad-hoc manner.

Another weak point of current implementations of dependent type theory is
abstraction: you *can* make a definition abstract but that means it becomes
an inert lump that stubbornly refuses to compute, so you lose most of the
benefits of working with a dependently typed language. But I see these as
reasons to continue to improve dependently typed languages rather than to
abandon them.

-- Jesper

On Tue, Mar 3, 2020 at 10:00 PM Viktor Kunčak <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 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> 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
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200303/38410e2e/attachment.html>