Skip to content

Commit d5b2cf3

Browse files
iitalicsiitalics
committed
a combination of stchang#11 and stchang#12 
1 parent 7acbcbb commit d5b2cf3

File tree

4 files changed

+542
-192
lines changed

4 files changed

+542
-192
lines changed

‎macrotypes/typecheck.rkt‎

Lines changed: 54 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -783,6 +783,20 @@
783783
[(_ e τ) (assign-type #`e #`τ)]))
784784

785785
(begin-for-syntax
786+
;; var-assign :
787+
;; Id (Listof Sym) (StxListof TypeStx) -> Stx
788+
(define (var-assign x seps τs)
789+
(attachs x seps τs #:ev (current-type-eval)))
790+
791+
;; current-var-assign :
792+
;; (Parameterof [Id (Listof Sym) (StxListof TypeStx) -> Stx])
793+
(define current-var-assign
794+
(make-parameter var-assign))
795+
796+
(define current-tyvar-assign
797+
(make-parameter (λ (X)
798+
(mk-tyvar (attach X ':: ((current-type-eval) #'#%type))))))
799+
786800
;; Type assignment macro (ie assign-type) for nicer syntax
787801
(define-syntax (⊢ stx)
788802
(syntax-parse stx
@@ -919,42 +933,58 @@
919933
;; but I'm not sure it properly generalizes
920934
;; eg, what if I need separate type-eval and kind-eval fns?
921935
;; - should infer be moved into define-syntax-category?
922-
(define (infer es #:ctx [ctx null] #:tvctx [tvctx null]
923-
#:tag [tag (current-tag)] ; the "type" to return from es
924-
#:expa [expa expand/df] ; used to expand e
925-
#:tev [tev #'(current-type-eval)] ; type-eval (τ in ctx)
926-
#:key [kev #'(current-type-eval)]) ; kind-eval (tvk in tvctx)
927-
(syntax-parse ctx
928-
[((~or X:id [x:id (~seq sep:id τ) ...]) ...) ; dont expand; τ may reference to tv
929-
#:with (~or (~and (tv:id ...)
936+
;; added: '#:var-stx lst' specifies the variable transformers used to bind
937+
;; ctx in the expansion of the expressions.
938+
;; TODO: delete #:tev and #:kev?
939+
(define (infer es
940+
#:tvctx [tvctx '()]
941+
#:ctx [ctx '()]
942+
#:tag [tag (current-tag)]
943+
#:expa [expa expand/df]
944+
#:tev [tev #'(current-type-eval)]
945+
#:kev [kev #'(current-type-eval)]
946+
#:var-assigns [vas (stx-map default-var-assign ctx)])
947+
(syntax-parse es
948+
[(e ...)
949+
#:with (var-assign ...) vas
950+
#:with (x ...) (stx-map (λ (e) (if (identifier? e) e (stx-car e))) ctx)
951+
952+
; TODO: turnstile syntax no longer uses tvctx.
953+
; is it obsolete? should we just prepend tvctx to ctx?
954+
#:with (~or ([tv:id (~seq tvsep:id tvk) ...] ...)
955+
(~and (tv:id ...)
930956
(~parse ([(tvsep ...) (tvk ...)] ...)
931-
(stx-map (λ _ #'[(::) (#%type)]) #'(tv ...))))
932-
([tv (~seq tvsep:id tvk) ...] ...))
933-
tvctx
934-
#:with (e ...) es
957+
(stx-map (λ _ #'[(::) (#%type)]) #'(tv ...)))))
958+
tvctx
935959
#:with ((~literal #%plain-lambda) tvs+
936960
(~let*-syntax
937961
((~literal #%expression)
938962
((~literal #%plain-lambda) xs+
939963
(~let*-syntax
940964
((~literal #%expression) e+) ... (~literal void))))))
941-
(expa
965+
(expa
942966
#`(λ (tv ...)
943-
(let*-syntax ([tv (make-rename-transformer
967+
(let*-syntax ([tv (make-rename-transformer ; TODO: make this an argument too?
944968
(mk-tyvar
945969
(attachs #'tv '(tvsep ...) #'(tvk ...)
946970
#:ev #,kev)))] ...)
947-
(λ (X ... x ...)
948-
(let*-syntax ([X (make-variable-like-transformer
949-
(mk-tyvar (attach #'X ':: (#,kev #'#%type))))] ...
950-
[x (make-variable-like-transformer
951-
(attachs #'x '(sep ...) #'(τ ...)
952-
#:ev #,tev))] ...)
971+
(λ (x ...)
972+
(let*-syntax ([x (make-variable-like-transformer
973+
var-assign)] ...)
953974
(#%expression e) ... void)))))
954-
(list #'tvs+ #'xs+
955-
#'(e+ ...)
956-
(stx-map (λ (e) (detach e tag)) #'(e+ ...)))]
957-
[([x τ] ...) (infer es #:ctx #`([x #,tag τ] ...) #:tvctx tvctx #:tag tag)]))
975+
(list #'tvs+
976+
#'xs+
977+
#'(e+ ...)
978+
(stx-map (λ (e) (detach e tag)) #'(e+ ...)))]))
979+
980+
(define default-var-assign
981+
(syntax-parser
982+
[X:id
983+
#'((current-tyvar-assign) #'X)]
984+
[(x (~seq sep:id τ) ...)
985+
#'((current-var-assign) #'x '(sep ...) #'(τ ...))]))
986+
987+
958988

959989
;; fns derived from infer ---------------------------------------------------
960990
;; some are syntactic shortcuts, some are for backwards compat

‎turnstile/examples/linear.rkt‎

Lines changed: 200 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,200 @@
1+
#lang turnstile
2+
3+
(provide (type-out Unit Int Str Bool -o ⊗ !!)
4+
#%top-interaction #%module-begin require only-in
5+
#%datum begin tup let λ #%app if
6+
(rename-out [λ lambda]))
7+
8+
(provide (typed-out [+ : (!! (-o Int Int Int))]
9+
[< : (!! (-o Int Int Bool))]
10+
[displayln : (!! (-o Str Unit))]))
11+
12+
(define-base-types Unit Int Str Bool)
13+
(define-type-constructor -o #:arity >= 1)
14+
(define-type-constructor ⊗ #:arity = 2)
15+
(define-type-constructor !! #:arity = 1)
16+
17+
(begin-for-syntax
18+
(require syntax/id-set)
19+
(define (sym-diff s0 . ss)
20+
(for*/fold ([s0 s0])
21+
([s (in-list ss)]
22+
[x (in-set s)])
23+
(if (set-member? s0 x)
24+
(set-remove s0 x)
25+
(set-add s0 x))))
26+
27+
28+
(define unrestricted-type?
29+
(or/c Int? Str? !!?))
30+
31+
32+
(define used-vars (immutable-free-id-set))
33+
34+
(define (lin-var-in-scope? x)
35+
(not (set-member? used-vars x)))
36+
37+
(define (use-lin-var x)
38+
(unless (lin-var-in-scope? x)
39+
(raise-syntax-error #f "linear variable used more than once" x))
40+
(set! used-vars (set-add used-vars x)))
41+
42+
(define (pop-vars xs ts)
43+
(set! used-vars
44+
(for/fold ([uv used-vars])
45+
([x (in-syntax xs)]
46+
[t (in-syntax ts)])
47+
(unless (unrestricted-type? t)
48+
(when (lin-var-in-scope? x)
49+
(raise-syntax-error #f "linear variable unused" x)))
50+
(set-remove uv x))))
51+
52+
53+
54+
(define scope-stack '())
55+
56+
(define (save-scope)
57+
(set! scope-stack (cons used-vars scope-stack)))
58+
59+
(define (merge-scope #:fail-msg fail-msg
60+
#:fail-src [fail-src #f])
61+
(for ([x (in-set (sym-diff used-vars (car scope-stack)))])
62+
(raise-syntax-error #f fail-msg fail-src x))
63+
(set! scope-stack (cdr scope-stack)))
64+
65+
(define (swap-scope)
66+
(set! used-vars
67+
(begin0 (car scope-stack)
68+
(set! scope-stack
69+
(cons used-vars (cdr scope-stack))))))
70+
71+
)
72+
73+
74+
(define-typed-syntax #%top-interaction
75+
[(_ . e) ≫
76+
[⊢ e ≫ e- ⇒ τ]
77+
--------
78+
[≻ (#%app- printf- '"~a : ~a\n"
79+
e-
80+
'#,(type->str #'τ))]])
81+
82+
83+
(define-typed-syntax LIN
84+
#:datum-literals [:]
85+
[(_ x- : σ) ≫
86+
#:when (unrestricted-type? #'σ)
87+
--------
88+
[⊢ x- ⇒ σ]]
89+
[(_ x- : σ) ≫
90+
#:do [(use-lin-var #'x-)]
91+
--------
92+
[⊢ x- ⇒ σ]])
93+
94+
(begin-for-syntax
95+
(define (stx-append-map f . lsts)
96+
(append* (apply stx-map f lsts)))
97+
98+
(current-var-assign
99+
(lambda (x seps types)
100+
#`(LIN #,x #,@(stx-append-map list seps types)))))
101+
102+
103+
(define-typed-syntax #%datum
104+
[(_ . n:exact-integer) ≫
105+
--------
106+
[⊢ (#%datum- . n) ⇒ Int]]
107+
[(_ . b:boolean) ≫
108+
--------
109+
[⊢ (#%datum- . b) ⇒ Bool]]
110+
[(_ . s:str) ≫
111+
--------
112+
[⊢ (#%datum- . s) ⇒ Str]]
113+
[(_ . x) ≫
114+
--------
115+
[#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
116+
117+
118+
(define-typed-syntax begin
119+
[(_ e ... e0) ≫
120+
[⊢ [e ≫ e- ⇒ _] ... [e0 ≫ e0- ⇒ σ]]
121+
--------
122+
[⊢ (begin- e- ... e0-) ⇒ σ]])
123+
124+
125+
(define-typed-syntax tup
126+
#:datum-literals (!)
127+
[(_ e1 e2) ≫
128+
[⊢ e1 ≫ e1- ⇒ σ1]
129+
[⊢ e2 ≫ e2- ⇒ σ2]
130+
--------
131+
[⊢ (#%app- list- e1- e2-) ⇒ (⊗ σ1 σ2)]]
132+
133+
[(_ ! e1 e2) ≫
134+
#:do [(save-scope)]
135+
[⊢ e1 ≫ e1- ⇒ σ1]
136+
[⊢ e2 ≫ e2- ⇒ σ2]
137+
#:do [(merge-scope #:fail-msg "linear variable may not be used by unrestricted tuple"
138+
#:fail-src this-syntax)]
139+
--------
140+
[⊢ (#%app- list- e1- e2-) ⇒ (!! (⊗ σ1 σ2))]])
141+
142+
143+
(define-typed-syntax let
144+
[(let ([x rhs] ...) e) ≫
145+
[⊢ [rhs ≫ rhs- ⇒ σ] ...]
146+
[[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
147+
#:do [(pop-vars #'(x- ...) #'(σ ...))]
148+
--------
149+
[⊢ (let- ([x- rhs-] ...) e-) ⇒ σ_out]])
150+
151+
152+
(define-typed-syntax λ
153+
#:datum-literals (: !)
154+
; linear function
155+
[(λ ([x:id : ty:type] ...) e) ≫
156+
#:with (σ ...) #'(ty.norm ...)
157+
[[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
158+
#:do [(pop-vars #'(x- ...) #'(σ ...))]
159+
--------
160+
[⊢ (λ- (x- ...) e-) ⇒ (-o σ ... σ_out)]]
161+
162+
; unrestricted function
163+
[(λ ! ([x:id : ty:type] ...) e) ≫
164+
#:do [(save-scope)]
165+
#:with (σ ...) #'(ty.norm ...)
166+
[[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
167+
#:do [(pop-vars #'(x- ...) #'(σ ...))
168+
(merge-scope #:fail-msg "linear variable may not be used by unrestricted function"
169+
#:fail-src this-syntax)]
170+
--------
171+
[⊢ (λ- (x- ...) e-) ⇒ (!! (-o σ ... σ_out))]])
172+
173+
174+
(define-typed-syntax #%app
175+
[(_) ≫
176+
--------
177+
[⊢ (#%app- void-) ⇒ Unit]]
178+
179+
[(#%app fun arg ...) ≫
180+
[⊢ fun ≫ fun- ⇒ σ_fun]
181+
#:with (~or (~-o σ_in ... σ_out)
182+
(~!! (~-o σ_in ... σ_out))
183+
(~post (~fail "expected function type")))
184+
#'σ_fun
185+
[⊢ [arg ≫ arg- ⇐ σ_in] ...]
186+
--------
187+
[⊢ (#%app- fun- arg- ...) ⇒ σ_out]])
188+
189+
190+
(define-typed-syntax if
191+
[(if c e1 e2) ≫
192+
[⊢ c ≫ c- ⇐ Bool]
193+
#:do [(save-scope)]
194+
[⊢ e1 ≫ e1- ⇒ σ]
195+
#:do [(swap-scope)]
196+
[⊢ e2 ≫ e2- ⇐ σ]
197+
#:do [(merge-scope #:fail-msg "linear variable may be unused in certain branches"
198+
#:fail-src this-syntax)]
199+
--------
200+
[⊢ (if- c- e1- e2-) ⇒ σ]])

‎turnstile/examples/tests/linear-tests.rkt‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
#lang s-exp turnstile/examples/linear
2+
3+
(require turnstile/rackunit-typechecking
4+
(only-in racket/base quote))
5+
6+
(check-type #t : Bool)
7+
(check-type 4 : Int)
8+
(check-type () : Unit)
9+
10+
(check-type (tup 1 #t) : (⊗ Int Bool) -> '(1 #t))
11+
(check-type (tup 1 (tup 2 3)) : (⊗ Int (⊗ Int Int)) -> '(1 (2 3)))
12+
13+
(check-type (let ([x 3] [y 4]) y) : Int -> 4)
14+
(check-type (let ([p (tup 1 2)]) p) : (⊗ Int Int) -> '(1 2))
15+
16+
(typecheck-fail (let ([p (tup 1 2)]) ())
17+
#:with-msg "p: linear variable unused")
18+
(typecheck-fail (let ([p (tup 1 2)]) (tup p p))
19+
#:with-msg "p: linear variable used more than once")
20+
21+
(check-type (if #t 1 2) : Int -> 1)
22+
(typecheck-fail (if 1 2 3)
23+
#:with-msg "expected Bool, given Int")
24+
(typecheck-fail (if #t 2 ())
25+
#:with-msg "expected Int, given Unit")
26+
27+
(check-type (let ([p (tup 1 ())]) (if #t p p)) : (⊗ Int Unit))
28+
(typecheck-fail (let ([p (tup 1 ())]) (if #t p (tup 2 ())))
29+
#:with-msg "linear variable may be unused in certain branches")
30+
(typecheck-fail (let ([p (tup 1 ())]) (if #t p (begin p p)))
31+
#:with-msg "p: linear variable used more than once")
32+
33+
34+
(check-type (λ ([x : Int]) (tup x x)) : (-o Int (⊗ Int Int)))
35+
(check-type (λ ([x : (⊗ Int Int)]) x) : (-o (⊗ Int Int) (⊗ Int Int)))
36+
(typecheck-fail (λ ([x : (⊗ Int Int)]) ())
37+
#:with-msg "x: linear variable unused")
38+
39+
(check-type (let ([p (tup 1 2)]) (λ ([x : Int]) p))
40+
: (-o Int (⊗ Int Int)))
41+
42+
(check-type (λ ! ([x : Int]) x) : (!! (-o Int Int)))
43+
(typecheck-fail (let ([p (tup 1 2)]) (λ ! ([x : Int]) p))
44+
#:with-msg "linear variable may not be used by unrestricted function")
45+
46+
47+
(check-type (let ([f (λ ([x : Int] [y : Int]) y)])
48+
(f 3 4))
49+
: Int -> 4)
50+
(check-type + : (!! (-o Int Int Int)))
51+
(check-type (+ 1 2) : Int -> 3)
52+
(check-type (< 3 4) : Bool -> #t)
53+
54+
55+
(check-type (let ([×2 (λ ! ([x : Int]) (+ x x))])
56+
(+ (×2 8)
57+
(×2 9)))
58+
: Int -> 34)
59+
60+
(typecheck-fail (let ([×2 (λ ([x : Int]) (+ x x))])
61+
(+ (×2 8)
62+
(×2 9)))
63+
#:with-msg "×2: linear variable used more than once")

0 commit comments

Comments
 (0)