[Agda] Module definition order

[Ulf Norell]

On Thu, May 22, 2008 at 10:17 AM, Lennart Augustsson <lennart at augustsson.net>
wrote:

> Could someone explain the rationale for the scoping rules in a module?
>
> It seems that the scope of a definition is from the point it is
> defined to the end of the module (except for mutual).  This is like a
> throwback to C, except it's worse.  At least in C I can make forward
> declarations, and then place my definition where ever I like.
>
> It's very easy to allow definitions in any order (and no mutual
> keyword), so why not do that?  Just build the dependency graph and
> find the strongly connected components, and that's it.
>

The reason is that even in mutual blocks the order of definitions is
significant. When type checking the body of a later definition you are
allowed to unfold earlier definitions, but not the other way around. This
means that when you've found your strongly connected components, you'll also
need to pick the right order of the definitions and I don't know how to do
that.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080522/9a903a70/attachment.html