typed versus untyped

To: types@theory.lcs.mit.edu
Subject: typed versus untyped
From: jcm@ra.stanford.edu (John Mitchell)
Date: Mon, 11 Apr 88 11:51:11 PDT

I tried to make much the same point as Albert regarding
equivalence in this year's POPL paper with Bob Harper.
Specifically, the typed approach leads to stronger notion
of term equivalence, and seems more appropriate for
studying representation independence or full abstraction.

(I believe it is well-known that there are two pure terms 
representing successor on Church numerals which have distinct
normal forms. I haven't checked whether these have all of the 
properties of Albert's example.) 

There is a third, intermediate position which muddies the 
water a bit. Milner's (and others') view of types as subsets 
is useful if we are concerned primarily with type membership.
If we are also interested in "typed equivalence," then we
can also make statements about UNTYPED terms such as 
"M and N are equivalent when used at type t." To use Albert's
example, we could say that the untyped terms 

	M     ::=  (F ONE)
	N     ::=  (F THREE)

are equivalent at type boolfunc. The natural semantics for
this kind of statement about untyped terms is to view types
as partial equivalence relations (i.e. subsets with equivalence
relations). This seems perfectly reasonable, and does not 
view typed terms as basic. (This is essentially the view of
Martin-Lof type theory, it seems, and Nuprl.) However, for 
the second-order lambda calculus, I proved in my 1986 Lisp and
FP paper that every partial equivalence relation model of types
determines an "explicitly typed" model, and the relationship
between meanings of terms is as expected (everything commutes).
The same should hold for other systems, as far as I can see.
So with the "untyped" view of types souped-up a bit,
the typed and untyped views remain essentially equivalent.

>From another point of view, typed model theory seems more general,
since we can construct typed models from partial equivalence
relations, but do not seem to be able to construct untyped
models from typed structures. However, if we consider parital
untyped structures, the we have a model-theoretic equivalence.

John