coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo.zimmi AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Strange subtyping
- Date: Sat, 9 Jun 2018 11:09:23 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f52.google.com
- Ironport-phdr: 9a23:XIfxAB8jHmCs0P9uRHKM819IXTAuvvDOBiVQ1KB40+gcTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRxDmiCgFNzA3/mLZhNFugq1Hux+uvQBzzpTObY2JKPZzfKXQds4aS2pbWcZRUjRMDJ28b4wVCOoOJeVXr4j4p1sLsxS+HwysC/npyj9Om3T72rE60+Q/HgHBxgAhHtMOsHHRrNX0L6oSXuW1w7PJzTXHdf9ZxTD96I3Rfx0nvPqCXqpwfNLPxUUzEw7JlFadpIz/Mz+Ly+gAvXKX4up+We+plmUpsRt+oiK1yccpkoTJhpwaylTD9ShhxYY6P9y4SEpibd66E5tcqziWN4V2T888WW1otyE6yroJuZ6/YicG0ogoxxnaa/CfcoiI5AzsVPqJLDtmmH5ofKizihWy/ES61OHwS8e53ExKoyZbitXMs2oC1x3X6siJUPt9+UKh1C6T1wDT9O5EJlo4lKvaK54kx74wl4EesUvGHiDsmUX2iLWaeVkj+uit8+jneKnppoeAN49ojQHzKrghmsumAeghLgcOW3Wb9v+n2b34/Uz5Ra1KgecsnqnYtpDaP8UbqbSjDw9byIZwoyq4WjyhyZETmWQNBFNDYhOOyYbzaH/UJ/WtMfc+hGOekTJuyurDN7vnSsHRLnXE1qXgeLN8w0FZwQs3i9tY4sQHWfk6PPvvVxqp55TjBRgjPlnsmre1OJBGzoobHFm3LOqcOaLWv0WP47t2ceaJbY4R/j36Lqp8vqK8vToCgVYYOJKR894PcnnhR6ZpJkyYZTznhdJTST5X7Dp7d/TjjRi5aRAWZ3u2WPhhtDQyCYbjE4SbA47w2vqO2yC0GpAQbWdDWAiB
Yes it is intended: your reasoning is perfectly accurate and unsurprisingly it is confirmed by the Coq type checker.
Le sam. 9 juin 2018 à 01:17, Helmut Brandl <helmut.luis.brandl AT gmail.com> a écrit :
Sorry. I cannot yet get it straight.From the subtype rules in the reference manual and your response to my question it has to be the case that Prop <= Set.From the Conv rule I conclude that T:Prop implies T:Set.This implies that I can feed any proposition into an argument expecting a Set.Definition idset (A:Set)(x:A):=x.The term idset (0<=0) (le_n 0) surprisingly passes the type checker.Is this really the intended behaviour?Sorry if my question is to stupid. But it puzzles me.RegardsHelmutOn Thu, Jun 7, 2018, 10:04 Matthieu Sozeau <mattam AT mattam.org> wrote:Hi,
What we don’t have is Prop : Set indeed, only Prop <= Set and Set <= Type(i). Actually we even have Prop < Set internally, i.e the two sorts are enforced to be distinct. One reason is that the set-theoretic model allows this, the impredicative universe Prop being interpreted as { ø, { ø } } which is a subset of Set’s interpretation. However this subtyping rule is a bit of a pain as it complicates the model: one has to modify the interpretation of function types and applications to use a so-called trace encoding to kind of dynamically detect if a term is in Prop or Set. If we remove it (which is a plan we have for a future version of the calculus), then one can see Prop as a separate universe from the predicative Type hierarchy and your example wouldn’t work anymore.
Hope this helps a little,
— MatthieuLe jeu. 7 juin 2018 à 16:34, Helmut Brandl <helmut.brandl AT gmx.net> a écrit :Hi.I am confused by a subtyping rule mentioned in chapter 4.4 of the reference manual.It says that Prop is a subtype of Set. I checked it with the identity functionDefinition id {T:Set} (x:T):= x.And indeed the _expression_ "id I" is well typed.I always thought that both Set and Prop are subtypes of Type(i) for any i but are not related in the subtyping relation.What is the reason for this subtyping rule? Can anybody explain?ThanksHelmut
- [Coq-Club] Strange subtyping, Helmut Brandl, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Matthieu Sozeau, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Stefan Monnier, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Maxime Dénès, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Stefan Monnier, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Maxime Dénès, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Stefan Monnier, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Maxime Dénès, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/09/2018
- Re: [Coq-Club] Strange subtyping, Théo Zimmermann, 06/09/2018
- Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/15/2018
- Re: [Coq-Club] Strange subtyping, Théo Zimmermann, 06/09/2018
- Re: [Coq-Club] Strange subtyping, Stefan Monnier, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Matthieu Sozeau, 06/07/2018
Archive powered by MHonArc 2.6.18.