[Agda] parameterized modules?

[Andreas Abel]

On 15 Oct 2012, at 7:09 PM, Serge D. Mechveliani wrote:
> Sorry if this is a silly question:

Yes, it is.

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

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