11.8 Records

 < Free Open Study > 



11.8 Records

The generalization from n-ary tuples to labeled records is equally straightforward. We simply annotate each field tj with a labelli drawn from some predetermined set L. For example, {x=5} and {partno=5524,cost=30.27} are both record values; their types are {x:Nat} and {partno:Nat,cost:Float}. We require that all the labels in a given record term or type be distinct.

The rules for records are given in Figure 11-7. The only one worth noting is E-PROJRCD, where we rely on a slightly informal convention. The rule is meant to be understood as follows: If {li=viiÎ1..n} is a record and lj is the label of its jth field, then {li=viiÎ1..n}.lj evaluates in one step to the jth value, vj. This convention (and the similar one that we used in E-PROJTUPLE) could be eliminated by rephrasing the rule in a more explicit form; however, the cost in terms of readability would be fairly high.


Figure 11-7: Records

11.8.1 Exercise [ ]

Write E-PROJRCD more explicitly, for comparison.

Note that the same "feature symbol," {}, appears in the list of features on the upper-left corner of the definitions of both tuples and products. Indeed, we can obtain tuples as a special case of records, simply by allowing the set of labels to include both alphabetic identifiers and natural numbers. Then when the ith field of a record has the label i, we omit the label. For example, we regard {Bool,Nat,Bool} as an abbreviation for {1:Bool,2:Nat,3:Bool}. (This convention actually allows us to mix named and positional fields, writing {a:Bool,Nat,c:Bool} as an abbreviation for {a:Bool,2:Nat,c:Bool}, though this is probably not very useful in practice.) In fact, many languages keep tuples and records notationally distinct for a more pragmatic reason: they are implemented differently by the compiler.

Programming languages differ in their treatment of the order of record fields. In many languages, the order of fields in both record values and record types has no affect on meaningi.e., the terms {partno=5524,cost=30.27} and {cost=30.27,partno=5524} have the same meaning and the same type, which may be written either {partno:Nat,cost:Float} or {cost:Float, partno:Nat}. Our presentation chooses the other alternative: {partno=5524,cost=30.27} and {cost=30.27,partno=5524} are different record values, with types {partno:Nat,cost:Float} and {cost:Float, partno:Nat}, respectively. In Chapter 15, we will adopt a more liberal view of ordering, introducing a subtype relation in which the types {partno:Nat,cost:Float} and {cost:Float,partno:Nat} are equivalenteach is a subtype of the otherso that terms of one type can be used in any context where the other type is expected. (In the presence of subtyping, the choice between ordered and unordered records has important effects on performance; these are discussed further in §15.6. Once we have decided on unordered records, though, the choice of whether to consider records as unordered from the beginning or to take the fields primitively as ordered and then give rules that allow the ordering to be ignored is purely a question of taste. We adopt the latter approach here because it allows us to discuss both variants.)

11.8.2 Exercise [⋆⋆⋆]

In our presentation of records, the projection operation is used to extract the fields of a record one at a time. Many high-level programming languages provide an alternative pattern matching syntax that extracts all the fields at the same time, allowing some programs to be expressed much more concisely. Patterns can also typically be nested, allowing parts to be extracted easily from complex nested data structures.

We can add a simple form of pattern matching to an untyped lambda calculus with records by adding a new syntactic category of patterns, plus one new case (for the pattern matching construct itself) to the syntax of terms. (See Figure 11-8.)


Figure 11-8: (Untyped) Record Patterns

The computation rule for pattern matching generalizes the let-binding rule from Figure 11-4. It relies on an auxiliary "matching" function that, given a pattern p and a value v, either fails (indicating that v does not match p) or else yields a substitution that maps variables appearing in p to the corresponding parts of v. For example, match({x,y}, {5,true}) yields the substitution [x 5, y true] and match(x, {5,true}) yields [x {5,true}], while match({x}, {5,true}) fails. E-LETV uses match to calculate an appropriate substitution for the variables in p.

The match function itself is defined by a separate set of inference rules. The rule M-VAR says that a variable pattern always succeeds, returning a substitution mapping the variable to the whole value being matched against. The rule M-RCD says that, to match a record pattern {l i=piiÎ1..n} against a record value {li=viiÎ1..n} (of the same length, with the same labels), we individually match each sub-pattern pi against the corresponding value vi to obtain a substitution σi, and build the final result substitution by composing all these substitutions. (We require that no variable should appear more than once in a pattern, so this composition of substitutions is just their union.)

Show how to add types to this system.

  1. Give typing rules for the new constructs (making any changes to the syntax you feel are necessary in the process).

  2. Sketch a proof of type preservation and progress for the whole calculus. (You do not need to show full proofsjust the statements of the required lemmas in the correct order.)



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net