[Agda] mutual strangeness

[Lennart Augustsson]

When it comes to ordering things, I prefer the computer to do menial
tasks rather than imposing them on me.
That's true for the whole mutual construct as well as what goes inside it.

I don't think reading is an issue.  I (with the help of Emacs) am
capable of scanning the text in both directions for a definition.

  -- Lennart

On Mon, Feb 2, 2009 at 11:33 AM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> On 2009-02-01 16:53, James M Chapman wrote:
>
>> Basically we just try to put everything in a sequence so at each level
>> you can only refer to earlier things at that level or things at an
>> earlier level. If not you have a cycle and you give up.
>
> Should the user specify the sequence, or is it up to the system to
> search for it? I think that it may be very hard to read code if we do
> not use the textual order of equations, but this is perhaps more
> restrictive than what you have in mind.
>
> Do you think that it is possible to construct a core theory into which
> your scheme can be transparently translated?
>
>> You can get some (all?) of the way to what I would like now by
>> defining lots of auxiliary functions that have types which are special
>> cases of the types of other functions and also by defining functions
>> which evaluate immediately to a constructor but this rapidly become
>> totally unreadable.
>
> Some people may not recognise the problems that are discussed here. As
> far as I know they have only been observed when people have tried to
> formalise dependently typed languages in a well-typed way, i.e. without
> the use of raw (untyped) terms. It would be interesting to know if
> anyone has encountered them in another context.
>
> --
> /NAD
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses, which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>