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

[Thorsten Altenkirch]

Good point. However, this is on a different level. While you can replace one object with another that behaves the same this doesn't mean that you can replace one piece of program text with another that produces an object that behaves the same. Clearly replacing program text must be an intensional operation. When you design your software or proof you need to take care that you support the right kind of parametrisation. Having types is essential but it doesn't mean that good design comes for free. As far as the dependency of code from arbitrary implementation choices is concerned I agree that we need to be more flexible about the distinction of strict and definitional equality. 

Thorsten

On 04/03/2020, 10:39, "Pierre-Marie Pédrot" <pierre-marie.pedrot at inria.fr> wrote:

    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
    
    




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.