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

[Pierre-Marie Pédrot]

On 03/03/2020 22:31, Jason Gross wrote:
> 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.

Without going fully reflexive, I have been told several times that the
computational nature of conversion was actually increasing the
performances compared to systems that do not feature it. In particular,
the meme-y "proving 2 + 2 = 4 requires on the order of 10⁷ symbols" has
some hint of truth in conversionless theories. Computation allows for
much more compact proofs, hence more efficient to typecheck. Memory is
not free.

(Note that I have no empirical proof of that, I am merely conveying
hearsay.)

Obviously, you can write (almost) arbitrary computations in conversion,
but then, I find it somewhat strange to complain about it. You can write
superexponential algorithms in C++, but that's not a valid reason to
rant against the language. I really wonder why people blame
dependently-typed languages instead of their own inefficient programs.

PMP

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200304/4c3d3a12/attachment.sig>