lin.rkt (10449B)
1 #lang turnstile 2 (extends "../ext-stlc.rkt" #:except define if begin let let* letrec λ #%app) 3 4 (provide (for-syntax current-linear-type? 5 linear-type? 6 unrestricted-type? 7 8 linear-mode? 9 linear-scope 10 linear-in-scope? 11 linear-use-var! 12 linear-out-of-scope! 13 linear-merge-scopes! 14 linear-merge-scopes*! 15 16 ;; TODO: should these be in turnstile/mode ? 17 branch-nth 18 branch-then 19 branch-else 20 21 make-empty-linear-mode 22 make-fresh-linear-mode 23 make-linear-branch-mode) 24 25 %%reset-linear-mode 26 27 (type-out Unit Int String Bool -o) 28 #%top-interaction #%module-begin require only-in 29 begin drop 30 #%app #%lin-var 31 λ (rename-out [λ lambda]) 32 let letrec 33 if 34 define 35 ) 36 37 38 (define-type-constructor -o #:arity >= 1) 39 40 41 (begin-for-syntax 42 (require syntax/id-set 43 racket/set 44 racket/generic 45 turnstile/mode) 46 47 (define (fail/multiple-use x) 48 (raise-syntax-error #f "linear variable used more than once" x)) 49 (define (fail/unused x) 50 (raise-syntax-error #f "linear variable unused" x)) 51 (define (fail/unbalanced-branches x) 52 (raise-syntax-error #f "linear variable may be unused in certain branches" x)) 53 (define (fail/unrestricted-fn x) 54 (raise-syntax-error #f "linear variable may not be used by unrestricted function" x)) 55 56 57 ;; this parameter defines the linear-type? function. 58 ;; we defining new types that are linear, modify this 59 ;; parameter like so: 60 ;; (current-linear-type? (or/c MYTYPE? (current-linear-type?))) 61 ;; 62 ;; current-linear-type? : (Parameter (Type -> Bool)) 63 (define current-linear-type? 64 (make-parameter -o?)) 65 66 ;; is the given type [linear|unrestricted]? 67 ;; Type -> Bool 68 (define (linear-type? T) 69 ((current-linear-type?) T)) 70 (define (unrestricted-type? T) 71 (not ((current-linear-type?) T))) 72 73 74 75 ;; mode object to be used during linear typing. 76 ;; the field 'scope' contains a free-id-set of 77 ;; variables that have been used, and therefore 78 ;; can't be used again. 79 (struct linear-mode mode (scope)) 80 81 ;; get the current scope (as described above) 82 ;; based on (current-mode) 83 (define (linear-scope) 84 (linear-mode-scope (current-mode))) 85 86 ;; is the given variable available for use? 87 ;; linear-in-scope? : Id -> Bool 88 (define (linear-in-scope? x) 89 (not (set-member? (linear-scope) x))) 90 91 ;; set the variable to be used in this scope, or raise 92 ;; an error if it's already used. 93 ;; 94 ;; linear-use-var! : Id Type -> void 95 (define (linear-use-var! x T #:fail [fail fail/multiple-use]) 96 (when (linear-type? T) 97 (when (set-member? (linear-scope) x) 98 (fail x)) 99 (set-add! (linear-scope) x))) 100 101 102 ;; call this with the ([x : t] ...) context after introducing variables, 103 ;; to remove those variables from the linear scope 104 ;; 105 ;; linear-out-of-scope! : Ctx -> Void 106 (define (linear-out-of-scope! ctx #:fail [fail fail/unused]) 107 (syntax-parse ctx 108 #:datum-literals (:) 109 [([x : σ] ...) 110 (for ([var (in-syntax #'[x ...])] 111 [T (in-syntax #'[σ ...])] #:when (linear-type? T)) 112 (if (linear-in-scope? var) 113 (fail var) 114 (set-remove! (linear-scope) var)))])) 115 116 ;; linear-merge-scopes! : (or '∪ '∩) FreeIdSet ... -> void 117 (define (linear-merge-scopes! op #:fail [fail fail/unbalanced-branches] . ss) 118 (linear-merge-scopes*! op ss #:fail fail)) 119 120 ;; linear-merge-scopes*! : (or '∪ '∩) (Listof FreeIdSet) -> void 121 (define (linear-merge-scopes*! op ss #:fail [fail fail/unbalanced-branches]) 122 (define s0 123 (case op 124 [(∩) 125 (let ([s0 (set-copy (car ss))]) 126 (for ([s (in-list (cdr ss))]) 127 (set-intersect! s0 s)) 128 (for* ([s (in-list ss)] 129 [x (in-set s)] #:when (not (set-member? s0 x))) 130 (fail x)) 131 s0)] 132 133 [(∪) (apply set-union ss)])) 134 135 (set-clear! (linear-scope)) 136 (set-union! (linear-scope) s0)) 137 138 139 140 ;; a mode that contains submodes, for use 141 ;; in branching (if, cond, etc.) 142 (struct branch-mode mode (sub-modes)) 143 144 ;; for use as `#:submode (branch-nth n)` 145 (define ((branch-nth n) bm) 146 (list-ref (branch-mode-sub-modes bm) n)) 147 (define branch-then (branch-nth 0)) 148 (define branch-else (branch-nth 1)) 149 150 ;; creates a branch-mode with n branches (default: 2) 151 ;; which merges the linear sub-scopes during teardown. 152 ;; see 'if' syntax. 153 ;; 154 ;; make-linear-branch : Int -> BranchMode 155 (define (make-linear-branch-mode [n 2]) 156 (define scopes 157 (for/list ([i (in-range n)]) 158 (set-copy (linear-scope)))) 159 160 (branch-mode void 161 (λ () (linear-merge-scopes*! '∩ scopes)) 162 (for/list ([s (in-list scopes)]) 163 (linear-mode void void s)))) 164 165 166 ;; creates a linear mode that disallows (on teardown) use 167 ;; of variables from outside of the current scope. 168 ;; see unrestricted λ syntax. 169 ;; 170 ;; make-fresh-linear-context : -> linear-mode? 171 (define (make-fresh-linear-mode #:fail [fail fail/unrestricted-fn]) 172 (let ([ls #f]) 173 (linear-mode (λ () (set! ls (set-copy (linear-scope)))) 174 (λ () (linear-merge-scopes! '∩ (linear-scope) ls #:fail fail)) 175 (linear-scope)))) 176 177 178 ;; creates an empty linear mode. 179 ;; 180 ;; make-empty-linear-mode : -> LinearMode 181 (define (make-empty-linear-mode) 182 (linear-mode void void (mutable-free-id-set))) 183 184 (current-mode (make-empty-linear-mode)) 185 186 ) 187 188 ;; this function resets the mode to be an empty 189 ;; linear-mode. this should ONLY be used by tests 190 ;; that screw up the state of current-mode, and 191 ;; need to reset it for the next test. this is because 192 ;; we don't have proper backtracking facilities, so 193 ;; errors in the middle of inference screw up the 194 ;; global state 195 (define-syntax %%reset-linear-mode 196 (syntax-parser 197 [(_) 198 #:do [(current-mode (make-empty-linear-mode))] 199 #'(#%app- void-)])) 200 201 202 203 (define-typed-syntax begin 204 [(begin e ... e0) ≫ 205 [⊢ [e ≫ e- ⇐ Unit] ... [e0 ≫ e0- ⇒ σ]] 206 -------- 207 [⊢ (begin- e- ... e0-) ⇒ σ]] 208 209 [(begin e ... e0) ⇐ σ ≫ 210 [⊢ [e ≫ e- ⇐ Unit] ... [e0 ≫ e0- ⇐ σ]] 211 -------- 212 [⊢ (begin- e- ... e0-)]]) 213 214 215 216 (define-typed-syntax drop 217 [(drop e) ≫ 218 [⊢ e ≫ e- ⇒ _] 219 -------- 220 [⊢ (#%app- void- e-) ⇒ Unit]]) 221 222 223 224 (define-typed-syntax #%app 225 [(_) ≫ 226 -------- 227 [⊢ (#%app- void-) ⇒ Unit]] 228 229 [(#%app fun arg ...) ≫ 230 [⊢ fun ≫ fun- ⇒ σ_fun] 231 #:with (~or (~-o σ_in ... σ_out) 232 (~→ σ_in ... σ_out) 233 (~post (~fail "expected linear function type"))) 234 #'σ_fun 235 [⊢ [arg ≫ arg- ⇐ σ_in] ...] 236 -------- 237 [⊢ (#%app- fun- arg- ...) ⇒ σ_out]]) 238 239 240 241 (define-typed-variable-syntax 242 #:name #%lin-var 243 [(#%var x- : σ) ≫ 244 #:do [(linear-use-var! #'x- #'σ)] 245 ---------- 246 [⊢ x- ⇒ σ]]) 247 248 249 (define-typed-syntax λ 250 #:datum-literals (: !) 251 ;; linear lambda; annotations 252 [(λ ([x:id : T:type] ...) b) ≫ 253 #:with [σ ...] #'[T.norm ...] 254 [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out] 255 #:do [(linear-out-of-scope! #'([x- : σ] ...))] 256 -------- 257 [⊢ (λ- (x- ...) b-) ⇒ (-o σ ... σ_out)]] 258 259 ;; unrestricted lambda; annotations 260 [(λ ! ([x:id : T:type] ...) b) ≫ 261 #:with [σ ...] #'[T.norm ...] 262 #:mode (make-fresh-linear-mode) 263 ([[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out] 264 #:do [(linear-out-of-scope! #'([x- : σ] ...))]) 265 -------- 266 [⊢ (λ- (x- ...) b-) ⇒ (→ σ ... σ_out)]] 267 268 ;; linear lambda; inferred 269 [(λ (x:id ...) b) ⇐ (~-o σ ... σ_out) ≫ 270 #:fail-unless (stx-length=? #'[x ...] #'[σ ...]) 271 (num-args-fail-msg this-syntax #'[x ...] #'[σ ...]) 272 [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇐ σ_out] 273 #:do [(linear-out-of-scope! #'([x- : σ] ...))] 274 -------- 275 [⊢ (λ- (x- ...) b-)]] 276 277 ;; unrestricted lambda; inferred 278 [(λ (x:id ...) b) ⇐ (~→ σ ... σ_out) ≫ 279 #:fail-unless (stx-length=? #'[x ...] #'[σ ...]) 280 (num-args-fail-msg this-syntax #'[x ...] #'[σ ...]) 281 #:mode (make-fresh-linear-mode) 282 ([[x ≫ x- : σ] ... ⊢ b ≫ b- ⇐ σ_out] 283 #:do [(linear-out-of-scope! #'([x- : σ] ...))]) 284 -------- 285 [⊢ (λ- (x- ...) b-)]]) 286 287 288 289 (define-typed-syntax let 290 [(let ([x e] ...) b) ≫ 291 [⊢ [e ≫ e- ⇒ σ] ...] 292 [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out] 293 #:do [(linear-out-of-scope! #'([x- : σ] ...))] 294 -------- 295 [⊢ (let- ([x- e-] ...) b-) ⇒ σ_out]]) 296 297 298 299 (define-typed-syntax letrec 300 [(letrec ([b:type-bind rhs] ...) e ...) ≫ 301 #:fail-when (ormap linear-type? (stx->list #'[b.type ...])) 302 (format "may not bind linear type ~a in letrec" 303 (type->str (findf linear-type? (stx->list #'[b.type ...])))) 304 [[b.x ≫ x- : b.type] ... 305 ⊢ [rhs ≫ rhs- ⇐ b.type] ... 306 [(begin e ...) ≫ e- ⇒ σ_out]] 307 #:do [(linear-out-of-scope! #'([x- : b.type] ...))] 308 -------- 309 [⊢ (letrec- ([x- rhs-] ...) e-) ⇒ σ_out]]) 310 311 312 313 (define-typed-syntax if 314 [(_ c e1 e2) ⇐ σ ≫ 315 [⊢ c ≫ c- ⇐ Bool] 316 #:mode (make-linear-branch-mode 2) 317 ([⊢ [e1 ≫ e1- ⇐ σ] #:submode branch-then] 318 [⊢ [e2 ≫ e2- ⇐ σ] #:submode branch-else]) 319 -------- 320 [⊢ (if- c- e1- e2-)]] 321 322 [(_ c e1 e2) ≫ 323 [⊢ c ≫ c- ⇐ Bool] 324 #:mode (make-linear-branch-mode 2) 325 ([⊢ [e1 ≫ e1- ⇒ σ1] #:submode branch-then] 326 [⊢ [e2 ≫ e2- ⇒ σ2] #:submode branch-else]) 327 -------- 328 [⊢ (if- c- e1- e2-) ⇒ (⊔ σ1 σ2)]]) 329 330 331 332 (define-typed-syntax define 333 #:datum-literals (:) 334 [(define (f [x:id : ty] ...) ret 335 e ...+) ≫ 336 -------- 337 [≻ (define f : (→ ty ... ret) 338 (letrec ([{f : (→ ty ... ret)} 339 (λ ! ([x : ty] ...) 340 (begin e ...))]) 341 f))]] 342 343 [(_ x:id : τ:type e:expr) ≫ 344 #:fail-when (linear-type? #'τ.norm) 345 "cannot define linear type globally" 346 #:with y (generate-temporary #'x) 347 -------- 348 [≻ (begin- 349 (define-syntax x (make-rename-transformer (⊢ y : τ.norm))) 350 (define- y (ann e : τ.norm)))]])