commit 9d3c55d02b1bf1f1c6958cf7d55011a142edd579
parent 7acbcbb0ccd560a57a6b2b9b541ca09e3d1a2a5e
Author: Alex Knauth <alexander@knauth.org>
Date: Fri, 7 Jul 2017 02:20:36 -0400
add current-var-assign parameter (#12)
* add current-var-assign parameter
* add example of linear language + tests (Based on @iitalics work in pull request #11)
Diffstat:
3 files changed, 277 insertions(+), 3 deletions(-)
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -783,6 +783,16 @@
[(_ e τ) (assign-type #`e #`τ)]))
(begin-for-syntax
+ ;; var-assign :
+ ;; Id (Listof Sym) (StxListof TypeStx) -> Stx
+ (define (var-assign x seps τs)
+ (attachs x seps τs #:ev (current-type-eval)))
+
+ ;; current-var-assign :
+ ;; (Parameterof [Id (Listof Sym) (StxListof TypeStx) -> Stx])
+ (define current-var-assign
+ (make-parameter var-assign))
+
;; Type assignment macro (ie assign-type) for nicer syntax
(define-syntax (⊢ stx)
(syntax-parse stx
@@ -922,7 +932,6 @@
(define (infer es #:ctx [ctx null] #:tvctx [tvctx null]
#:tag [tag (current-tag)] ; the "type" to return from es
#:expa [expa expand/df] ; used to expand e
- #:tev [tev #'(current-type-eval)] ; type-eval (τ in ctx)
#:key [kev #'(current-type-eval)]) ; kind-eval (tvk in tvctx)
(syntax-parse ctx
[((~or X:id [x:id (~seq sep:id τ) ...]) ...) ; dont expand; τ may reference to tv
@@ -948,8 +957,10 @@
(let*-syntax ([X (make-variable-like-transformer
(mk-tyvar (attach #'X ':: (#,kev #'#%type))))] ...
[x (make-variable-like-transformer
- (attachs #'x '(sep ...) #'(τ ...)
- #:ev #,tev))] ...)
+ ((current-var-assign)
+ #'x
+ '(sep ...)
+ #'(τ ...)))] ...)
(#%expression e) ... void)))))
(list #'tvs+ #'xs+
#'(e+ ...)
diff --git a/turnstile/examples/linear-var-assign.rkt b/turnstile/examples/linear-var-assign.rkt
@@ -0,0 +1,200 @@
+#lang turnstile
+
+(provide (type-out Unit Int Str Bool -o ⊗ !!)
+ #%top-interaction #%module-begin require only-in
+ #%datum begin tup let λ #%app if
+ (rename-out [λ lambda]))
+
+(provide (typed-out [+ : (!! (-o Int Int Int))]
+ [< : (!! (-o Int Int Bool))]
+ [displayln : (!! (-o Str Unit))]))
+
+(define-base-types Unit Int Str Bool)
+(define-type-constructor -o #:arity >= 1)
+(define-type-constructor ⊗ #:arity = 2)
+(define-type-constructor !! #:arity = 1)
+
+(begin-for-syntax
+ (require syntax/id-set)
+ (define (sym-diff s0 . ss)
+ (for*/fold ([s0 s0])
+ ([s (in-list ss)]
+ [x (in-set s)])
+ (if (set-member? s0 x)
+ (set-remove s0 x)
+ (set-add s0 x))))
+
+
+ (define unrestricted-type?
+ (or/c Int? Str? !!?))
+
+
+ (define used-vars (immutable-free-id-set))
+
+ (define (lin-var-in-scope? x)
+ (not (set-member? used-vars x)))
+
+ (define (use-lin-var x)
+ (unless (lin-var-in-scope? x)
+ (raise-syntax-error #f "linear variable used more than once" x))
+ (set! used-vars (set-add used-vars x)))
+
+ (define (pop-vars xs ts)
+ (set! used-vars
+ (for/fold ([uv used-vars])
+ ([x (in-syntax xs)]
+ [t (in-syntax ts)])
+ (unless (unrestricted-type? t)
+ (when (lin-var-in-scope? x)
+ (raise-syntax-error #f "linear variable unused" x)))
+ (set-remove uv x))))
+
+
+
+ (define scope-stack '())
+
+ (define (save-scope)
+ (set! scope-stack (cons used-vars scope-stack)))
+
+ (define (merge-scope #:fail-msg fail-msg
+ #:fail-src [fail-src #f])
+ (for ([x (in-set (sym-diff used-vars (car scope-stack)))])
+ (raise-syntax-error #f fail-msg fail-src x))
+ (set! scope-stack (cdr scope-stack)))
+
+ (define (swap-scope)
+ (set! used-vars
+ (begin0 (car scope-stack)
+ (set! scope-stack
+ (cons used-vars (cdr scope-stack))))))
+
+ )
+
+
+(define-typed-syntax #%top-interaction
+ [(_ . e) ≫
+ [⊢ e ≫ e- ⇒ τ]
+ --------
+ [≻ (#%app- printf- '"~a : ~a\n"
+ e-
+ '#,(type->str #'τ))]])
+
+
+(define-typed-syntax LIN
+ #:datum-literals [:]
+ [(_ x- : σ) ≫
+ #:when (unrestricted-type? #'σ)
+ --------
+ [⊢ x- ⇒ σ]]
+ [(_ x- : σ) ≫
+ #:do [(use-lin-var #'x-)]
+ --------
+ [⊢ x- ⇒ σ]])
+
+(begin-for-syntax
+ (define (stx-append-map f . lsts)
+ (append* (apply stx-map f lsts)))
+
+ (current-var-assign
+ (lambda (x seps types)
+ #`(LIN #,x #,@(stx-append-map list seps types)))))
+
+
+(define-typed-syntax #%datum
+ [(_ . n:exact-integer) ≫
+ --------
+ [⊢ (#%datum- . n) ⇒ Int]]
+ [(_ . b:boolean) ≫
+ --------
+ [⊢ (#%datum- . b) ⇒ Bool]]
+ [(_ . s:str) ≫
+ --------
+ [⊢ (#%datum- . s) ⇒ Str]]
+ [(_ . x) ≫
+ --------
+ [#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
+
+
+(define-typed-syntax begin
+ [(_ e ... e0) ≫
+ [⊢ [e ≫ e- ⇒ _] ... [e0 ≫ e0- ⇒ σ]]
+ --------
+ [⊢ (begin- e- ... e0-) ⇒ σ]])
+
+
+(define-typed-syntax tup
+ #:datum-literals (!)
+ [(_ e1 e2) ≫
+ [⊢ e1 ≫ e1- ⇒ σ1]
+ [⊢ e2 ≫ e2- ⇒ σ2]
+ --------
+ [⊢ (#%app- list- e1- e2-) ⇒ (⊗ σ1 σ2)]]
+
+ [(_ ! e1 e2) ≫
+ #:do [(save-scope)]
+ [⊢ e1 ≫ e1- ⇒ σ1]
+ [⊢ e2 ≫ e2- ⇒ σ2]
+ #:do [(merge-scope #:fail-msg "linear variable may not be used by unrestricted tuple"
+ #:fail-src this-syntax)]
+ --------
+ [⊢ (#%app- list- e1- e2-) ⇒ (!! (⊗ σ1 σ2))]])
+
+
+(define-typed-syntax let
+ [(let ([x rhs] ...) e) ≫
+ [⊢ [rhs ≫ rhs- ⇒ σ] ...]
+ [[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
+ #:do [(pop-vars #'(x- ...) #'(σ ...))]
+ --------
+ [⊢ (let- ([x- rhs-] ...) e-) ⇒ σ_out]])
+
+
+(define-typed-syntax λ
+ #:datum-literals (: !)
+ ; linear function
+ [(λ ([x:id : ty:type] ...) e) ≫
+ #:with (σ ...) #'(ty.norm ...)
+ [[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
+ #:do [(pop-vars #'(x- ...) #'(σ ...))]
+ --------
+ [⊢ (λ- (x- ...) e-) ⇒ (-o σ ... σ_out)]]
+
+ ; unrestricted function
+ [(λ ! ([x:id : ty:type] ...) e) ≫
+ #:do [(save-scope)]
+ #:with (σ ...) #'(ty.norm ...)
+ [[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
+ #:do [(pop-vars #'(x- ...) #'(σ ...))
+ (merge-scope #:fail-msg "linear variable may not be used by unrestricted function"
+ #:fail-src this-syntax)]
+ --------
+ [⊢ (λ- (x- ...) e-) ⇒ (!! (-o σ ... σ_out))]])
+
+
+(define-typed-syntax #%app
+ [(_) ≫
+ --------
+ [⊢ (#%app- void-) ⇒ Unit]]
+
+ [(#%app fun arg ...) ≫
+ [⊢ fun ≫ fun- ⇒ σ_fun]
+ #:with (~or (~-o σ_in ... σ_out)
+ (~!! (~-o σ_in ... σ_out))
+ (~post (~fail "expected function type")))
+ #'σ_fun
+ [⊢ [arg ≫ arg- ⇐ σ_in] ...]
+ --------
+ [⊢ (#%app- fun- arg- ...) ⇒ σ_out]])
+
+
+(define-typed-syntax if
+ [(if c e1 e2) ≫
+ [⊢ c ≫ c- ⇐ Bool]
+ #:do [(save-scope)]
+ [⊢ e1 ≫ e1- ⇒ σ]
+ #:do [(swap-scope)]
+ [⊢ e2 ≫ e2- ⇐ σ]
+ #:do [(merge-scope #:fail-msg "linear variable may be unused in certain branches"
+ #:fail-src this-syntax)]
+ --------
+ [⊢ (if- c- e1- e2-) ⇒ σ]])
diff --git a/turnstile/examples/tests/linear-var-assign-tests.rkt b/turnstile/examples/tests/linear-var-assign-tests.rkt
@@ -0,0 +1,63 @@
+#lang s-exp turnstile/examples/linear-var-assign
+
+(require turnstile/rackunit-typechecking
+ (only-in racket/base quote))
+
+(check-type #t : Bool)
+(check-type 4 : Int)
+(check-type () : Unit)
+
+(check-type (tup 1 #t) : (⊗ Int Bool) -> '(1 #t))
+(check-type (tup 1 (tup 2 3)) : (⊗ Int (⊗ Int Int)) -> '(1 (2 3)))
+
+(check-type (let ([x 3] [y 4]) y) : Int -> 4)
+(check-type (let ([p (tup 1 2)]) p) : (⊗ Int Int) -> '(1 2))
+
+(typecheck-fail (let ([p (tup 1 2)]) ())
+ #:with-msg "p: linear variable unused")
+(typecheck-fail (let ([p (tup 1 2)]) (tup p p))
+ #:with-msg "p: linear variable used more than once")
+
+(check-type (if #t 1 2) : Int -> 1)
+(typecheck-fail (if 1 2 3)
+ #:with-msg "expected Bool, given Int")
+(typecheck-fail (if #t 2 ())
+ #:with-msg "expected Int, given Unit")
+
+(check-type (let ([p (tup 1 ())]) (if #t p p)) : (⊗ Int Unit))
+(typecheck-fail (let ([p (tup 1 ())]) (if #t p (tup 2 ())))
+ #:with-msg "linear variable may be unused in certain branches")
+(typecheck-fail (let ([p (tup 1 ())]) (if #t p (begin p p)))
+ #:with-msg "p: linear variable used more than once")
+
+
+(check-type (λ ([x : Int]) (tup x x)) : (-o Int (⊗ Int Int)))
+(check-type (λ ([x : (⊗ Int Int)]) x) : (-o (⊗ Int Int) (⊗ Int Int)))
+(typecheck-fail (λ ([x : (⊗ Int Int)]) ())
+ #:with-msg "x: linear variable unused")
+
+(check-type (let ([p (tup 1 2)]) (λ ([x : Int]) p))
+ : (-o Int (⊗ Int Int)))
+
+(check-type (λ ! ([x : Int]) x) : (!! (-o Int Int)))
+(typecheck-fail (let ([p (tup 1 2)]) (λ ! ([x : Int]) p))
+ #:with-msg "linear variable may not be used by unrestricted function")
+
+
+(check-type (let ([f (λ ([x : Int] [y : Int]) y)])
+ (f 3 4))
+ : Int -> 4)
+(check-type + : (!! (-o Int Int Int)))
+(check-type (+ 1 2) : Int -> 3)
+(check-type (< 3 4) : Bool -> #t)
+
+
+(check-type (let ([×2 (λ ! ([x : Int]) (+ x x))])
+ (+ (×2 8)
+ (×2 9)))
+ : Int -> 34)
+
+(typecheck-fail (let ([×2 (λ ([x : Int]) (+ x x))])
+ (+ (×2 8)
+ (×2 9)))
+ #:with-msg "×2: linear variable used more than once")
