Feature Request: meta modules re-exporting a lot of definitions

[gallais]

Would it make sense to define a meta module Data exporting a lot of the standard data structures? Because we can have a lot of functions with similar names in these various modules, it would only expose the type and its constructors (Agda can disambiguate them in a type-directed manner) and provide a short name to refer to the module itself.

For instance:

module Data where

import Data.Nat
import Data.Fin hiding (module Fin)
import Data.List
import Data.Vec hiding (module Vec)

module Nat = Data.Nat
open Nat using (ℕ ; zero ; suc) public
module Fin = Data.Fin
open Fin using (Fin ; zero ; suc) public
module List = Data.List
open List using (List ; [] ; _∷_) public
module Vec  = Data.Vec
open Vec using (Vec ; [] ; _∷_) public

-- etc.

We can also think of defining e.g. a Prelude module which would also re-export content Function, Relation.Binary.PropositionalEquality, etc. Basically all of the really useful modules.

This type of module which is purely re-exporting (potentially renamed) constants could also be relevant to #60: it'd be a way to provide saner naming conventions whilst maintaining backwards compatibility.

[MatthewDaggitt]

Hmm interesting suggestion. I'm unsure how useful this would be in practice although I'm open to being convinced! The problem as I see it is that for anything that involves proofs rather than programming you're still going to have to individually import the Properties file for each type. I can imagine it might be useful for "Introduction to Agda" sort of tutorials, on the other hand you often want to demonstrate your own implementations of the basic datatypes in such tutorials.

Unfortunately I don't think it would help with #60 because the problematic names in questions are record fields for orderings e.g. decTotalOrder. Therefore they can't be renamed ahead of time, but only renamed locally when opening them.

[gallais]

Can't you provite a DecTotalOrder' module parametrised by a record exporting renamed fields? Because when you open DecTotalOrder my_record you basically apply such a module and open it.

[MatthewDaggitt]

Can't you provite a DecTotalOrder' module parametrised by a record exporting renamed fields? Because when you open DecTotalOrder my_record you basically apply such a module and open it.

But am I right in thinking DecTotalOrder' wouldn't be compatible with DecTotalOrder? You could only use DecTotalOrder' when you wanted to open it but it wouldn't be able to interact with the rest of the library. And each time you'd have to feed your original DecTotalOrder through the converter module anyway, so you're not gaining much over simply renaming the variables manually which at least has the advantage that it's clear what you're doing and why you're doing it.

[gallais]

I'm not sure I understand what you mean. Here is the kind of thing I have in mind IsDecTotalOrder' is not another record we'd need to translate to but rather a different "opening" module than the one generated automatically for each record type declaration:

module DecTO where

open import Level
open import Relation.Binary

module IsDecTotalOrder'
       {a b c : Level}
       {A : Set a}
       {E^A : A → A → Set b}
       {O^A : A → A → Set c}
       (R : IsDecTotalOrder E^A O^A) where

  open IsDecTotalOrder R public hiding (refl ; trans)

  ≈-refl : Reflexive E^A
  ≈-refl = IsEquivalence.refl (IsDecTotalOrder.isEquivalence R)

  ≈-trans : Transitive E^A
  ≈-trans = IsEquivalence.trans (IsDecTotalOrder.isEquivalence R)
  
  ≤-refl : Reflexive O^A
  ≤-refl = IsDecTotalOrder.refl R

  ≤-trans : Transitive O^A
  ≤-trans = IsDecTotalOrder.trans R

postulate
  A   : Set
  E^A : A → A → Set
  O^A : A → A → Set
  R   : IsDecTotalOrder E^A O^A

test : (a : A) → O^A a a
test a = ≤-trans (reflexive ≈-refl) ≤-refl

  where open IsDecTotalOrder' R

-- vs:

test' : (a : A) → O^A a a
test' a = trans (reflexive (IsEquivalence.refl isEquivalence)) refl

  where open IsDecTotalOrder R

[MatthewDaggitt]

That's very clever, and completely different from what I thought you were proposing! And definitely quite a neat solution!

The only problem might be the potential to deeply confuse new users to the library, Where would you imagine putting such modules?

[gallais]

Something like Relation.Binary.Renamed?

[MatthewDaggitt]

Having had a look at some other people's libraries, this seems to be quite common. @gallais apologies for being a little sceptical at first!

Feel free to put a PR together. I think best to leave out the clever field renaming tricks for common records for now. Probably will just confuse people.