[Agda] parameterized modules?

[Serge D. Mechveliani]

On Wed, Oct 17, 2012 at 08:36:28AM +0200, Andreas Abel wrote:
> On 15 Oct 2012, at 7:09 PM, Serge D. Mechveliani wrote:
[..]
>> are you sure that Agda really needs parameterized modules?
>> For example, Haskell has not such and still looks all right
>
> It looks alright, but you cannot really do abstract developments.  For  
> the other end of the spectrum of module systems, see ML functors.
>
>> (except absence of dependent types).
>> If they are replaced with classes and instances by records, then the
>> implementors could save effort.
>
> Classes cannot replace modules, since classes are inferred automatically 
> and thus need unique instances.
>


Sorry, this is somewhat not so clear to me, looks rather generic.
Consider an example of a parametrized module for several functions 
related to sorting a list:  

 module Sort (A : Set) (_<=_ : Rel A _) 
                       (isDTO : IsDecidableTotalOrder \equiv _<=_)
   where
   insert : A -> List A -> List A
   insert x []       = x :: []
   insert x (y :: ys)  with x <=? y
   ...               | yes _  = x :: y :: ys
   ...               | no _   = y :: insert x ys

   <other related functions>

(the examples in this letter were not tried to compile).

I understand its idea as follows.   
module Sort-T-l = Sort T lessEQ  
produces a module  Sort-T-l  which is ready to perform `insert' for 
for this given particular type T and this given DTO ordering  lessEq  on  
T  (T and lessEq  are uniformly substituted for  A and _<=_).
And then, a programmer can choose different pairs (T , lessEq).

Now I try to replace a parameterized module with using classes:

  insert : {A : Set} -> {_<=_ : Rel A _} ->
           (isDTO : IsDecidableTotalOrder \equiv _<=_) -> A -> [A] -> [A]

  open IsDecidableTotalOrder {{...}}
  insert _     x []         =  x :: []
  insert isDTO x (y :: xs)  with x <=? y
  ...               | true  = x :: y :: ys
  ...               | false = y :: insert isDTO x ys

Now, having any given  T : Set,  any given  lessEq : Rel T _,
and a record value
                   isDTO : IsDecidableTotalOrder \equiv lessEq
for this lessEq,
a call             insert isDTO x xs

performs the insertion for any  x : T,  xs :: List T.
Fetching to `insert' different pairs (T , lessEq) will do the needed 
thing.
The effect is the same as in a parameterized module.
Is not it?
If it is the same, why does one need a parameterized module?

I see only the following reason.
Suppose that the above parameterized module  Sort  has many types and 
functions:  insert, sort, merge, merge-sort ...,
and they depend on the _same_ above parameters  (A, _<=_, isDTO).
A parameterized module allows to _skip uniformly_ the part
  (A : Set) (_<=_ : Rel A _) (isDTO : IsDecidableTotalOrder \equiv _<=_)

in all these item declarations
(no matter whether they are denoted as implicit by `{}').

Now, I think that:
a parameterized module is a tool for an automatic insertion of some 
common declaration prefix to many declarations in this module.
Is it for something else?

Well, this may be a reason for supporting parameterized modules.


> Classes cannot replace modules, since classes are inferred automatically
> and thus need unique instances.

Can you illustrate this on the above sorting example?
In the above my example,   IsDecidableTotalOrder  stands for something 
like a  class,  and each value pair  (lessEq, isDTO)  stands for an 
instance of this class.
Right? 
Where is an automatic class inference, where is an unique instance?

A programmer has a choice:
(PM) to program the sorting-related functions by using a parameterized 
     module, as in the first example,
(C) instead of using a parameterized module to use the class denotations
    in each sorting-related function (as in the second example).

(C) replaces (PM) at the cost of inserting a repeating prefix in the 
    declarations in each related function.

And I suspect that choosing (PM) one looses a certain imporant 
possibility as compared with (C). 
This will be visible in the case when sorting is lifted to a tower
of types built by repeated applying of several type constructors
(for example, the tower over the set {Nat, \times, List}). 

This year I had such an unlucky experience with  parsing  designed via 
parameterized modules  as compared with its design via  classes.
This was with the  Spad  language which has _categories_ for classes
and _packages_ for parameterized modules.
>From this time, I a bit fear of parameterized modules, have an 
impression that they tend to lead to a wrong field. 

Thank you for explanations,

------
Sergei