coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] module "best practices"?

From: David Holland <dholland-coq AT netbsd.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] module "best practices"?
Date: Thu, 23 Aug 2018 20:43:28 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dholland-coq AT netbsd.org; spf=Pass smtp.mailfrom=dholland AT netbsd.org; spf=None smtp.helo=postmaster AT mail.netbsd.org
Ironport-phdr: 9a23:ru7/OhRw1qkM++klZJ6zkW8Krtpsv+yvbD5Q0YIujvd0So/mwa68bR2N2/xhgRfzUJnB7Loc0qyK6/+mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/m/XhMJukaxVoxyhqBNjzIHJYo6aOuFzfr/Bcd4AWWZNQtxcWzJHD4ihb4UPFe0BPeNAoofzvVQOsxq+ChSxD+3tzT9Ignv20rc80+s8DArL2xEvH9IJsHTQqNX6LqESXv2swKbUyjXDduhb2THj54jUaR8huuyDUah3ccrLxkkiDgXIhUiTp4z9Jz6Zy+AAvmyB4+Z+W++ihXQrpx9srjWt3MsglJXFip4Tx1vZ7yt22pw1Kse9SENjYd6rDp9QtyaCOotzWMwiQmVotDw8yrIYpZ60ZzMKx4k9yx7YcfyHfJCE4hPlVOmPPTd1nG9pdba7ihqo70StxOPxWtOq3FpXrCdJiMfAumwR2xDL78iIUPp9/kOv2TaV0ADT7/lJLl00larcL54hxqQ/lpwOvknYGC/5hln2g7SNdko54OSo7P7nYrr+qp+GK4B0kh3+MrgpmsGnHes4NREOU3GH9uS4yb3s5lb0QK5Kj/0ziqnWqorWJcUdpq6jAg9ayJwv6xilD2Tu7NNNln4eaVlBZRivjo7zOliILuqrI+24hgGAmSlqy7jmObnlC5PBZizPkLDleb975wtXzxMby91D7YlYTLYbL6SgCQfKqNXEA0phYESPyOH9BYAlj9JMaSe0GqacdZjqnxqN7+MrLfOLYdZP6jDwN/I+67jpl3BrwAZBL5ns5oMebTWDJtojO1+QOCC+hNodG3wG+A0kQ76y0QDQYXtof3+3GpkEyHQ7BYahVNiRQ4mshPqH0TuxBZEQYXpJWAiB

On Thu, Aug 23, 2018 at 10:21:24AM +0000, Soegtrop, Michael wrote:
> Maybe we should do a feature request to have the "include
> definitions in module type ascription". I guess not that many
> people are using definitions in module types, so likely it would
> break little code.

+1

It's always irritated me in ML that if you put anything nontrivial in
an interface you have to cutpaste it into every implementation.
Especially because it seems completely unnecessary; but maybe there's
some subtlety I'm missing about uniqueness of possible
concretizations.

(as far as breaking stuff, one can just add new syntax for the new form)

--
David A. Holland
dholland AT netbsd.org

Re: [Coq-Club] module "best practices"?, (continued)
- Re: [Coq-Club] module "best practices"?, Samuel Gruetter, 08/18/2018
  - RE: [Coq-Club] module "best practices"?, Soegtrop, Michael, 08/19/2018
    - Re: [Coq-Club] module "best practices"?, Kevin Hamlen, 08/20/2018
      - RE: [Coq-Club] module "best practices"?, Soegtrop, Michael, 08/20/2018
        
        Re: [Coq-Club] module "best practices"?, Benjamin C. Pierce, 08/20/2018
        
        RE: [Coq-Club] module "best practices"?, Soegtrop, Michael, 08/23/2018
- Re: [Coq-Club] module "best practices"?, Adam Chlipala, 08/21/2018
  - Re: [Coq-Club] module "best practices"?, Kevin Hamlen, 08/21/2018
    - Re: [Coq-Club] module "best practices"?, Samuel Gruetter, 08/22/2018
      - RE: [Coq-Club] module "best practices"?, Soegtrop, Michael, 08/23/2018
        
        Re: [Coq-Club] module "best practices"?, David Holland, 08/23/2018
        
        Re: [Coq-Club] module "best practices"?, Anders Lundstedt, 08/24/2018
        
        RE: [Coq-Club] module "best practices"?, Soegtrop, Michael, 08/24/2018