adt-row-tausigma.scrbl (3736B)
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)]{Types (with ρ)} 10 11 We introduce two new sorts of types: constructors and records. Constructors 12 are similar to a @typedracket pair whose left element is a symbol, used as a 13 tag. A constructor's tag does not need to be declared beforehand, and can be 14 used on-the-fly. This makes these constructors very similar to the 15 constructors used in @OCAML's polymorphic 16 variants@~cite[#:precision "chapter 6" "minskyRealWorldOCaml"]. Records are 17 similar to the @racket[struct]s available in @typedracket, but the accessor 18 for a field is not prefixed by the name of the struct introducing that field. 19 This means that the same accessor can be used to access the field in all 20 records which contain that field, whereas a different accessor would be needed 21 for each struct type in @|typedracket|. We also introduce row-polymorphic 22 abstractions, which allow a single row type variable to range over several 23 constructors or fields. 24 25 @cases["σ,τ" #:first-sep "⩴" 26 @acase{…} 27 @acase{@ctorτ[@κof[τ]]@tag*{constructor}} @; same 28 @acase{@recordτ[@ςf]@tag*{possibly row-polymorphic record}} @; changed 29 @acase{@∀c[(@repeated{@ρc}) τ] 30 @tag*{row-polymorphic abstraction (constructors)}} @; new 31 @acase{@∀f[(@repeated{@ρf}) τ] 32 @tag*{row-polymorphic abstraction (fields)}}] @; new 33 34 @; new↓ 35 36 We further define variants as a subset of the unions allowed by @|typedracket| 37 (including unions of the constructors defined above). Variants are equivalent 38 to the union of their cases, but guarantee that pattern matching can always be 39 performed (for example, it is not possible in @|typedracket| to distinguish 40 the values of two function types present in the same union, and it is 41 therefore impossible to write a pattern matching expression which handles the 42 two cases differently). Additionally, constraints on the absence of some 43 constructors in the row type can be specified on variants. 44 45 @cases["σ,τ" #:first-sep "⩴" 46 @acase{…} 47 @acase{@variantτ[@ςf] 48 @tag*{possibly row-polymorphic variant}}] @; new/changed 49 50 A variant acts as the union of multiple constructor types. The variant type 51 can also contain a row type variable ranging over constructors. A variant 52 containing a row type variable will normally contain all the constructors used 53 to instantiate that row. The constructors which are explicitly marked as 54 omitted using the syntax @${-@|κ|} are however removed from the row if present 55 within, and the constructors explicitly marked as present using the syntax @${ 56 +@κof[τ]} will always be members of the variant. If such a constructor was 57 present in the row with a different type, it is replaced by a constructor 58 wrapping a value of the explicitly specified type. 59 60 @cases[@ςc #:first-sep "⩴" 61 @acase{@repeatset{@κof[τ]}@tag*{fixed constructors}} 62 @acase{@|ρc|\ @repeatset{-@|κ|ᵢ}\ @repeatset{+@κof[ⱼ τⱼ]} 63 @tag*{row without some ctors, with extra ctors}}] 64 65 Similarly, records can contain a set of fields. It is also possible to use a 66 row type variable ranging over constructors. The syntax @${-@|ɐ|} indicates a 67 field which could be present in the row and but will not be present in the 68 record type, and the syntax @${+@|ɐ|:τ} indicates a field which will always be 69 present, as well as its type. 70 71 @cases[@ςf #:first-sep "⩴" 72 @acase{@repeatset{@|ɐ|:τ}@tag*{fixed fields}} 73 @acase{@|ρf|\ @repeatset{-@|ɐ|ᵢ}\ @repeatset{+@|ɐ|ⱼ:τⱼ} 74 @tag*{row without some fields, with extra fields}}]