Go backward to Type Attributes of Functions Go up to Top Go forward to Typing Rules

Typing Rules

• Program:

  • {} |- D: pdec	p |- C: comm
    |- D in C: comm

    
    
  • To annotate D in C, annotate D-tree in empty assignment {} and obtain its type pdec. Then annotate C-tree in pdec; if it has type comm, annotate D in C with type comm.
• Declaration:

  • p |- E: Texp

    p |- fun I=E: {I:Texp}dec

    
    

  • p |- D1: p1dec	p |- D2: p2dec
    p |- D1,D2: (p1 U p2)dec

    
    

  • p |- D1: p1dec	pU p |- D2: p2dec
    p |- D1,D2: (p1 U p2)dec

    
    
  • p₁ U p₂ := p₁ union p₂, if {I |(I:H) inp₁}
    intersect {I |(I:H) in p₂} = {} (else undefined)

Construction and combination of type assignments.