adt-row-e.scrbl (3502B)
1 #lang scribble/manual 2 3 @require["util.rkt" 4 "adt-utils.rkt" 5 (for-label (only-meta-in 0 typed/racket))] 6 @(use-mathjax) 7 8 @title[#:style (with-html5 manual-doc-style) 9 #:version (version-text)]{Expressions (with ρ)} 10 11 We extend the syntax of expressions in typed racket as defined 12 by@~cite[#:precision "pp. 62, 72 and 92" "tobin-hochstadt_typed_2010"] and 13 presented in 14 @secref["from-dissertation-tobin-hochstadt" 15 #:doc '(lib "phc-thesis/scribblings/phc-thesis.scrbl")] 16 by adding expressions related to constructors. The first syntax builds an 17 instance of the constructor with label @|κ| and the value of @${e}. The 18 expression @${(@ctor-pred[@κ] e)} determines whether @${e} is an instance of 19 the constructor with label @|κ|. The expression @${(@ctor-val[@κ] e)} extracts 20 the value stored in an instance of a constructor. 21 22 @cases*[ 23 "e" #:first-sep "⩴" 24 @acase{…} 25 @acase{@ctore[@κ e]@tag*{constructor instance}} 26 @acase{(@ctor-pred[@κ]\ e)@tag*{constructor predicate}} 27 @acase{(@ctor-val[@κ]\ e)@tag*{constructor value access}} 28 @interpar{ 29 We also introduce expressions related to records. The first builds an instance 30 of a record with the given fields. We note that the order in which the fields 31 appear affects the order in which the sub-expressions will be evaluated. 32 However, in the resulting value and in its type, the order of the fields is 33 irrelevant. The second expression tests whether @${e} is an instance of a 34 record with the given fields present. The third expression is similar, but 35 allows any number of extra fields to be present, while checking that the @${ 36 -@|ɐ|ⱼ} fields are absent. The fourth expression accesses the value of the @ɐ 37 field stored in the given instance. The fifth expression updates an existing 38 record instance by adding (or replacing) the field @ɐ, while the sixth removes 39 the @ɐ field. 40 } 41 @acase{…} 42 @acase{@recorde[@repeated{@↦e[@${@|ɐ|ᵢ} eᵢ]}]@tag*{record instance}} 43 @acase{(@record-pred[@repeatset{@|ɐ|ᵢ}]\ e)@tag*{record predicate}} 44 @acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ e) 45 @tag*{row-record predicate}}@;added 46 @acase{@record-gete[e @|ɐ|]@tag*{record field access}} 47 @acase{@opwith[e @|ɐ| e]@tag*{record update (new/change field)}} 48 @acase{@opwithout[e @|ɐ|]@tag*{record update (remove field)}} 49 @interpar{ 50 Finally, we define the row-polymorphic abstractions 51 @Λce[(@repeated{@ρc}) e] and @Λfe[(@repeated{@ρf}) e] which bind row 52 type variables hiding constructors and fields respectively. The corresponding 53 instantiation operators are @atc[e @repeated{@ςc}] and @atf[e @repeated{@ςf}]. 54 } 55 @acase{…} 56 @acase{@Λce[(@repeated{@ρc}) e] 57 @tag*{row-polymorphic abstraction (constructors)}}@; new 58 @acase{@Λfe[(@repeated{@ρf}) e] 59 @tag*{row-polymorphic abstraction (fields)}}@; new 60 @acase{@atc[e @repeated{@ςc}] 61 @tag*{row-polymorphic instantiation (constructors)}}@; new 62 @acase{@atf[e @repeated{@ςf}] 63 @tag*{row-polymorphic instantiation (fields)}}]@; new 64 65 @;{ 66 Note: In the @${@record[@repeated{@|ɐ|ᵢ = eᵢ}]} expression, which builds a 67 new record value, the @${@|ɐ|ᵢ} are ordered, and the field order defines the 68 order of evaluation, as indicated by the extensions to the @${E} contexts 69 which is given below. In other uses, the order of fields within the record is 70 irrelevant, i.e. the record can be assimilated to a set of 2-uples, of which 71 the first element is a field name, and the second a value or type. 72 }