Go backward to Expression Abstractions Go up to Top Go forward to Typing Rules

Type Attributes of Functions

• Type attribute of a function established by its definition.
• Type attribute forwarded to users of function
• Introduce type assignment p = Sdec.
  • Set S of (identifier:type attribute) pairs.
  • For each I, at most one (I:H) in S.
• Example:
  • fun A = 1+@loc₁.
  • fun B = @loc₁=0.
  • p₁ = {A: intexp, B: boolexp}dec.
• Each tree node annotated with type and type assignment.
  • p₁ |- loc₁:=A+2: comm.
  • See Schmidt, Figure 2.2.