adt-row-pe.scrbl (3166B)
1 #lang scribble/manual 2 3 @require["util.rkt" 4 "adt-utils.rkt" 5 scriblib/render-cond 6 (for-label (only-meta-in 0 typed/racket))] 7 @(use-mathjax) 8 9 @title[#:style (with-html5 manual-doc-style) 10 #:version (version-text)]{Path elements (with ρ)} 11 12 @todo{Does this need any change when adding row typing?} 13 14 @cases[@pe #:first-sep "⩴" 15 @acase{…} 16 @acase{@πctor-val @tag*{value of constructor}} 17 @acase{@|ɐ| @tag*{value of field @|ɐ|}}] 18 19 We extend the metafunctions for paths given 20 in@~cite[#:precision "pp. 65 and 75" "tobin-hochstadt_typed_2010"]. The @${ 21 @update} metafunction is used when using filters to restrict the type 22 of a (subpart of a) local variable in the @tt{then} and @tt{else} branches of 23 a conditional. 24 25 @todo{∷ is not defined in@~cite["tobin-hochstadt_typed_2010"], we have to 26 define it.} 27 28 @todo{How should I note cleanly these removals / replacements which refer to 29 an @|ɐ| and its τ or @${v} inside the set of @${@|ɐ|ᵢ}?} 30 31 @todo{Also write down the simple "update" cases for row polymorphism} 32 33 @aligned{ 34 @update(@recordτ[@repeatset{@|ɐ|ᵢ : τᵢ}], σ_{π∷@|ɐ|ⱼ}) 35 &= @recordτ[@${@repeatset{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}} 36 @${@|ɐ|ⱼ : @${@update(τⱼ, σ_π)}}] 37 \\ 38 @update(@recordτ[@repeatset{@|ɐ|ᵢ : τᵢ}], @!{σ}_{π∷@|ɐ|ⱼ}) 39 &= @recordτ[@${@repeatset{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}} 40 @${@|ɐ|ⱼ : @${@update(τⱼ, @!{σ}_π)}}] 41 \\ 42 &\quad @where @|ɐ|ⱼ : τⱼ ∈ @repeatset{@|ɐ|ᵢ : τᵢ}\\ 43 @update(@ctorτ[@κ τ], σ_{π∷@πctor-val}) 44 &= @ctorτ[@κ @${@update(τ, σ_π)}]\\@;TODO: update rule when the π is ɐ or getval 45 } 46 47 @$${ 48 @restrict(@variantτ[@repeatset{τ}], σ) 49 = @variantτ[@repeatset{@restrict(τ,σ)}] 50 } 51 @$${ 52 @cond-element[ 53 [html @${\begin{multline}}] 54 [else @${\begin{multlined}}]] 55 @|restrict|\left( 56 @cond-element[ 57 [html @${\begin{array}{l}}] 58 [else @$|{\begin{array}{@{}l@{}}}|]] 59 @recordτ[@ρf 60 @repeatset{-@|ɐ|ᵢ} 61 @repeatset{-@|ɐ|ⱼ} 62 @repeatset{+@|ɐ|ₗ : τₗ} 63 @repeatset{+@|ɐ|ₘ : τₘ}], 64 \\@; TODO: this does not handle the regular per-field update like above? 65 @recordτ[@ρf 66 @repeatset{-@|ɐ|ᵢ} 67 @repeatset{-@|ɐ|ₖ} 68 @repeatset{+@|ɐ|ₗ : σₗ} 69 @repeatset{+@|ɐ|ₙ : σₙ}]\end{array}\right) 70 \\ 71 = @recordτ[@repeatset{-@|ɐ|ᵢ} 72 @repeatset{-@|ɐ|ⱼ} 73 @repeatset{-@|ɐ|ₖ} 74 @repeatset{+@|ɐ|ₗ : @update(τₗ, σₗ)} 75 @repeatset{+@|ɐ|ₘ : τₘ} 76 @repeatset{+@|ɐ|ₙ : σₙ}] 77 @cond-element[ 78 [html @${\end{multline}}] 79 [else @${\end{multlined}}]] 80 } 81 82 @$${ 83 @where @disjoint-sets( 84 @repeatSet{@|ɐ|ᵢ}, 85 @repeatSet{@|ɐ|ⱼ}, 86 @repeatSet{@|ɐ|ₖ}, 87 @repeatSet{@|ɐ|ₗ}, 88 @repeatSet{@|ɐ|ₘ}, 89 @repeatSet{@|ɐ|ₙ}) 90 } 91 92 where 93 94 @aligned{ 95 @disjoint-sets(@repeated{s}) 96 &= @metatrue @textif ∀ sᵢ, sⱼ ∈ s . i ≠ j ⇒ sᵢ ∩ sⱼ = ∅\\ 97 @disjoint-sets(@repeated{s}) 98 &= @metafalse @otherwise 99 } 100 101 @aligned{ 102 @remove(@variantτ[@repeatset{τ}], σ) &= @variantτ[@repeatset{@remove(τ,σ)}] 103 }