add current-var-assign parameter

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+ ...) 

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-) ⇒ σ]])

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")