[Prev][Next][Index][Thread]

Re: Bard's message on subtypes



It's a bit off of the subject, but I wanted to point out something subtle going on in Bard's example:
	\x:nat. (\y:int . y) x
and that is that this term does NOT have type nat -> nat.  Straightforward
use of the typing rules in Cardelli or Cardelli & Wegner shows that
the application of (\y:int . y) to x will only take place if x is first typed
as (coerced to be) an int.  Thus the function has type nat -> int.  The eta
reduction gives a function of type int -> int which of course can also be typed as nat -> int.  However int -> int and nat -> nat are incompatible types and in
general a function from int to int canNOT be "coerced to be nat -> nat".
   Finally note that in "Bounded Fun" (the extension of second order lambda
calculus with bounded type quantification), 
	\x:nat . (\t<=int. \y:t. y) (nat) x
does have type nat -> nat.
   It's a bit off of the main subject, but worthwhile keeping track of since
subtypes end up being fairly slippery in typing.
	Kim Bruce
	Kim Bruce