Re: typed versus untyped

To: types@theory.lcs.mit.edu
Subject: Re: typed versus untyped
From: gtl@electron.lcs.mit.edu
Date: 11 Apr 88 18:09:37 D (Mon)
Cc: gtl@electron.lcs.mit.edu

	In my thesis research on subtyping in object-oriented programming
languages (like Smalltalk-80) I have (independently) discovered a notion
similar John Mitchell's ``typed equivalence.'' Specifically, for each type T,
there is a relation that I call ``imitates-via-T.'' Roughly speaking, an object
q imitates-via-T an object r in a given programming language if, for any
observation P(x:T) of visible type, the possible results from P(q) are a subset
of the possible results from P(r) (I allow nondeterminism).  Of course, in the
study of subtyping, an object may be observed at various different types; the
type of the formal argument to an observation (e.g., T), is limits the instance
operations that can be applied to the actual argument.

	Let me give an simple example.  Consider two immutable integer triples
(1,2,3) and (1,2,4).  These triples can be treated as if they were integer
pairs, so we have
	(1,2,3) imitates-via-IntPair (1,2,4).
But it is not true that
	(1,2,3) imitates-via-IntTriple (1,2,4),
since the type IntTriple gives one access to the third component of the triple.

	Gary Leavens