[Agda] parameterized modules?

[Andreas Abel]

On 17.10.2012 12:42, Serge D. Mechveliani wrote:
> 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?

That is already the main purpose.

Internally, we use parametrized as a tool for local definitions, like 
where clauses.

> 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?

Well, you have not turned module Sort into a class.

You have just abstracted over the Sort module parameters manually in 
insert.  Parametrized modules do that for you.

> 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.

Modules are not first-class in Agda.  If you would need to abstract over 
modules or compose modules, then switch to records, which are 
first-class.  Classes are just records used with instance inference.

Note that records do not support recursive function declarations, for 
instance, nor local data type definitions.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/