Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <5255.9212231331@frogland.inmos.co.uk>
Subject: Re: define_type extension?
To: shb@com.oracorp
Date: Wed, 23 Dec 1992 13:31:14 +0000 (GMT)
Cc: info-hol@edu.uidaho.cs.ted
In-Reply-To: <9212231309.AA02406@sparta.oracorp.com> from "shb@oracorp.com" at Dec 23, 92 08:09:35 am
Content-Type: text
Content-Length: 1701

shb@oracorp.com has said:
> Is there some profound reason why
> 
>   define_type `foo` `foo = bar1 | bar2 (foo)list`;;
> 
> gets the response
> 
>   evaluation failed     ill-formed type expression(s)  ?
> 
> I can see why expressions defining foo in terms of function types
> involving foo are sometimes impossible to handle, but there's an
> obvious recursive algorithm for telling whether an object is an object
> of type foo.  The mut_rec_types contrib entry extends define_type, but
> I can't test trying to get the same effect with it because its makefile
> fails at our site for some reason I haven't figured out.  Has anyone
> made an extension of define_type that recognizes lists as exceptionally
> easy and handles them correctly?

i think the reason isn't very profound ... its just that the type 
definition mechanism is designed to handle thay sort of type.

in the procedings of HOL92 there is a paper by elsa gunter which
discusses type definitions in HOL. she says that they have
implemented an extension of the type definition mechanism in
hol90 which allows the defined type to have recursive occurences
of itself inside recusively defined types.

also, a few weeks ago i was playing around with an idea to allow
the defined type to occur as the range of functions: i.e.
allowing a mini csp-like type

process = SKIP | INPUT (*->process) | OUTPUT * process | DISJ process process


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                1992: celebrate the quincentenary of columbus getting lost