[Agda] mutual strangeness

[Nils Anders Danielsson]

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.