trivial.rkt (13668B)
1 #lang turnstile 2 (require (prefix-in tr: typed/racket)) 3 4 ;; This file tries to extend Ben Greenman's trivial package with lambdas 5 ;; see tests/trivial-test.rkt for examples 6 7 ;; TODO: 8 ;; ) do I need separate → and CCs types, both with constraints? 9 ;; - yes? 10 ;; - → is for introducing constraints 11 ;; - and CCs is for propagating them 12 ;; 13 ;; ) why doesnt eval-syntax work with quote? 14 15 ;; NOTES: 16 ;; - using inference algorithm similar to turnstile/examples/infer 17 ;; - tyvars flow down 18 ;; - types, constraints, and tyvar mappings flow up 19 ;; - currently, type variables must be numbers 20 21 (provide Any Int Vec 22 (rename-out [datum/tc #%datum] 23 [app/tc #%app]) 24 λ tr:λ tr:Any define begin let 25 (typed-out 26 [make-vector : (→ (N) [] (Int N) (Vec N))] 27 [vector-ref 28 : (→ (M N) 29 [[(<= 0 N) 30 (< N M) 31 "index is out of range, given ~a, valid range: [0, ~a]" 32 ((lambda (x) x) N) (sub1 M)]] 33 (Vec M) (Int N) Any)] 34 [build-vector 35 : (→ (P) 36 [] 37 (Int P) Any (Vec P))] 38 ;; using different tyvars, to make debugging easier to read 39 [add1 40 : (→ (A) 41 [] 42 (Int A) (Int (+ A 1)))] 43 [sub1 44 : (→ (B) 45 [] 46 (Int B) (Int (- B 1)))] 47 [+ 48 : (→ (C D) 49 [] 50 (Int C) (Int D) (Int (+ C D)))] 51 [- 52 : (→ (E F) 53 [] 54 (Int E) (Int F) (Int (- E F)))]) 55 procedure?) 56 57 (define-base-type Any) ; different from tr:Any 58 (define-internal-type-constructor Vec) 59 (define-syntax Vec 60 (syntax-parser 61 [(_ n) ; n = (quote _) = length of vec; can be numeric expr 62 (mk-type #'(Vec- n))])) 63 (define-internal-type-constructor Int) 64 (define-syntax Int 65 (syntax-parser 66 [(_ n) ; n = (quote _) = length of vec; can be numeric expr 67 (mk-type #'(Int- n))])) 68 69 (define-internal-binding-type →) 70 (define-syntax (→ stx) 71 (syntax-parse stx 72 [(_ (X:id ...) ; tyvars 73 [C ...] ; constraints 74 ty_in ... ty_out) 75 #'(→- (X ...) [void C ...] ty_in ... ty_out)])) 76 77 ;; TODO: pattern expander for MaybeCCs 78 (define-internal-binding-type CCs) 79 (define-syntax (CCs stx) 80 (syntax-parse stx 81 [(_ (X:id ...) ; tyvars 82 [C ...] ; constraints 83 [B ...] ; leftover binding constraints 84 ty) 85 #'(CCs- (X ...) [void C ...] [void B ...] ty)])) 86 87 ;; redefine some parameters --------------------------------------------------- 88 (begin-for-syntax 89 ;; eval for constraints 90 (define (eval-C stx) 91 ; (displayln "evaling:") 92 ; (displayln stx) 93 ; (pretty-print (stx->datum stx)) 94 ;; TODO: eval-syntax does not work due to quoting err, e.g.: 95 ; quote: unbound identifier in the transformer environment; 96 ; also, no #%app syntax transformer is bound 97 ;; - using eval for now 98 (parameterize ([current-namespace (make-base-namespace)]) 99 (define res 100 (with-handlers ([exn? 101 (lambda (e) #;(displayln e) stx)]) 102 (eval (syntax->datum stx)))) 103 ; (displayln res) 104 res)) 105 106 ;; current-typecheck-relation 107 ;; go under CCs if necessary 108 (define old-type=? (current-type=?)) 109 (define (new-type=? t1 t2) ; extend to literals 110 ;; (printf "t1: ~a\n" (syntax->datum t1)) 111 ;; (printf "t2: ~a\n" (syntax->datum t2)) 112 (or (Any? t2) 113 (old-type=? t1 t2) 114 (equal? (syntax-e t1) (syntax-e t2)) 115 ;; unwrap CCs if necessary 116 (syntax-parse (list t1 t2) 117 [((~CCs _ _ _ t1*) _) 118 ((current-type=?) #'t1* t2)] 119 [(_ (~CCs _ _ _ t2*)) 120 ((current-type=?) t1 #'t2*)] 121 [_ #f]))) 122 (current-type=? new-type=?) 123 (current-typecheck-relation new-type=?) 124 125 ;; current-type? 126 ;; TODO: disabling type validation for now 127 (current-type? (lambda _ #t)) 128 129 ;; current-type-eval 130 ;; reduce numberic expressions when possible 131 (define old-teval (current-type-eval)) 132 (define (new-teval t) 133 (define t+ (old-teval t)) 134 (syntax-parse t+ 135 [(~Int (_ e:integer)) t+] ; already reduced 136 [(~Int e) 137 #:with e- (eval-C #'e) 138 (if (typecheck? #'e #'e-) ; couldnt reduce 139 t+ 140 ((current-type-eval) #'(Int (#%datum- . e-))))] 141 [(~CCs a b c (~Int (_ e:integer))) t+] ; already reduced 142 [(~CCs a b c (~Int e)) 143 #:with e- (eval-C #'e) 144 (if (typecheck? #'e #'e-) ; couldnt reduce 145 t+ 146 ((current-type-eval) #'(CCs- a b c (Int (#%datum- . e-)))))] 147 [_ t+])) 148 (current-type-eval new-teval) 149 150 ;; type inference helpers --------------------------------------------------- 151 ;; A "B" is a type binding, eg (X ty) or (ty X) 152 ;; returns a stx list of Bs 153 ;; TODO: add fall through case 154 (define (unify t expected-t) 155 ; (printf "unifying:\n~a\nand\n~a\n" 156 ; (syntax->datum t) 157 ; (syntax->datum expected-t)) 158 (syntax-parse (list t expected-t) 159 [(_ ~Any) #f] 160 [((~CCs _ _ _ t1) _) 161 (unify #'t1 expected-t)] 162 [(_ (~CCs _ _ _ t2)) 163 (unify t #'t2)] 164 [((~Int n) (~Int m)) 165 (unify #'n #'m)] 166 [((~Vec n) (~Vec m)) 167 (unify #'n #'m)] 168 [(t X:id) #'(X t)] 169 [(X:id t) #'(X t)])) 170 (define (unifys ts expected-ts) 171 (filter 172 (lambda (x) x) ; filter out #f 173 (stx-map unify ts expected-ts))) 174 175 ;; Bs should be listof either (Y ty) or (ty Y) 176 ;; returns ty (when X = Y), or #f 177 (define (lookup1 X Bs) 178 (let L ([Bs (stx->list Bs)]) 179 (if (null? Bs) 180 #f 181 (syntax-parse (car Bs) 182 [(Y:id t) 183 #:when (free-identifier=? #'Y X) 184 #'t] 185 [(_ Y:id t) ; expanded version 186 #:when (free-identifier=? #'Y X) 187 #'t] 188 [_ (L (cdr Bs))])))) 189 ;; returns (as list): 190 ;; - list of unsolved Xs 191 ;; - list of solved Xs 192 ;; - tys for solved Xs 193 (define (lookup Xs Bs) 194 (define (lookupX X) (lookup1 X Bs)) 195 (let L ([Xs (stx->list Xs)] 196 [unsolved null] 197 [solved null] 198 [tys-solved null]) 199 (if (null? Xs) 200 (list (reverse unsolved) 201 (reverse solved) 202 (reverse tys-solved)) 203 (let ([res (lookupX (car Xs))]) 204 (if res 205 (L (cdr Xs) 206 unsolved 207 (cons (car Xs) solved) 208 (cons res tys-solved)) 209 (L (cdr Xs) 210 (cons (car Xs) unsolved) 211 solved tys-solved)))))) 212 (define (append-Bs Bss) 213 ; (printf "appending\n") 214 ; (pretty-print (syntax->datum Bss)) 215 (define appended 216 (apply stx-append 217 (stx-map 218 (syntax-parser 219 [((~literal #%plain-app) (~literal void) . rst) 220 #'rst] 221 [rst #'rst]) 222 Bss))) 223 ; (printf "appended\n") 224 ; (pretty-print (stx->datum appened)) 225 appended) 226 ;; prune out solved entries 227 (define (prune-Bs Bs) 228 (filter ; drop #fs 229 (lambda (x) x) 230 (stx-map 231 (syntax-parser 232 [(t1 t2) #:when (typecheck? #'t1 #'t2) #f] 233 [b #'b]) 234 Bs))) 235 236 ;; A "C" is a stx obj that evals to a boolean 237 ;; - function types may additionally specify a list of Cs 238 ;; and they are checked when the fn is applied 239 240 ;; Constraint expr-stx -> Constraint or #t or type error 241 (define (check-C C src-e) 242 (syntax-parse C 243 [(_ e ... (_ msg:str) msg-e ...) 244 (or (and (eval-C #'(and e ...)) 245 C) 246 (type-error 247 #:src src-e 248 #:msg (apply format (syntax-e #'msg) 249 (map 250 ;; this is here bc, due to the "and", 251 ;; constraint may fail before all the tyvars 252 ;; are inferred 253 ;; TODO: improve err msg in this case 254 (lambda (s) 255 (if (syntax? s) 256 (syntax->datum s) 257 s)) 258 (stx-map eval-C #'(msg-e ...))))))] 259 [_ C])) 260 (define (check-Cs Cs e) 261 (filter 262 syntax? 263 (stx-map 264 (lambda (c) (check-C c e)) 265 (stx-cddr Cs)))) ; cddr drops app, void 266 (define (append-Cs Css) 267 (apply 268 append 269 (list #'#%app #'void) 270 (stx-map 271 (syntax-parser 272 [(_ _ . rst) ; drop app void 273 #'rst]) 274 Css))) 275 ) 276 277 ;; λ -------------------------------------------------------------------- 278 ;; no annotations allowed 279 ;; type of lambda inferred from lambda body (as much as possible) 280 (define-typed-syntax λ #:datum-literals (:) 281 [(_ ((~and (~or (~and x:id (~parse ty #'tr:Any)) 282 [x:id : ty])) ...) 283 . es) ≫ 284 #:with (X ...) (generate-temporaries #'(x ...)) 285 [([X ≫ X- :: #%type] ...) ([x ≫ x- : X] ...) 286 ⊢ (begin . es) ≫ e- ⇒ τ_out] 287 ;; TODO: investigate why this extra syntax-local-introduce is needed? 288 #:with τ_out* (syntax-local-introduce #'τ_out) 289 #:with (~or (~CCs Ys Cs Bs τ_out**) 290 (~and τ_out** 291 (~parse (Ys Cs Bs) 292 #'(() (#%app void) (#%app void))))) 293 #'τ_out* 294 ; #:when (begin (displayln "Bs:") 295 ; (stx-map 296 ; (compose pretty-print syntax->datum) 297 ; (stx-cddr #'Bs))) 298 #:with (unsolved solved solved-tys) 299 (lookup #'(X- ...) (stx-cddr #'Bs)) 300 ; #:when (begin (printf "unsolved: ~a\n" (syntax->datum #'unsolved))) 301 ; #:when (begin (printf "solved: ~a\n" (syntax->datum #'solved))) 302 #:with (ty-arg ...) 303 (stx-map 304 (lambda (x) 305 (if (stx-member x #'unsolved) 306 x 307 (cdr 308 (stx-assoc x (stx-map cons #'solved #'solved-tys))))) 309 #'(X- ...)) 310 ; #:when (begin 311 ; (printf "lambda type:\n") 312 ; (pretty-print 313 ; (syntax->datum #'(→- Ys Cs ty-arg ... τ_out**)))) 314 ------- 315 [⊢ (tr:λ ([x- tr:: ty] ...) e-) 316 ⇒ (→- Ys Cs ty-arg ... τ_out**)]]) 317 318 ;; #%app -------------------------------------------------------------------- 319 (define-typed-syntax app/tc 320 [(_ e_fn e_arg ...) ≫ 321 ; #:when (begin (displayln "applying: ----------------------") 322 ; (displayln (syntax->datum #'e_fn))) 323 ;; TODO: propagate constraints from the function expression 324 [⊢ e_fn ≫ e_fn- ⇒ (~→ Xs Cs τ_in ... τ_out)] 325 ; #:when (begin (displayln "fn type:") 326 ; (pretty-print (syntax->datum #'(→ Xs Cs τ_in ... τ_out)))) 327 ;; TODO: create pattern expander for maybe-ccs 328 [⊢ e_arg ≫ e_arg- 329 ⇒ (~or (~CCs Xs-arg Cs-arg Bs-arg τ_arg) 330 (~and τ_arg 331 (~parse (Xs-arg Cs-arg Bs-arg) 332 #'(() (#%app void) ()))))] 333 ... 334 ; #:when (begin (displayln "ty-args:") 335 ; (pretty-print (syntax->datum #'(τ_arg ...)))) 336 #:with Bs (unifys #'(τ_arg ...) #'(τ_in ...)) 337 #:with (unsolved solved tys-solve) (lookup #'Xs #'Bs) 338 ; #:when (begin 339 ; (displayln "solved:") 340 ; (displayln (syntax->datum #'solved)) 341 ; (displayln (syntax->datum #'tys-solve))) 342 #:with (Cs* Bs* ty-in* ... ty-out*) 343 (substs #'tys-solve #'solved #'(Cs Bs τ_in ... τ_out)) 344 #:with Bs** (prune-Bs #'Bs*) 345 ; #:when (begin (displayln "checking Cs:") 346 ; (pretty-print (syntax->datum #'Cs*))) 347 #:with remaining-Cs (check-Cs #'Cs* this-syntax) 348 ; #:when (printf "remaining Cs: ~a\n" 349 ; (syntax->datum #'remaining-Cs)) 350 #:with ty-out** 351 #`(CCs #,(stx-apply stx-append #'(unsolved Xs-arg ...)) 352 remaining-Cs 353 #,(append-Bs #'(Bs** Bs-arg ...)) 354 ty-out*) 355 ; #:when (begin 356 ; (displayln "app out type:") 357 ; (pretty-print (syntax->datum #'ty-out**)) 358 ; (displayln "end apply ---------------------------")) 359 -------- 360 [⊢ (tr:#%app e_fn- e_arg- ...) ⇒ ty-out**]] 361 [(_ e ...) ≫ 362 -------- 363 [⊢ (tr:#%app e ...) ⇒ Any]]) 364 365 ;; #%datum -------------------------------------------------------------------- 366 (define-typed-syntax datum/tc 367 [(_ . n:integer) ≫ 368 ------- 369 [⊢ (tr:#%datum . n) ⇒ (Int (#%datum- . n))]] 370 [(_ . x) ≫ 371 ------- 372 [⊢ (tr:#%datum . x) ⇒ Any]]) 373 374 (define-typed-syntax procedure? 375 [(_ e) ≫ 376 [⊢ e ≫ e- ⇒ _] 377 ------- 378 [⊢ (tr:procedure? e-) ⇒ Any]]) 379 380 381 ;; TODO: resolve clash between TR and my annotations 382 ;; currently, no annotations allowed 383 (define-typed-syntax define 384 [(_ x:id e) ≫ 385 [⊢ e ≫ e- ⇒ ty] 386 #:with x* (generate-temporary) 387 ---------- 388 [≻ (begin- 389 (tr:define-syntax x 390 (make-rename-transformer (⊢ x* : ty))) 391 (tr:define x* e-))]] 392 [(_ (f b ...) . es) ≫ 393 [⊢ (λ (b ...) (begin . es)) ≫ fn- ⇒ ty-f] 394 #:with g (generate-temporary #'f) 395 -------- 396 [≻ (begin- 397 (tr:define-syntax f 398 (make-rename-transformer (⊢ g : ty-f))) 399 (tr:define g fn-))]]) 400 401 (define-typed-syntax begin 402 [(_ e_unit ... e) ≫ 403 [⊢ e_unit ≫ e_unit- ⇒ _] ... 404 [⊢ e ≫ e- ⇒ τ_e] 405 -------- 406 [⊢ (tr:begin e_unit- ... e-) ⇒ τ_e]]) 407 408 (define-typed-syntax let 409 [(_ ([x e] ...) . es) ≫ 410 [⊢ e ≫ e- ⇒ τ_x] ... 411 [[x ≫ x- : τ_x] ... ⊢ (begin . es) ≫ e_body- ⇒ τ_body] 412 -------- 413 [⊢ (tr:let ([x- e-] ...) e_body-) ⇒ τ_body]] 414 [(_ . rst) ≫ 415 ------- 416 [⊢ (tr:let . rst) ⇒ X]]) 417