Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] multiple typeclass instance question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] multiple typeclass instance question


Chronological Thread 
  • 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 inference 
provides some, with the (informal) guarantee that print(infer(t)) = t. This determinism
can go away as soon as proof search is involved though, through type classes for 
example, 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.




Archive powered by MHonArc 2.6.18.

Top of Page