[Agda] Module definition order

[Lennart Augustsson]

OK, if you need a restriction about unfolding, then I guess definition
order is all right for that.
But why force it on the rest of the module?  It makes code
organization rather ugly at times; I like to group related things
together and now I can't.

  -- Lennart

On Thu, May 22, 2008 at 9:28 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
>
> 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
>