Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl
Subject: Re: a question about define_type
In-Reply-To: Your message of 07 Nov 91 21:34:00 +0000. <3529*joyce@cs.ubc.ca>
Date: Fri, 08 Nov 91 15:58:30 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.842:08.10.91.15.58.53"@cl.cam.ac.uk>

Regarding Jeff's recent query:

> 1. Is this restriction just an artifact of the current implementation
>    of define_type ?

the define_type program was designed to solve a specific and well-defined
class of equations, namely those of the form stipulated in the documentation.
This class does not include the equation

   `ty = X | C (ty)list`     [1]

   It would not, however, be particularly difficult to extend the class
of types dealt with by the recursive types package to include the type
specified by [1].  The underlying representation type is rich enough to
handle this. Of course, one would have to rewrite every function in the
package to deal with this extended class of types.

   But I would not suggest ad-hoc extension of the package for just this
problem.  For if we do the programming for [1], then why not also for:

   ty = X | C ((ty)list)list
   ty = X | C (ty # *)list
   ty = X | C (* # (ty)list)
   ty = X | C (ty + ty)list .... etc

or, indeed, also for ty = X | C (num->ty)?

   The problem is that nobody has the time to do a proper job of this.
Or are there any volunteers?

Tom