[Agda] mutual strangeness

[James M Chapman]

Hi all,

I would like to propose a generalisation of the current scheme. Basically this is how I personally would like it to work:

A mutual definition type checks if it can be written down as a Generalized Algebraic Theory in the sense of Cartmell in the following way:

There are four levels of things to be checked.

1. Sort symbols - These are type constructors or the type signatures of type-valued functions.
2. Operator symbols - These are data constructors or type signatures of data-valued functions.
3. Equations between sort expressions - These are the individual lines of type-valued function definitions.
4. Equations between term expressions - These are individual lines of a data-valued function definitions.

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.

In more detail:

First put the sort symbols in a sequence so that the type of each symbol only refers to previous type symbols in the sequence.

Second put the operator symbols in a sequence so that each symbol only refers to previous operator symbols in the sequence or sort symbols.

Third put the equations between sort expressions in a sequence so that each symbol refers to sort or operator symbols but also it may require that an earlier equation (line of a (potentially the same) type valued function definition) must be executed for it to typecheck.

Forth do the same for equations between term expressions (lines of a data valued function definition) as sort expressions.

The point in the last two is that it is sometimes the case that to type check a function definition we must be able to execute other lines of the definition itself. This happens quite regularly when dealing with the 'total syntax of type theory' when you are defining operations on types as often the case for 'El' requires that the case for 'U' to be executed for it to typecheck.

Sorry this isn't very rigorous, I guess it is just a 'feature request'.

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.

Regards from Estonia,

James


On Sun, Feb 01, 2009 at 02:09:54PM +0000, Thorsten Altenkirch wrote:
> A few thoughts:
> 
> Actually there are two issues with mutually inductive and inductive  
> recursive definitions which should be considered independently:
> i) We have to avoid to much circularity to make sense. E.g. we can  
> only pattern match once we have seen all constructors.
> ii) We may have negative occurences if they are on structurally  
> smaller instances. This allows the definition of universe-like
>      constructions.
> 
> Actually, in my intended application (total syntax of Type Theory)  
> only the first issue arises, the ii) is not relevant since the syntax  
> is finitary.
> 
> I believe it should be possible to justify a very liberal approach re  
> i). Clearly every constant and definition has to appear before it is  
> used. One should expect that all constructors and cases appear  
> together, even though there are case where one would like to  
> interleave those as well. However, this may get a bit tricky to justify.
> 
> For ii) one would hope that it is sufficent to say that negative  
> occurences may appear on structurally smaller recursive calls. One  
> should hope that this can be justified via Anton's Mahlo universe.
> 
> Thorsten
> 
> On 1 Feb 2009, at 13:27, Nils Anders Danielsson wrote:
> 
> >On 2009-02-01 12:16, Thorsten Altenkirch wrote:
> >>On 1 Feb 2009, at 04:43, Nils Anders Danielsson wrote:
> >>>A better alternative might be to try to come up with new rules for
> >>>mutually recursive definitions, preferably both flexible and easy to
> >>>understand.
> >>Indeed, and moreover these rules should be justified, ideally by a  
> >>translation into a core type theory with a fixed set of combinators.
> >
> >Indeed. Moreover this translation should ideally be simple and
> >transparent, and the core theory simple and consistent. :)
> >
> >-- 
> >/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
> 
> 
> 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

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.