The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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

Attachment: signature.asc
Description: OpenPGP digital signature