[Agda] mutual strangeness

[James Chapman]

Hi,

On 2 Feb 2009, at 16:42, Lennart Augustsson wrote:
> 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

Yes I agree. I would like the machine to find the ordering. I like the  
current arrangement most of the time:

mutual
   data Blah where
     constructors

   f : Blah -> Blah
   f x = y

   data Bluh where
   ...

This is fine until you have to give aliases to things or define  
special cases of types just to work around the scoping restrictions.

However, sometimes it is nice to group all the type constructors  
together. For example Conor has suggested something like this to me  
before:

data
   A
   B
   C
where
   conA1
   conA2
   conB1
   etc.

> On Mon, Feb 2, 2009 at 11:33 AM, Nils Anders Danielsson
> <nad at cs.nott.ac.uk> wrote:
>>
>> Do you think that it is possible to construct a core theory into  
>> which
>> your scheme can be transparently translated?

I don't know how to do this. Am I correct in saying that there is  
currently no explanation (or translation into a core theory) of mutual  
inductive types that cannot be collapsed into a single inductive type?  
Let alone what happens when you combine these types with induction- 
recursion or even the more interleaved version I have tried to describe.

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

I think this is a case where you know the program you want to write  
first, so you try to find a language you can write it in. Then when  
you have the language you will probably find some more programs that  
you want to write in this way. I have the feeling I'm badly  
paraphrasing Conor here too!

James

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.