Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <6608.9404201541@frogland.inmos.co.uk>
Subject: Re: Overloading of constants
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Wed, 20 Apr 1994 16:41:55 +0100 (BST)
In-Reply-To: <"i80fs2.ira.967:20.03.94.15.03.07"@ira.uka.de> from "reetz" at Apr 20, 94 03:26:01 pm
Content-Type: text
Content-Length: 2465

reetz has said:
> variables in HOL90 can be overloaded, i.e.
> you can have variables in the same scope
> with same names, but different types and
> these variables are distinct, e.g.
> 
> let
>  val x_num      = mk_var{Name="x",Ty=(==`:num`==)}
>  val x_bool     = mk_var{Name="x",Ty=(==`:bool`==)}
>  val x_num_eq_0 = mk_eq{lhs=x_num,rhs=(--`0`--)}
> in
>  mk_conj{conj1=x_num_eq_0,conj2=x_bool}
> end;
> 
> leads to
> 
> val it = (--`((x :num) = (0 :num)) /\ (x :bool)`--) : term
> - Compat.frees it;
> val it = [(--`(x :num)`--),(--`(x :bool)`--)] : term list

Note you have to go to some lengths to persuade HOL to accept this

(--`(x = 0) /\ x`--);

doesn't parse

> So, what makes variables different from constants in respect to
> overloading? Can't we have constants with same name, but different
> types for some theoretical reasons? But why does it works with
> free variables? Or is it just not implemented in HOL90?

The problem is the way HOL parses things. When it gets a name it looks
it up to see if its the name of a constant. If so, the parser returns a
constant with the relevant type. If you had 2 constants with the same name
then HOL wouldn't know which type to use.

What could be done is for overloaded constants would be to return the 
"least general" type that match the types of any constants with that name,
perform and then rest of the parsing and type unification. After this the
parser would have to revisit all (overloaded) constants to ensure that their
types had "resolved" to a legal value.

E.g. is + were overloaded as :num->num->num and
:integer->integer->integer. The in an expression

--`(E1) + (E2)`--

the parser could parse + as a constant with type :'a->'a->'a and the
infer types from E1 and E2. After finishing this it would have to check
that 'a had resolved to :num or :integer -- note that the full term
being parsed would have to be type inferered first as the inference of
'a could come externally from this sub expression.

I expect that there are good reasons why this might not work.

The other reason is that when you type

	--`1 + 2`--

you may not want to have to say

	--`(1:num) + 2`--

or

	--`(1:integer) + 2`--


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."