flexible-with-generalized-ctor.hl.rkt (10665B)
1 #lang hyper-literate #:꩜ #:no-auto-require (dotlambda/unhygienic 2 . type-expander/lang) 3 4 ꩜title[#:tag "generalized-flex-ctor"]{Generalised constructor functions for 5 flexible structures} 6 7 ꩜(require hyper-literate/diff1) 8 9 ꩜chunk[<*> 10 (provide builder-τ 11 propagate-τ 12 oracle 13 builder-f) 14 15 (require racket/require 16 (for-syntax (subtract-in racket/base subtemplate/override) 17 syntax/stx 18 racket/list 19 racket/function 20 subtemplate/override) 21 (for-meta 2 racket/base) 22 "binarytree.hl.rkt") 23 24 <propagate-τ> 25 <oracle-τ> 26 <oracle> 27 <builder-τ> 28 <builder-f>] 29 30 We first define the builder function's type. Since this type is rather 31 complex, we define it using a macro. The type expander takes two arguments. 32 The first argument ꩜racket[n] indicates the total number of fields which 33 appear in the program (i.e. on the number of leaves of the generated tree 34 type), and the second argument ꩜racket[m] indicates how many key/value pairs 35 the function accepts. 36 37 ꩜chunk[<builder-τ> 38 (define-type-expander builder-τ 39 (syntax-parser 40 [(_ n m) 41 <builder-τ-with-1> 42 <builder-τ-with-2> 43 <builder-τ-with-3> 44 #'|<builder-function-type″>|]))] 45 46 We start by defining a few syntax pattern variables which will be used in the 47 later definitions. The lists ꩜racket[Nᵢ] and ꩜racket[Mⱼ] range over the field 48 and argument indices, respectively: 49 50 ꩜chunk[<builder-τ-with-1> 51 #:with (Nᵢ …) (range n) 52 #:with (Mⱼ …) (range m)] 53 54 The builder function takes a number of keys and values, and builds a (promise 55 for) a binary tree where the leaves corresponding to those keys contain given 56 value, and other leaves contain ꩜racket[None]. We could write (a simplified 57 form of) the builder function type as follows: 58 59 ꩜chunk[<builder-function-type> 60 (∀ ({?@ Kⱼ Xⱼ} …) 61 (→ (code:comment "; Keys and values:") 62 {?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} … 63 ;; Result type: 64 (BinaryTree (Promise |<Some or None>|) …)))] 65 66 We expect each key ꩜racket[Kⱼ] to be a symbol of the shape ꩜racket[|0|], 67 ꩜racket[|1|], ꩜racket[|2|] and so on: 68 69 ꩜chunk[<builder-τ-with-2> 70 #:with (NSymᵢ …) ((string->symbol (format "~a" Nᵢ)) …) 71 #:with ((NSymⱼᵢ …) …) (map (const (NSymᵢ …)) (Mⱼ …))] 72 73 The type of each leaf of the binary tree should be ꩜racket[(Some Xⱼ)] if a 74 corresponding ꩜racket[Kⱼ] matches the leaf name, and ꩜racket[None] otherwise. 75 76 ꩜chunk[|<Some or None>| 77 (U |<(Some Xⱼ) if Kⱼ = NSymᵢ>| 78 |<None if ∀ k ∈ Kⱼ , k ≠ NSymᵢ>|)] 79 80 This type-level conditional is achieved via a trick involving intersection 81 types. The ꩜racket[Kⱼ] type should be a singleton type containing exactly one 82 of the ꩜racket['NSymᵢ …] symbols. For a given leaf with index ꩜racket[i], if 83 the ꩜racket[Kⱼ] key is the type ꩜racket['NSymᵢ], then the intersection type 84 ꩜racket[(∩ Kⱼ 'NSymᵢ)] is ꩜racket['NSymᵢ]. Conversely, if the ꩜racket[Kⱼ] key 85 is not ꩜racket['NSymᵢ], the intersection will be the bottom type 86 ꩜racket[Nothing]. No values inhabit the bottom type, and Typed Racket can 87 determine that there is no pair whose first (or second) element has the type 88 ꩜racket[Nothing], since no concrete value could be used to construct such a 89 pair. 90 91 ꩜chunk[|<(Some Xⱼ) if Kⱼ = NSymᵢ>| 92 (Pairof (∩ Kᵢⱼ 'NSymᵢⱼ) 93 Xᵢⱼ) 94 …] 95 96 where ꩜racket[Kᵢⱼ], ꩜racket[Xᵢⱼ] and ꩜racket[NSymᵢⱼ] are defined as follows: 97 98 ꩜chunk[<builder-τ-with-3> 99 #:with ((Kᵢⱼ …) …) (map (const #'(Kⱼ …)) (Nᵢ …)) 100 #:with ((Xᵢⱼ …) …) (map (const #'(Xⱼ …)) (Nᵢ …)) 101 #:with ((NSymᵢⱼ …) …) (map λni.(map (const ni) (Xⱼ …)) (NSymᵢ …))] 102 103 We use this fact to construct a pair above. Its first element is either 104 ꩜racket['NSymᵢ] when ꩜racket[Kⱼ] is ꩜racket['NSymᵢ], and ꩜racket[Nothing] 105 otherwise. The second element of the pair contains our expected 106 ꩜racket[(Some Xⱼ)] type, but the whole pair is collapsed to ꩜racket[Nothing] 107 when ꩜racket[Kⱼ] is not ꩜racket['NSymᵢ]. 108 109 We use a similar approach to conditionally produce the ꩜racket[None] element 110 (which we represent as ꩜racket[#f]), but instead of intersecting ꩜racket[Kⱼ] 111 with ꩜racket['NSymᵢ], we intersect it with the complement of ꩜racket['NSymᵢ]. 112 Typed Racket lacks the possibility to negate a type, so we manually compute 113 the complement of ꩜racket['NSymᵢ] in the set of possible keys (that is, 114 ꩜racket['NSymᵢ …]). 115 116 ꩜chunk[<builder-τ-with-3> 117 #:with NSyms (NSymᵢ …) 118 #:with Ms (Mⱼ …) 119 #:with (exceptᵢ …) ((remove NSymᵢ NSyms) …) 120 #:with (((exceptᵢⱼ …) …) …) ((map (const exceptᵢ) Ms) …)] 121 122 If ꩜racket[Kⱼ] is ꩜racket[Nᵢ], then ꩜racket[{∩ Kⱼ {U . exceptᵢ}}] will be 123 ꩜racket[Nothing]. We take the Cartesian product of the intersections by 124 building a ꩜racket[List] out of them. A single occurrence of ꩜racket[Nothing] 125 will collapse the whole list to ꩜racket[Nothing], because the Cartesian 126 product of the empty set and any other set will produce the empty set. 127 128 The resulting type should therefore be ꩜racket[Nothing] only if there is no 129 ꩜racket[Kⱼ] equal to ꩜racket[Nᵢ], and be the list of symbols 130 ꩜racket[(List . exceptᵢ)] otherwise. 131 132 ꩜chunk[|<None if ∀ k ∈ Kⱼ , k ≠ NSymᵢ>| 133 (Pairof #f (List {∩ Kᵢⱼ {U 'exceptᵢⱼ …}} …))] 134 135 This approach relies on the fact that occurrences of ꩜racket[Nothing] within 136 structs and pairs containing collapse the entire struct or pair type to 137 ꩜racket[Nothing]. Unfortunately, current versions of Typed Racket perform this 138 simplification step in some situations but not others: 139 140 ꩜itemlist[ 141 ꩜item{It simplifies polymorphic types when they are defined;} 142 ꩜item{When a polymorphic type is instantiated, the parts which are directly 143 affected by the intersection with a polymorphic type variable are subject to 144 this simplification;} 145 ꩜item{However, occurrences of ꩜racket[Nothing] which occur as a result of 146 instantiating the type variable do not propagate outside of the intersection 147 itself. This means that given the following type: 148 ꩜racketblock[(define-type (Foo A) (U (Pairof (∩ Integer A) String) Boolean))] 149 its instantiation ꩜racket[(Foo Symbol)] will produce the type 150 ꩜racket[(U (Pairof Nothing String) Boolean)], but this type will not be 151 simplified to ꩜racket[(U Nothing Boolean)] or equivalently to 152 ꩜racket[Boolean].}] 153 154 To force Typed Racket to propagate ꩜racket[Nothing] outwards as much as 155 we need, we intersect the whole form with a polymorphic type ꩜racket[A]: 156 157 ꩜hlite[|<builder-function-type′>| 158 {/(∀(+ _ / _ _)(→ _ _ ooo (bt (p + (∩ / _ + A)) / ooo)))} 159 (∀ (A {?@ Kⱼ Xⱼ} …) 160 (→ (code:comment "; Keys and values:") 161 {?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} … 162 ;; Result type: 163 (BinaryTree (Promise (∩ |<Some or None>| A)) …)))] 164 165 The type ꩜racket[propagate-τ] defined below is used to instantiate ꩜racket[A], 166 and is carefully picked so that its intersection will in no way change the 167 result type (i.e. the intersection with ꩜racket[A] will be an identity 168 operation where it is used). In other words, ꩜racket[propagate-τ] has the same 169 shape as the leaves of the binary tree. This intersection however forces the 170 simplification step to be performed on the affected parts once the type is 171 instantiated. 172 173 ꩜chunk[<propagate-τ> 174 (define-type propagate-τ 175 (U (Pairof Symbol Any) 176 (Pairof #f (Listof Symbol))))] 177 178 ꩜;Use chunkref instead of ꩜racket[|<Some or None>|] ? 179 180 The implementation of the builder function will need to convert values with 181 the ꩜racket[|<Some or None>|] type to values of type 182 ꩜racket[(∩ |<Some or None>| A)]. Since the intersection could, in principle, 183 be any subtype of ꩜racket[|<Some or None>|], we request that the caller 184 supplies a proof that the conversion is possible. This proof takes the form of 185 an ꩜racket[oracle] function, which transforms an element with the type 186 ꩜racket[propagate-τ] (which is a supertype of every possible 187 ꩜racket[|<Some or None>|] type) into an element with the type 188 ꩜racket[(∩ A B)], where ꩜racket[B] is the original type of the value to 189 upgrade. 190 191 ꩜chunk[<oracle-τ> 192 (define-type (oracle-τ A) 193 (∀ (B) (→ (∩ B 194 (U (Pairof Symbol Any) 195 (Pairof #f (Listof Symbol)))) 196 (∩ A B))))] 197 198 The oracle does nothing more than return its argument unchanged: 199 200 ꩜chunk[<oracle> 201 (: oracle (oracle-τ propagate-τ)) 202 (define (oracle v) v)] 203 204 We update the builder function type to accept an extra argument for the 205 oracle: 206 207 ꩜hlite[|<builder-function-type″>| 208 {/(∀(_ _ _)(→ + _ _ / _ _ ooo _))} 209 (∀ (A {?@ Kⱼ Xⱼ} …) 210 (→ (code:comment "; Oracle:") 211 (oracle-τ A) 212 (code:comment "; Keys and values:") 213 {?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} … 214 ;; Result type: 215 (BinaryTree (Promise (∩ |<Some or None>| A)) …)))] 216 217 218 219 220 221 ꩜chunk[<builder-f> 222 (define-syntax builder-f 223 (syntax-parser 224 [(_ name n m) 225 <builder-τ-with-1> 226 <builder-τ-with-2> 227 <builder-τ-with-3> 228 <builder-τ-with-4> 229 #'(begin |<builder-function-implementation>|)]))] 230 231 ꩜chunk[<builder-τ-with-4> 232 #:with ((kᵢⱼ …) …) (map (const #'(kⱼ …)) (Nᵢ …)) 233 #:with ((xᵢⱼ …) …) (map (const #'(xⱼ …)) (Nᵢ …))] 234 235 ꩜chunk[<builder-function-implementation> 236 (: name |<builder-function-type″>| #;(builder-τ n m)) 237 (define (name oracle {?@ kⱼ xⱼ} …) 238 (list (delay 239 (cond 240 [((make-predicate 'NSymᵢⱼ) kᵢⱼ) 241 ((inst oracle (Pairof (∩ Kᵢⱼ 'NSymᵢⱼ) Xᵢⱼ)) (cons kᵢⱼ xᵢⱼ))] 242 … 243 [else 244 ((inst oracle (Pairof #f (List (∩ Kᵢⱼ (U 'exceptᵢⱼ …)) …))) 245 (cons #f (list kᵢⱼ …)))])) 246 …))]