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

[Pierre-Marie Pédrot]

On 04/03/2020 10:42, Thorsten Altenkirch wrote:
> To me the most important feature of Type Theory is the support of
> abstraction in Mathematics and computer science. Using  types instead of
> sets means that you can hide implementation choices which is essential
> if you want to build towers of abstraction. Set theory fails here badly.

This is true, but I am also afraid that "dependent type theory" is a
regression on that point, compared to, say, ML.

Conversion is a fanciful abstraction-breaker that is a well-known source
of non-modularity in dependently-typed languages. Worse, there is not
even a proper way to abstract over it, except for monstruosities such as
Extensional Type Theory, where you throw the baby with the bathwater.

The weak type system of ML is a strength in this setting. As long as you
don't touch the interface, you can mess with the implementation and it
will still compile. (Running properly is another story.)

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/75d41b59/attachment.sig>