coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] multiple typeclass instance question
- Date: Wed, 16 Mar 2016 20:35:12 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=arnaud.spiwack AT gmail.com; spf=Pass smtp.mailfrom=arnaud.spiwack AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f46.google.com
- Ironport-phdr: 9a23:IBTwNx/gLsKtx/9uRHKM819IXTAuvvDOBiVQ1KB92+gcTK2v8tzYMVDF4r011RmSDdWds6gP0rCL+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt6U1578jrrvs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+nh7aBSCL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faOTsS7kpVXyZ96Z0QRTrwHMOLCY472jcieR0jbIduBWltgByyI7SYZiIObxwZPWOLpshWWNdU5MJBGR6CYSmYt5KVrJZMA==
Usually one wants some control on what is produced, and the current type inferenceprovides some, with the (informal) guarantee that print(infer(t)) = t. This determinismcan go away as soon as proof search is involved though, through type classes forexample, and means to ensure that this search is predictable are useful too.
We'd rather like infer(print(t)) = t, I suppose. Neither are true in Coq, I don't know which is less true. I don't see how non-determinism affects print(infer(t)) = t. It may affect infer(print(t))=t, but let's keep in mind that, in most cases, a backtracking pretyper would return the first solution, which would be the same as a non-backtracking one. Also, we can already simulate non-determinism by specifying implicit arguments to values which are not found by the pretyper. In theory at least, the situation would not be significantly worse than today. Of course, in practice it may feel rather unpleasant, I don't know.
- Re: [Coq-Club] multiple typeclass instance question, (continued)
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/11/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/11/2016
- Re: [Coq-Club] multiple typeclass instance question, Pierre-Marie Pédrot, 03/12/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/16/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/16/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/16/2016
Archive powered by MHonArc 2.6.18.