Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Date: 7 Nov 91 21:34
From: Jeffrey Joyce <joyce@ca.ubc.cs>
To: info-hol <info-hol@edu.uidaho.cs.ted>
Message-Id: <3529*joyce@cs.ubc.ca>
Subject: a question about define_type


I attempted to make the following type definition (a simplified
version of my original problem):

  define_type `x1` `x1 = A1 | B1 ((x1)list)`;;

but it results in,

  #evaluation failed     ill-formed type expression(s)

which is clearly the result predicted by the HOL documentation:
"... the type being defined may not occur as a proper subtype in
any of the types of the arguments of the constructors".

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

2. I think that mutually recursive types would work,

        eg. define_mutually_rec_type
              `x0` `x0 = x1 list`
               `x1` `x1 = A1 | B1 x0`;;

     note: "define_mutually_rec_type" is just something I've made up !

     ... but this is a bit of hack (I'd rather just not have the
     restriction on define_type that disallows the above use of
     define_type)

3.  I'd like to have types of this kind for representing the abstract
    syntax of languages with terms that may consist of a list of
    sub-terms.  For example, I would like to have a type such as,

       DataStructures = INT | CHAR | RECORD (DataStructures)list

    for terms such as,

        RECORD [INT;CHAR;RECORD [INT;INT]]

4. Any suggestions ?

       (I'm sure that others must have encountered this before).