coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about definitions inside type classes

From: "John Wiegley" <johnw AT newartisans.com>
To: Ben Sherman <sherman AT csail.mit.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about definitions inside type classes
Date: Thu, 27 Apr 2017 22:32:45 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f178.google.com
Ironport-phdr: 9a23:ZvznfhToPXpQeqZlYIyBXLdXttpsv+yvbD5Q0YIujvd0So/mwa6yYBeN2/xhgRfzUJnB7Loc0qyN4vymATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbx/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRBDI2icoUADeQPPeFboYnzqVQBogexCBKwBO/z0DJEmmP60Lcm3+knDArI3BYgH9ULsHnMotn7MKASUeCzzKLVzTrDbu1Z2Tj56IfWchEtr+yHULVyccrWyUkvEQ3Eg06WqYP7MTKazP4Ns3Sa7+p7T+2vjXUnpxttrTiow8chk4/EjZ8bxFDD8CV22oc1JdugRU59f9GlHoFftzuGN4t3WcMtWWdouD0gxrIavp67eS4Hw4kkyR7Hc/GLbZSE7xb5WOuSITp0nm9pdbahixqo7EStyO7xWtG23VtLtCZJjNfBu38X2xHS7sWLUOZx80il1DuJygvd8PtLIVoumqreM5MhwqA/lp4UsUnbGy/5gkT2jKuPekU89Oik9/3rYrv7qpKeNIJ4kA7+MqMpmsywBeQ3LBICUHSc+eS5zLHj/Ev5T6tWjvAujKXVrJTXKd4Yq6O5GQNZz4Iu5wilAzu70tkVnmELLFdfdxKGi4jpNUvOIPf9DfqngVStnjZryO7JPr3lHJrMLmPOkLjkfbln6k5czBA/wsxY55JREr0BOu78WlfttNzECR80KxC7w+H+CNlkyoweXX+PDbSCPaPJsV6I4/ovLPOWaI8Uvjb9Mfkl6OT0gX83g19ONZWuiLEabjiDHvl8JkyfKS73gtobFG4MlgElRe3uzliDTXhea2vkDIwm4TRuQqChDYGLeYGgj7iMzW3zSp9RZmZZIlaBDn7ya4SfUvEXLimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8id7KM9w==
Organization: New Artisans LLC

>>>>> Ben Sherman
>>>>> <sherman AT csail.mit.edu>
>>>>> writes:

> I have run into this issue before, and one approach that I took was to split
> up such a type class into two parts, one with the "data" and the other with
> the "proofs". The "proof" part would depend on the "data" part and live in
> [Prop] rather than [Type], or at least definitions of the "proof" class
> instances could be closed off opaquely, which can also be beneficial for
> performance reasons. Then your [adj_left] definition can come *after* the
> "data" part but before the "proof" part. You could still later choose to
> package up the data and proof part into a single object.

That's a great idea, Ben, thank you! I will do just that.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Question about definitions inside type classes, John Wiegley, 04/25/2017
- <Possible follow-up(s)>
- Re: [Coq-Club] Question about definitions inside type classes, Ben Sherman, 04/27/2017
  - Re: [Coq-Club] Question about definitions inside type classes, John Wiegley, 04/28/2017