[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