coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Functors & Opaqueness

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: AUGER Cédric <sedrikov AT gmail.com>
Cc: Gregory Malecha <gmalecha AT cs.harvard.edu>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Functors & Opaqueness
Date: Tue, 16 Apr 2013 15:49:25 +0200

On 16/04/2013 14:08, AUGER Cédric wrote:
> The advantage of Modules over Records are just:
> → name space management
> → notations management
> → tactics management
> → Extraction (to Ocaml)
> → interactive definitions
> → inclusion of other modules via Inline/Include
> → subtyping

You forget an important (and misleading) part of the module machinery,
which is the generativity of universes in modules. Functors create fresh
universes constraints, which is not the case for records.

This advantage may not be as clear when we have the universe
polymorphism branch merged, though.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Functors & Opaqueness, Gregory Malecha, 04/15/2013
- Re: [Coq-Club] Functors & Opaqueness, AUGER Cédric, 04/16/2013
- Re: [Coq-Club] Functors & Opaqueness, AUGER Cédric, 04/16/2013
  - Re: [Coq-Club] Functors & Opaqueness, Gregory Malecha, 04/16/2013
  - Re: [Coq-Club] Functors & Opaqueness, Pierre-Marie Pédrot, 04/16/2013