Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Impredicative Set

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Impredicative Set


Chronological Thread 
  • From: Stefan Monnier <monnier AT IRO.UMontreal.CA>
  • To: Xavier Leroy <xavier.leroy AT college-de-france.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Impredicative Set
  • Date: Tue, 02 Apr 2019 12:49:05 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=monnier AT IRO.UMontreal.CA; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT pruche.dit.umontreal.ca
  • Ironport-phdr: 9a23:odcdiRVFSFjXQ8OzNQBBTHt4y/LV8LGtZVwlr6E/grcLSJyIuqrYbBOFt8tkgFKBZ4jH8fUM07OQ7/m5HzRYqsbd+DBaKdoQDkdD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrssxhfTvndEZ+tayGBnKFmOmxrw+tq88IRs/ihNp/4t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ91cXDJdDIyic4QPDvIBPedGoIn7u1sOtga1CQ21CO/y1jNEmnr60Ksn2OojDA7GxhQtEdIQvnrJr9v1OqkcXuK7w6bH0TrOdO9W1Svn5YTUbhwsu+2AULRtesTR00kvEAbFg02Np4z5ITyV2P4Cs26G5ORnUuKvjWgnqwBvrTi128whjYzJhoUTylDC9CV23pw1KMa7RkBneNCoCpVfuSadN4twXsMiWX9ntzw+yrEcp5O2YDEHxZI6zBDcc/yKa5WE7xz9WOqLPzt0mH1odKihixu98EWs0PPwWtes3FpXoCdJjMPAum4R2xHc8MSLVPlw8l2/1TuAyQze7PxPL1oumqrBMZEhx6Y9lpoNvkTHGS/7gF32jLWLdko4+uin9f7rbajnpp+ALYN0lwT+MqMomsyjG+Q3LBIBX2yB9eugzrLv5Uz5QLNUgf0qiqTVrZ7XKdoBqqKnHwNY3Zwv5wiwAjqnytgUg2cLIEpAeB2djojpP1/OIOr/Dfe6m1mslTBrx/bAPr3gHJrNNGPOkLb7fbZ68UJc1Q8zzddZ55JIELEOPuj8WkvruNPEFBA1Kxa0zPr/CNVhyoMeXnqCDbOeMKPLqFOH+uYvI/SXa4IOozb8K/0l5+b0gnMjmF8de7Op3ZoNZ3yiEPRmORbRXX25st4fEGoQ9i4zVuv7wAmSWCBSamz0W68m4SATA4WiCYrMS8WhjfmPxi69FZAQaHoQWX6WFnK9TJmJVf4KIAeVJMlgnyZMAb2mTYkg2AuGlTXdjYdCKezI4CARsdTI/Y4mtKXoiRgu+GksXIym2GaXQjQxxztQHm5k7OVEuUV4j2y7/+19iv1cG8ZU4qoZAAYgMtjByut8F8r/UwaHdd7bEQ/6EOXjOik4S5cK+/FLe1x0QoXwryrkmRePBLkJjbGCANof2/CEhiWjF4NG03/DkZIZoRwmT89IbzD0nrRi/AjeQYLIjwOEkqGsab4R1SqL/27RlWc=

> The usual objection is that typechecking is undecidable. The party line
> for typed programming languages is that they should be Turing-complete but
> have decidable type-checking, or maybe even type inference. F_omega +
> general recursion fits this profile.

I think this is just the result of a confusion between theory and practice.
Decidability of type-checking is neither necessary nor sufficient for
what people really want:
- decidability doesn't do them any good if it takes centuries (or
petabytes) to terminate.
- lots of real languages have potentially non-terminating "compile-time
operations" (whether it's type-checking, type-inference,
macro-expansion, tactic expansion (to tie this back to Coq), ...) and
users don't seem to mind.

I think the more important aspect is that you can only erase terms which
are known to be pure (and hence terminating). For that reason Type:Type
makes erasure of type arguments more difficult.


Stefan



Archive powered by MHonArc 2.6.18.

Top of Page