main.rkt (4844B)
1 #lang hyper-literate #:no-auto-require (dotlambda/unhygienic . turnstile/lang) 2 3 @(define (turnstile) @racketmodname[turnstile]) 4 5 @(require racket/require 6 (for-label (prefix-in host: (only-meta-in 0 turnstile/lang)) 7 (prefix-in host: 8 (subtract-in (only-meta-in 1 turnstile/lang) 9 (only-meta-in 0 turnstile/lang))) 10 macrotypes/examples/mlish)) 11 12 @section{Introduction} 13 14 We define our type system as an extension to another language. We could extend 15 one of the many sufficiently capable languages built with @turnstile[]. Here, 16 we will base ourselves on @racketmodname[mlish], a ml-like language 17 implemented with @turnstile[], and provided as part of @turnstile[]'s suite of 18 examples. 19 20 @chunk[<*> 21 (extends macrotypes/examples/mlish)] 22 23 Since @racketmodname[macrotypes/examples/mlish] provides some identifiers which 24 conflict with some racket utilities, we import those with a prefix. 25 26 @chunk[<*> 27 (require racket/require 28 (prefix-in host: turnstile/lang) 29 (for-syntax "aliases.rkt") 30 (for-syntax "stx-sort.rkt") 31 (for-meta 2 syntax/stx) 32 (for-meta 2 "stx-sort.rkt") 33 (for-meta 2 "aliases.rkt"))] 34 35 We define a @racket[Record] type, in which the order of fields is irrelevant. 36 37 @CHUNK[<*> 38 ;;(host:provide (type-out Record)) 39 (host:provide Record (for-syntax ~Record)) 40 41 (define-type-constructor Record* #:arity >= 0 42 #:arg-variances λstx.(make-list (sub1 (stx-length stx)) covariant)) 43 44 (define-type-constructor Field* #:arity = 2 45 #:arg-variances λstx.(make-list (sub1 (stx-length stx)) covariant)) 46 47 (define-syntax (Field stx) 48 (syntax-case stx () 49 [(_ ℓ τ) #`(Field* #,(mk-type #'(quote ℓ)) τ)])) 50 51 (define-syntax Record 52 (syntax-parser 53 [(_ {~sort-seq [{~key ℓ:id} {~literal :} τ] …}) 54 #'(Record* [Field ℓ τ] …)])) 55 56 (begin-for-syntax 57 (define-syntax ~Field 58 (pattern-expander 59 (λ (stx) 60 (syntax-case stx () 61 [(_ ℓ τ) 62 #'[~Field* ({~literal quote} ℓ) τ]])))) 63 64 (define-syntax ~Record 65 (pattern-expander 66 (syntax-parser 67 [(_ [ℓ {~literal :} τ] {~datum ⊤ρ}) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 68 #'(~Record* _ (… …) [~Field ℓ τ] _ (… …))] 69 [(_ {~sort-seq [{~key ℓ} {~literal :} τ] …}) 70 #'(~Record* [~Field ℓ τ] …)]))))] 71 72 The builder form for the @racket[Record] type is @racket[record]. 73 74 @chunk[<*> 75 (host:provide record) 76 (define-typed-syntax 77 (record [ℓ:id {~literal =} e] …) ≫ 78 [⊢ e ≫ e- ⇒ τ] … 79 #:with (tmp …) (generate-temporaries #'(e …)) 80 #:with (~sort [{~key sorted-ℓ} sorted-τ sorted-tmp] …) #'([ℓ τ tmp] …) 81 -------- 82 [⊢ (let ([tmp e] …) 83 (list- (list- 'sorted-ℓ sorted-tmp) …)) 84 ⇒ (Record [sorted-ℓ : sorted-τ] …)])] 85 86 Fields can be accessed via the @racket[getfield] operator. The @racket[i.ℓ] 87 notation will later be introduced, and will reduce to @racket[(getfield i ℓ)]. 88 89 @chunk[<*> 90 (host:provide getfield) 91 (require (for-syntax "same-id-pattern.rkt")) 92 (define-typed-syntax 93 (getfield ℓ:id e) ≫ 94 [⊢ e ≫ e- ⇒ {~or {~Record [{~same-free-id ℓ} : τ] ⊤ρ} <record-err-ℓ>}] 95 -------- 96 [⊢ (car- (assoc- 'ℓ e-)) ⇒ τ])] 97 98 @chunk[<record-err-ℓ> 99 {~and 100 other 101 {~do (type-error 102 #:src #'other 103 #:msg "expected record type containing the field ~a, got: ~a" 104 #'ℓ #'other)}}] 105 106 @chunk[<*> 107 (host:provide :) 108 (define-syntax (: stx) 109 (raise-syntax-error ': "Invalid use of token" stx))] 110 111 We define a quick and dirty @racket[:type] operator, which can be used to 112 print the type of an expression. For now, we simply trigger an error message 113 which should contain the inferred type, unless the type of @racket[e] is an 114 @racket[Int]. 115 116 @chunk[<*> 117 (host:provide :type) 118 (require syntax/macro-testing) 119 (define ann/:type-regexp 120 #px"ann: type mismatch: expected Int, given (.*)\n expression:") 121 (define-syntax-rule (:type e) 122 (with-handlers ([(λ (exn) #true) 123 (λ (exn) 124 (displayln 125 (cadr (regexp-match ann/:type-regexp 126 (exn-message exn)))))]) 127 (convert-compile-time-error (ann e : Int))))] 128 129 @section{Conclusion}