Go backward to Minimal Types
Go up to Top
Go forward to Extension of Subtyping

Denotational Semantics

Meaning of subtyping relation
- [[theta₁ <= theta₂]]: [[theta₁]] $->$ [[theta₂]]
- Coercion map must exist.
- [[theta <= theta]] is identity function.
- [[theta₁ <= theta₃]] = [[theta₂ <= theta₃]] o [[theta₁ <= theta₂]]
- [[pi |- E: theta₂]] $e$ $s$ = [[theta₁ <= theta₂]]([[pi |- E: theta₁]] $e$ $s$ )
Semantics must be coherent
- Meaning of well-typed program independent of derivation used to assert well-typing.
Subtyping on objects:
- {I₁:theta₁,...,I_m:theta_m,...,I_n:theta_n} <=
  {I₁:theta₁',...,I_m:theta_m'}
  if 0 <= $m$ <= $n$ and theta_j <= theta_j' for all 1 <= $j$ <= $m$
- [[{I₁:theta₁,...,I_m:theta_m,...,I_n:theta_n} <=
  {I₁:theta₁',...,I_m:theta_m'}]]
  {I₁= $v$ ₁,...,I_m=v_m,...,I_n=v_n}
  = {I₁=[[theta₁<=theta₁']] $v$ ₁,...,[[theta_m<=theta_m']] $v$ _m}

Id: qualification.tex,v 1.2 1996/05/02 11:53:49 schreine Exp schreine