Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] "Opaquify operator" to simplify work with dependent types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] "Opaquify operator" to simplify work with dependent types


Chronological Thread 
  • From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] "Opaquify operator" to simplify work with dependent types
  • Date: Tue, 15 May 2018 16:26:32 +0000
  • Accept-language: en-CA, en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM03-BY2-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:+00u2BSUVLWYEaj4X+fRTeej2tpsv+yvbD5Q0YIujvd0So/mwa6yYxSN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zIHIb46YL+Bxcr/Bcd4AWWZNQsZcWipcCY28dYsPCO8BMP5coYbnvFsOqh2+DhS1COzsyj9IgXn23aIn2Oo8EQHJwgogH90XvH/Jrtv1KboZXOe7zKbVzTXCbuhW1Snh5ITVbhwsuvGMXbVsccrU00YvFgfFgk+MpoziOjOYz+IAuHWV4epnUOKgkW8nqwdprziuwMcslpfGhoYPxl/Z6yp0xps+K96gSENjbtOoDIFcuiWEO4dsQ84uWW5ltSkixr0Ip5G2fzQGxZEiyhPRdvOKd4aF7xf5W+mKLzp0mXdod66xhxuw/0itz/HzWdW63VZEqCdOj8PCuWoX1xPJ78iKUvt98Vml2TaIzw3d8v1JL0comafVMpIs37w/moQKvUTEBSD5hl/6jKiLdkU44eeo7PnnYrP7qZOGL490kAb+MrgwlcOjHeQ4Mw8OX26B9eS7yb3j4Un5QLJNjv01iKXWrJfaJcEDqq64BQ9azJoj5g6wAju6ytgVmWcLIEhEdR6dgIXkNEnCIPXiAve+h1Ssni1rx/fDPrD5DJXCM3jDkbb6fbpj90JQ1RY/wMtf55JTFrEBJej8Wk71tNDCEhA5NAm0z/79CNphzoMeRX6PAqiBPazOtl+I//sjLPWIZI8IoznwMOMl5v7rjX8hg1ARZ6ip3Z0NaHC5BPtqOUuZYWC/yusGRC0BuRN7R+j3gnWDVyRSbjC8Reh0sjo8EcetCZrJboGrmr2ImimhSM54fGdDX3KFCnDuP8C2W/AKZ2qpIsJnnXlMdaXpH4Et1QO17lejk5JnKfbR8ywc85nk0Y4mtKXoiRgu+GksXIym2GaXQjQsxzJad3oNxKl65HdF5BKG2Kl8jeZfEIUItfNOTgIzNJqaxOt/WYmrBlDxO+yRQVPjee2IRCkrR4tqkd8Jf0N0GtHkhRfGjXLzXu0l0oeTDZlxyZrymnj8I8EhlCTg/Yx51BwMc5EKMmerwKli6wLUGojF1V2DkLqnfrgd2yiL83qfyW2JvwdTVwsiCKg=
Hi Michael,

I'm interested in your question but I'm not sure I'm understanding well. This sounds similar to irrelevance parameters in Agda, which is used whenever some terms are considered "proof only" and to prevent the compiler from looking into them. Maybe a small example would help with understanding?

Thanks,
Jason Hu


-------- Original message --------
From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
Date: 5/15/18 12:12 (GMT-05:00)
To: coq-club AT inria.fr
Subject: [Coq-Club] "Opaquify operator" to simplify work with dependent types

Dear Coq Users/Team,

 

I did some experiments with dependent types again, and I think the thing I am sometimes missing is an opaquify operator. Terms of dependent types usually contain a mixture of “data” expressions one is interested in and “proof” expressions for which just the type is interesting. The idea is that if I have a term, opaquify(term) makes the term as such opaque, only the type remains visible. The term cannot be unified any more, only its type.  When printing an opaquified term, it is printed as something like opaque:<type> or maybe just opaque in case the type can be inferred.

 

I can use notations and to a certain extent opaque proofs to hide the proof parts of terms of dependent type, but sometimes I think it might also help Coq’s performance to know that it should never look into the term as such, just as if it would be an opaque proof term. Another benefit would be less distraction and maybe a better understanding of the users.

 

My question: am I doing something wrong when I end up at this thought? How are others handling this?

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928


Archive powered by MHonArc 2.6.18.

Top of Page