Go backward to Typing Rules Go up to Top Go forward to Example

Record Introduction

• Abstraction/qualification principle:
  • E ::= ...| I=E |E₁,E₂ | with E₁ do E₂ | I

  • pi |- E: theta

    pi |- I=E: {I:theta}

    
    

    pi |- E1: pi1	pi |- E2: pi2
    pi |- E1,E2: pi1 U pi2

    
    

    pi |- E1: pi1	pi -U- pi1 |- E2: theta
    pi |- with E1 do E2: theta

    
    

    pi |- I: theta

    if (I:theta) in pi
• Record I=E
  • Record union E₁,E₂.
  • Local record definitions.
  • Record field reference I.
• Enrichement of type system:
  • Type attribute for records.
  • {i:theta_i}_{i in I}
  • Type assignment attributes introduced.