created fabUL-like langauge using lin + ext-stlc

closes #21

macrotypes/typecheck.rkt

@@ -783,6 +783,26 @@
    [(_ 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)))
+
+  ;; macro-var-assign : Id -> (Id (Listof Sym) (StxListof TypeStx) -> Stx)
+  ;; generate a function for current-var-assign that expands
+  ;; to an invocation of the macro by the given identifier
+  ;; e.g.
+  ;;   > (current-var-assign (macro-var-assign #'foo))
+  ;;   > ((current-var-assign) #'x '(:) #'(τ))
+  ;;   #'(foo x : τ)
+  (define ((macro-var-assign mac-id) x seps τs)
+    (datum->syntax x `(,mac-id ,x . ,(stx-appendmap list seps τs))))
+
+  ;; 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 +942,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 +967,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/fabul-utils.rkt

@@ -0,0 +1,71 @@
+#lang racket
+(require syntax/parse
+         turnstile/mode
+         (for-syntax syntax/parse syntax/stx racket/syntax)
+         (for-template macrotypes/typecheck
+                       (only-in "lin.rkt"
+                                linear-mode?
+                                make-empty-linear-mode)))
+
+(provide current-language
+         language-name
+         type-converter
+         unrestricted-mode?
+         make-empty-unrestricted-mode
+         L->U
+         U->L
+         )
+
+(struct unrestricted-mode mode (lin-mode))
+
+(define (make-empty-unrestricted-mode)
+  (unrestricted-mode void void (make-empty-linear-mode)))
+
+(define (L->U lin-mode)
+  (unrestricted-mode void void lin-mode))
+
+(define (U->L un-mode)
+  (unrestricted-mode-lin-mode un-mode))
+
+
+(define (current-language)
+  (if (linear-mode? (current-mode))
+      'L
+      'U))
+
+(define (language-name [lang (current-language)])
+  (case lang
+    [(L) "linear"]
+    [(U) "unrestricted"]))
+
+
+; generates function to convert type into language
+; e.g.   (type-converter [ <clauses> ... ]
+;                        [ A  =>  B ]
+;                        [ C  =>  D ]
+;                        <fail-function>)
+(define-syntax type-converter
+  (syntax-parser
+    #:datum-literals (=>)
+    [(_ (stxparse ...)
+        ([from:id => to:id] ...)
+        fail-fn)
+     #:with self (generate-temporary)
+     #:with [(lhs rhs) ...] #'[(from to) ... (to to) ...]
+     #:with [tycon-clause ...]
+     (stx-map (λ (tycon/l tycon/r)
+                (with-syntax ([patn (format-id tycon/l "~~~a" tycon/l)]
+                              [ctor tycon/r]
+                              [t (generate-temporary)]
+                              [s (generate-temporary)])
+                  #'[(patn t (... ...))
+                     #:with [s (... ...)] (stx-map self #'[t (... ...)])
+                     (syntax/loc this-syntax (ctor s (... ...)))]))
+              #'[lhs ...]
+              #'[rhs ...])
+     #'(letrec ([self (syntax-parser
+                        stxparse ...
+                        tycon-clause ...
+                        [(~not (~Any _ . _)) this-syntax]
+                        [_ (fail-fn this-syntax)])])
+         self)]))

turnstile/examples/linear/fabul.rkt

@@ -0,0 +1,241 @@
+#lang turnstile
+(require (for-syntax "fabul-utils.rkt"
+                     turnstile/mode))
+
+(provide begin let let* letrec λ lambda #%app if tup cons nil
+         drop match-list
+         proj isnil head tail list-ref member
+         define
+         %L %U
+         #%module-begin #%top-interaction require
+         (typed-out [= : (→ Int Int Int)]
+                    [< : (→ Int Int Bool)]
+                    [sub1 : (→ Int Int)]
+                    [add1 : (→ Int Int)]
+                    [zero? : (→ Int Bool)]))
+
+; import other languages
+(require (prefix-in U: "../ext-stlc.rkt")
+         (prefix-in U: (except-in "../stlc+cons.rkt" tup proj))
+         (prefix-in U: (only-in "../stlc+tup.rkt" tup proj))
+         (prefix-in L: "lin.rkt")
+         (prefix-in L: "lin+cons.rkt")
+         (only-in "../ext-stlc.rkt" → ~→)
+         (only-in "../stlc+tup.rkt" × ~×)
+         (only-in "../stlc+cons.rkt" List ~List)
+         (only-in "lin+cons.rkt" ⊗ ~⊗ MList ~MList)
+         (only-in "lin+tup.rkt" in-cad*rs)
+         "lin.rkt" #| this includes base types like Int, Unit, etc. |#)
+
+; reuse types
+(reuse Unit Bool Int Float String → #:from "../ext-stlc.rkt")
+(reuse × #:from "../stlc+tup.rkt")
+(reuse List #:from "../stlc+cons.rkt")
+(reuse -o ⊗ MList #:from "lin+cons.rkt")
+
+; reuse forms
+(reuse #%datum ann and or define-type-alias #:from "../ext-stlc.rkt")
+
+
+
+; begin in unrestricted mode
+(begin-for-syntax
+  (current-mode (make-empty-unrestricted-mode)))
+
+
+; dispatch some forms to L: or U: variant, based on [current-language]
+(define-syntax language-dispatch
+  (syntax-parser
+    [(_ [lang ...] form)
+     #:with (form/lang ...) (stx-map (λ (X) (format-id X "~a:~a" X #'form)) #'[lang ...])
+     #'(define-syntax form
+         (syntax-parser
+           [(_ . args)
+            #:when (eq? (current-language) 'lang)
+            (syntax/loc this-syntax
+              (form/lang . args))] ...
+           [_
+            (raise-syntax-error 'form
+                                (format "form not allowed inside ~a language"
+                                        (language-name)))]))]
+
+    [(_ [lang ...] form ...+)
+     #'(begin-
+         (language-dispatch [lang ...] form) ...)]))
+
+(language-dispatch [L U] begin let let* letrec λ lambda #%app if tup cons nil)
+(language-dispatch [L] drop match-list)
+(language-dispatch [U] proj isnil head tail list-ref member)
+
+
+(begin-for-syntax
+  (define (fully-unrestricted? type)
+    (and (unrestricted-type? type)
+         (syntax-parse type
+           [(~Any _ τ ...) (for/and ([t (in-syntax #'[τ ...])])
+                             (fully-unrestricted? t))]
+           [_ #t])))
+
+  (define (fail/type-convert src lang ty)
+    (raise-syntax-error #f (format "cannot convert type ~a into ~a language"
+                                   (type->str ty)
+                                   (language-name lang))
+                        src))
+
+  ; convert-type : Symbol Type -> Type
+  ;  converts a type into a more appropriate variant for the given language
+  (define (convert-type lang type
+                        #:src [fail-src #f]
+                        #:fail [fail (λ (_) (fail/type-convert fail-src lang type))])
+    (define converter
+      (case lang
+        [(L)
+         (type-converter ([σ #:when (linear-type? #'σ) #'σ])
+                         ([List =>  MList]
+                          [×    =>  ⊗]
+                          [→    =>  →]
+                          [-o   =>  -o])
+                         fail)]
+
+        [(U)
+         (type-converter ([τ #:when (fully-unrestricted? #'τ) #'τ])
+                         ([MList =>  List]
+                          [⊗    =>  ×]
+                          [→     =>  →])
+                         fail)]
+
+        [else (error "invalid language" lang)]))
+
+    ((current-type-eval) (converter type)))
+
+  ; convert-syntax : Type Type Syntax -> Syntax
+  ;  creates an expression that wraps the given syntax such that
+  ;  it converts objects from the first type into the second type.
+  ;  the resulting syntax will never evaluate the original syntax twice.
+  ;  e.g.
+  ;    (convert-stx #'(List Int) #'(MList Int) #'x)
+  ;    ->
+  ;    #'(foldr mcons '() x)
+  (define (convert-syntax . args)
+    (syntax-parse args
+      [[τ σ src] #:when (type=? #'τ #'σ) #'src]
+
+      ; convert tuples
+      [[(~or (~⊗ τ ...) (~× τ ...)) (~or (~⊗ σ ...) (~× σ ...)) src]
+       #:with [out ...] (for/list ([cad*r (in-cad*rs #'tmp)]
+                                   [T (in-syntax #'[τ ...])]
+                                   [S (in-syntax #'[σ ...])])
+                          (convert-syntax T S cad*r))
+       #'(let- ([tmp src]) (#%app- list- out ...))]
+
+      ; convert lists
+      [[(~List τ) (~MList σ) src]
+       #:with x+ (convert-syntax #'τ #'σ #'x)
+       #'(#%app- foldr- (λ- (x l) (#%app- mcons- x+ l)) '() src)]
+
+      [[(~MList τ) (~List σ) src]
+       #:with x+ (convert-syntax #'τ #'σ #'x)
+       #'(for/list- ([x (in-mlist src)]) x+)]
+
+      ; convert functions
+      [[(~or (~→ τ ... τ_out) (~-o τ ... τ_out))
+        (~or (~→ σ ... σ_out) (~-o σ ... σ_out))
+        src]
+       #:with (x ...) (stx-map generate-temporary #'[τ ...])
+       #:with (x+ ...) (stx-map convert-syntax #'[σ ...] #'[τ ...] #'[x ...])
+       #:with out (convert-syntax #'τ_out #'σ_out #'(#%app- f x+ ...))
+       #'(let- ([f src]) (λ- (x ...) out))]))
+
+  )
+
+
+; generate barrier crossing macros
+(define-syntax define-barrier
+  (syntax-parser
+    [(_ form LANG A->B)
+     #'(define-typed-syntax form
+         [(_ e) ≫
+          #:when (eq? (syntax-local-context) 'expression)
+          #:fail-when (eq? (current-language) 'LANG)
+                      (format "already in ~a language"
+                              (language-name 'LANG))
+          [⊢ [e ≫ e- ⇒ τ] #:submode A->B]
+          #:with σ (convert-type (current-language) #'τ #:src this-syntax)
+          #:with e-- (convert-syntax #'τ #'σ #'e-)
+          --------
+          [⊢ e-- ⇒ σ]]
+
+         ; expand toplevels using different syntax, bleh
+         [(_ e ...+) ≫
+          #:submode (if (eq? (current-language) 'LANG)
+                        values
+                        A->B)
+            (#:with e- (local-expand #'(begin- e (... ...))
+                                     'top-level
+                                     '()))
+          --------
+          [≻ e-]])]))
+
+(define-barrier %L L U->L)
+(define-barrier %U U L->U)
+
+
+; variable syntax
+(define-typed-variable-syntax
+  #:datum-literals (:)
+  [(_ x- : τ) ≫
+   #:when (eq? (current-language) 'U)
+   #:fail-unless (fully-unrestricted? #'τ)
+   (raise-syntax-error #f "cannot use linear variable from unrestricted language" #'x-)
+   --------
+   [⊢ x- ⇒ τ]]
+
+  [(_ x- : σ) ≫
+   #:when (eq? (current-language) 'L)
+   --------
+   [≻ (#%lin-var x- : σ)]])
+
+; define syntax
+(define-typed-syntax define
+  #:datum-literals (:)
+  [(define (f [x:id : ty] ...) ret
+     e ...+) ≫
+   --------
+   [≻ (define f : (→ ty ... ret)
+        (letrec ([{f : (→ ty ... ret)}
+                  (λ (x ...)
+                    (begin e ...))])
+          f))]]
+
+  [(_ x:id : τ:type e:expr) ≫
+   #:fail-when (linear-type? #'τ.norm)
+               "cannot define linear type globally"
+   #:with y (generate-temporary #'x)
+   --------
+   [≻ (begin-
+        (define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
+        (define- y (ann e : τ.norm)))]])
+
+
+; REPL prints expression types
+; enter :lang=L or :lang=U to switch language in REPL
+(define-typed-syntax #%top-interaction
+  [(_ . d) ≫
+   #:when (regexp-match? #px":lang=L" (~a (syntax-e #'d)))
+   #:do [(when (unrestricted-mode? (current-mode))
+           (current-mode (U->L (current-mode))))]
+   --------
+   [≻ (#%app- void-)]]
+
+  [(_ . d) ≫
+   #:when (regexp-match? #px":lang=U" (~a (syntax-e #'d)))
+   #:do [(when (linear-mode? (current-mode))
+           (current-mode (L->U (current-mode))))]
+   --------
+   [≻ (#%app- void-)]]
+
+  [(_ . e) ≫
+   #:do [(printf "; language: ~a\n" (language-name))]
+   [⊢ e ≫ e- ⇒ τ]
+   --------
+   [≻ (#%app- printf- '"~v : ~a\n" e- '#,(type->str #'τ))]])

turnstile/examples/linear/lin+chan.rkt

@@ -0,0 +1,61 @@
+#lang turnstile/lang
+(extends "lin+tup.rkt")
+
+(provide (type-out InChan OutChan)
+         make-channel channel-put channel-get
+         thread sleep)
+
+(define-type-constructor InChan #:arity = 1)
+(define-type-constructor OutChan #:arity = 1)
+
+(begin-for-syntax
+  (current-linear-type? (or/c InChan? (current-linear-type?))))
+
+
+(define-typed-syntax make-channel
+  [(_ {ty:type}) ≫
+   #:with σ #'ty.norm
+   #:with tmp (generate-temporary)
+   --------
+   [⊢ (let ([tmp (#%app- make-channel-)])
+            (list tmp tmp))
+      ⇒ (⊗ (InChan σ) (OutChan σ))]])
+
+
+(define-typed-syntax channel-put
+  [(_ ch e) ≫
+   [⊢ ch ≫ ch- ⇒ (~OutChan σ)]
+   [⊢ e ≫ e- ⇐ σ]
+   --------
+   [⊢ (channel-put- ch- e-) ⇒ Unit]])
+
+
+(define-typed-syntax channel-get
+  [(_ ch) ≫
+   [⊢ ch ≫ ch- ⇒ (~InChan σ)]
+   #:with tmp (generate-temporary #'ch)
+   --------
+   [⊢ (let ([tmp ch-])
+            (list tmp (channel-get- tmp)))
+      ⇒ (⊗ (InChan σ) σ)]])
+
+
+(define-typed-syntax thread
+  [(_ f) ≫
+   [⊢ f ≫ f- ⇒ (~-o _)]
+   --------
+   [⊢ (void (thread- f-)) ⇒ Unit]])
+
+
+(define-typed-syntax sleep
+  [(_) ≫
+   --------
+   [⊢ (sleep-) ⇒ Unit]]
+
+  [(_ e) ≫
+   [⊢ e ≫ e- ⇒ σ]
+   #:fail-unless (or (Int? #'σ)
+                     (Float? #'σ))
+   "invalid sleep time, expected Int or Float"
+   --------
+   [⊢ (sleep- e-) ⇒ Unit]])

turnstile/examples/linear/lin+cons.rkt

@@ -0,0 +1,80 @@
+#lang turnstile/lang
+(extends "lin+tup.rkt")
+
+(provide (type-out MList MList0)
+         cons nil match-list)
+
+(define-type-constructor MList #:arity = 1)
+(define-base-type MList0)
+
+(begin-for-syntax
+  (current-linear-type? (or/c MList? MList0? (current-linear-type?))))
+
+
+(define-typed-syntax cons
+  #:datum-literals (@)
+
+  ; implicit memory location created
+  [(_ e e_rest) ≫
+   [⊢ e ≫ e- ⇒ σ]
+   [⊢ e_rest ≫ e_rest- ⇐ (MList σ)]
+   --------
+   [⊢ (#%app- mcons- e- e_rest-) ⇒ (MList σ)]]
+
+  ; with memory location given
+  [(_ e e_rest @ e_loc) ≫
+   [⊢ e ≫ e- ⇒ σ]
+   [⊢ e_rest ≫ e_rest- ⇐ (MList σ)]
+   [⊢ e_loc ≫ e_loc- ⇐ MList0]
+   #:with tmp (generate-temporary #'e_loc)
+   --------
+   [⊢ (let- ([tmp e_loc-])
+            (set-mcar!- tmp e-)
+            (set-mcdr!- tmp e_rest-)
+            tmp)
+      ⇒ (MList σ)]])
+
+
+(define-typed-syntax nil
+  [(_ {ty:type}) ≫
+   --------
+   [⊢ '() ⇒ (MList ty.norm)]]
+  [(_) ⇐ (~MList σ) ≫
+   --------
+   [⊢ '()]])
+
+
+(define-typed-syntax match-list
+  #:datum-literals (cons nil @)
+  [(_ e_list
+      (~or [(cons x+:id xs+:id @ l+:id) e_cons+]
+           [(nil) e_nil+]) ...) ≫
+   #:with [(l x xs e_cons)] #'[(l+ x+ xs+ e_cons+) ...]
+   #:with [e_nil] #'[e_nil+ ...]
+
+   ; list
+   [⊢ e_list ≫ e_list- ⇒ (~MList σ)]
+   #:with σ_xs ((current-type-eval) #'(MList σ))
+   #:with σ_l ((current-type-eval) #'MList0)
+
+   #:mode (make-linear-branch-mode 2)
+     (; cons branch
+      #:submode (branch-nth 0)
+        ([[x ≫ x- : σ]
+          [xs ≫ xs- : σ_xs]
+          [l ≫ l- : σ_l]
+          ⊢ e_cons ≫ e_cons- ⇒ σ_out]
+         #:do [(linear-out-of-scope! #'([x- : σ] [xs- : σ_xs] [l- : σ_l]))])
+
+      ; nil branch
+      #:submode (branch-nth 1)
+        ([⊢ [e_nil ≫ e_nil- ⇐ σ_out]]))
+
+   --------
+   [⊢ (let- ([l- e_list-])
+            (if- (null? l-)
+                 e_nil-
+                 (let- ([x- (mcar- l-)]
+                        [xs- (mcdr- l-)])
+                       e_cons-)))
+      ⇒ σ_out]])

turnstile/examples/linear/lin+tup.rkt

@@ -0,0 +1,112 @@
+#lang turnstile/lang
+(extends "lin.rkt")
+
+(provide (type-out ⊗) tup let*)
+(begin-for-syntax (provide in-cad*rs
+                           list-destructure-syntax))
+
+(define-type-constructor ⊗ #:arity >= 2)
+
+(begin-for-syntax
+  (define (num-tuple-fail-msg σs xs)
+    (format "wrong number of tuple elements: expected ~a, got ~a"
+            (stx-length xs)
+            (stx-length σs)))
+
+  (current-linear-type? (or/c ⊗? (current-linear-type?))))
+
+
+(define-typed-syntax tup
+  [(_ e1 e2 ...+) ≫
+   [⊢ e1 ≫ e1- ⇒ σ1]
+   [⊢ e2 ≫ e2- ⇒ σ2] ...
+   --------
+   [⊢ (list- e1- e2- ...) ⇒ (⊗ σ1 σ2 ...)]])
+
+
+(define-typed-syntax let*
+  ; normal let* recursive bindings
+  [(_ ([x:id e_rhs] . xs) . body) ≫
+   [⊢ e_rhs ≫ e_rhs- ⇒ σ]
+   [[x ≫ x- : σ] ⊢ (let* xs . body) ≫ e_body- ⇒ σ_out]
+   #:do [(linear-out-of-scope! #'([x- : σ]))]
+   --------
+   [⊢ (let- ([x- e_rhs-]) e_body-) ⇒ σ_out]]
+
+  ; tuple unpacking with (let* ([(x ...) tup]) ...)
+  [(_ ([(x:id ...) e_rhs] . xs) . body) ≫
+   [⊢ e_rhs ≫ e_rhs- ⇒ (~⊗ σ ...)]
+   #:fail-unless (stx-length=? #'[σ ...] #'[x ...])
+                 (num-tuple-fail-msg #'[σ ...] #'[x ...])
+
+   [[x ≫ x- : σ] ... ⊢ (let* xs . body) ≫ e_body- ⇒ σ_out]
+   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
+
+   #:with tmp (generate-temporary #'e_tup)
+   #:with destr (list-destructure-syntax #'[x- ...] #'tmp #:unsafe? #t
+                                         #'e_body-)
+   --------
+   [⊢ (let- ([tmp e_rhs-]) destr) ⇒ σ_out]]
+
+  [(_ () e) ≫
+   --------
+   [≻ e]]
+
+  [(_ () e ...+) ≫
+   --------
+   [≻ (lin:begin e ...)]])
+
+
+
+(require racket/unsafe/ops)
+
+;; generate infinite sequence of cad*r syntax, e.g.
+;;   (car e) (cadr e) (caddr e) ...
+(define-for-syntax (in-cad*rs e #:unsafe? [unsafe? #f])
+  (make-do-sequence
+   (λ ()
+     (values (λ (s)
+               (if unsafe?
+                   (quasisyntax/loc e (unsafe-car #,s))
+                   (quasisyntax/loc e (car #,s))))
+             (λ (s)
+               (if unsafe?
+                   (quasisyntax/loc e (unsafe-cdr #,s))
+                   (quasisyntax/loc e (cdr #,s))))
+             e
+             #f #f #f))))
+
+
+;; (list-destructure-syntax #'(x y z ...) #'rhs #'body)
+;;   =
+;; (let ([x (car rhs)]
+;;       [y (cadr rhs)]
+;;       [z (caddr rhs)]
+;;       ...)
+;;   body)
+(define-for-syntax (list-destructure-syntax xs rhs body #:unsafe? [unsafe? #f])
+  (with-syntax ([binds (for/list ([c (in-cad*rs rhs #:unsafe? unsafe?)]
+                                  [x (in-syntax xs)])
+                         (list x c))]
+                [body body])
+    (syntax/loc rhs
+      (let- binds body))))
+
+
+
+(module+ test
+  (begin-for-syntax
+    (require  rackunit)
+    (check-equal? (for/list ([c (in-cad*rs #'x)]
+                             [i (in-range 4)])
+                    (syntax->datum c))
+                  '[(car x)
+                    (car (cdr x))
+                    (car (cdr (cdr x)))
+                    (car (cdr (cdr (cdr x))))])
+
+    (check-equal? (syntax->datum
+                   (list-destructure-syntax #'[x y] #'lst #'z #:unsafe? #t))
+                  '(let- ([x (unsafe-car lst)]
+                          [y (unsafe-car (unsafe-cdr lst))])
+                         z))))

turnstile/examples/linear/lin+var.rkt

@@ -0,0 +1,118 @@
+#lang turnstile/lang
+(extends "lin.rkt")
+(require (only-in "lin+tup.rkt" list-destructure-syntax))
+
+(provide ⊕ var match)
+
+(define-internal-type-constructor ⊕/i)
+
+(define-syntax ⊕
+  (syntax-parser
+    [(_ (V:id t ...) ...)
+     (add-orig (mk-type #'(⊕/i- (#%app 'V t ...) ...))
+               this-syntax)]))
+
+(begin-for-syntax
+  (provide ⊕? ~⊕)
+  (define ⊕? ⊕/i?)
+
+  (define (fail/no-variant type V [src V])
+    (raise-syntax-error #f
+       (format "expected type ~a does not have variant named '~a'\n"
+               (type->str type)
+               (stx->datum V))
+       src))
+
+  (define (num-var-args-fail-msg σs xs)
+    (format "wrong number of arguments to variant: expected ~a, got ~a"
+            (stx-length σs)
+            (stx-length xs)))
+
+
+  (define (unvariant type)
+    (syntax-parse type
+      [(~⊕/i ((~literal #%plain-app) ((~literal quote) U) τ ...) ...)
+       #'[(U τ ...) ...]]))
+
+  (define-syntax ~⊕
+    (pattern-expander
+     (λ (stx)
+       (syntax-case stx ()
+         [(_ . pat)
+          (with-syntax ([(x) (generate-temporaries #'(x))])
+            #'(~and x (~⊕/i . _) (~parse pat (unvariant #'x))))]))))
+
+  (define (has-variant? type v)
+    (syntax-parse type
+      [(~⊕ [U . _] ...)
+       (for/or ([u (in-syntax #'[U ...])])
+         (eq? (stx->datum u) (stx->datum v)))]
+      [_ #f]))
+
+  (define (get-variant type v)
+    (syntax-parse type
+      [(~⊕ [U τ ...] ...)
+       (for/first ([u (in-syntax #'[U ...])]
+                   [ts (in-syntax #'[(τ ...) ...])]
+                   #:when (eq? (stx->datum u) (stx->datum v)))
+         ts)]))
+
+  (current-linear-type? (or/c ⊕? (current-linear-type?)))
+  )
+
+
+(define-typed-syntax var
+  [(_ [V:id e ...]) ⇐ σ_var ≫
+   #:when (⊕? #'σ_var)
+   #:fail-unless (has-variant? #'σ_var #'V)
+                 (fail/no-variant #'σ_var #'V this-syntax)
+   #:with [σ ...] (get-variant #'σ_var #'V)
+   #:fail-unless (stx-length=? #'[σ ...] #'[e ...])
+                 (num-var-args-fail-msg #'[σ ...] #'[e ...])
+   [⊢ e ≫ e- ⇐ σ] ...
+   --------
+   [⊢ (list 'V e- ...)]]
+
+  [(_ [V:id e ...] (~datum as) t) ≫
+   --------
+   [≻ (lin:ann (var [V e ...]) : t)]])
+
+
+
+(define-typed-syntax match
+  [(_ e_var [(V:id x:id ...) e_bra] ...) ≫
+   [⊢ e_var ≫ e_var- ⇒ σ_var]
+   #:fail-unless (⊕? #'σ_var)
+   (format "expected type ⊕, given ~a" (type->str #'σ_var))
+
+   #:mode (make-linear-branch-mode (stx-length #'[e_bra ...]))
+     (#:with ([(x- ...) e_bra- σ_bra] ...)
+      (for/list ([q (in-syntax #'([V (x ...) e_bra] ...))]
+                 [i (in-naturals)])
+        (syntax-parse/typecheck q
+         [(V (x ...) e) ≫
+          #:fail-unless (has-variant? #'σ_var #'V)
+                        (fail/no-variant #'σ_var #'V)
+
+          #:with [σ ...] (get-variant #'σ_var #'V)
+          #:fail-unless (stx-length=? #'[σ ...] #'[x ...])
+                        (num-var-args-fail-msg #'[σ ...] #'[x ...])
+
+          #:submode (branch-nth i)
+            ([[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_bra]
+             #:do [(linear-out-of-scope! #'([x- : σ] ...))])
+          --------
+          [≻ [(x- ...) e- σ_bra]]])))
+
+   #:with tmp (generate-temporary)
+   #:with (destr ...) (stx-map (λ (l) (apply list-destructure-syntax (stx->list l)))
+                               #'[([x- ...]
+                                   (cdr tmp)
+                                   e_bra-) ...])
+   --------
+   [⊢ (let ([tmp e_var-])
+        (case (car tmp)
+          [(V) destr] ...
+          [else (printf "~a\n" tmp)
+                (error '"unhandled case: " (car tmp))]))
+      ⇒ (⊔ σ_bra ...)]])

turnstile/examples/linear/lin.rkt

@@ -0,0 +1,350 @@
+#lang turnstile
+(extends "../ext-stlc.rkt" #:except define if begin let let* letrec λ #%app)
+
+(provide (for-syntax current-linear-type?
+                     linear-type?
+                     unrestricted-type?
+
+                     linear-mode?
+                     linear-scope
+                     linear-in-scope?
+                     linear-use-var!
+                     linear-out-of-scope!
+                     linear-merge-scopes!
+                     linear-merge-scopes*!
+
+                     ;; TODO: should these be in turnstile/mode ?
+                     branch-nth
+                     branch-then
+                     branch-else
+
+                     make-empty-linear-mode
+                     make-fresh-linear-mode
+                     make-linear-branch-mode)
+
+         %%reset-linear-mode
+
+         (type-out Unit Int String Bool -o)
+         #%top-interaction #%module-begin require only-in
+         begin drop
+         #%app #%lin-var
+         λ (rename-out [λ lambda])
+         let letrec
+         if
+         define
+         )
+
+
+(define-type-constructor -o #:arity >= 1)
+
+
+(begin-for-syntax
+  (require syntax/id-set
+           racket/set
+           racket/generic
+           turnstile/mode)
+
+  (define (fail/multiple-use x)
+    (raise-syntax-error #f "linear variable used more than once" x))
+  (define (fail/unused x)
+    (raise-syntax-error #f "linear variable unused" x))
+  (define (fail/unbalanced-branches x)
+    (raise-syntax-error #f "linear variable may be unused in certain branches" x))
+  (define (fail/unrestricted-fn x)
+    (raise-syntax-error #f "linear variable may not be used by unrestricted function" x))
+
+
+  ;; this parameter defines the linear-type? function.
+  ;; we defining new types that are linear, modify this
+  ;; parameter like so:
+  ;;   (current-linear-type? (or/c MYTYPE? (current-linear-type?)))
+  ;;
+  ;; current-linear-type? : (Parameter (Type -> Bool))
+  (define current-linear-type?
+    (make-parameter -o?))
+
+  ;; is the given type [linear|unrestricted]?
+  ;; Type -> Bool
+  (define (linear-type? T)
+    ((current-linear-type?) T))
+  (define (unrestricted-type? T)
+    (not ((current-linear-type?) T)))
+
+
+
+  ;; mode object to be used during linear typing.
+  ;; the field 'scope' contains a free-id-set of
+  ;; variables that have been used, and therefore
+  ;; can't be used again.
+  (struct linear-mode mode (scope))
+
+  ;; get the current scope (as described above)
+  ;; based on (current-mode)
+  (define (linear-scope)
+    (linear-mode-scope (current-mode)))
+
+  ;; is the given variable available for use?
+  ;; linear-in-scope? : Id -> Bool
+  (define (linear-in-scope? x)
+    (not (set-member? (linear-scope) x)))
+
+  ;; set the variable to be used in this scope, or raise
+  ;; an error if it's already used.
+  ;;
+  ;; linear-use-var! : Id Type -> void
+  (define (linear-use-var! x T #:fail [fail fail/multiple-use])
+    (when (linear-type? T)
+      (when (set-member? (linear-scope) x)
+        (fail x))
+      (set-add! (linear-scope) x)))
+
+
+  ;; call this with the ([x : t] ...) context after introducing variables,
+  ;; to remove those variables from the linear scope
+  ;;
+  ;; linear-out-of-scope! : Ctx -> Void
+  (define (linear-out-of-scope! ctx #:fail [fail fail/unused])
+    (syntax-parse ctx
+      #:datum-literals (:)
+      [([x : σ] ...)
+       (for ([var (in-syntax #'[x ...])]
+             [T (in-syntax #'[σ ...])] #:when (linear-type? T))
+         (if (linear-in-scope? var)
+             (fail var)
+             (set-remove! (linear-scope) var)))]))
+
+  ;; linear-merge-scopes! : (or '∪ '∩) FreeIdSet ... -> void
+  (define (linear-merge-scopes! op #:fail [fail fail/unbalanced-branches] . ss)
+    (linear-merge-scopes*! op ss #:fail fail))
+
+  ;; linear-merge-scopes*! : (or '∪ '∩) (Listof FreeIdSet) -> void
+  (define (linear-merge-scopes*! op ss #:fail [fail fail/unbalanced-branches])
+    (define s0
+      (case op
+        [(∩)
+         (let ([s0 (set-copy (car ss))])
+           (for ([s (in-list (cdr ss))])
+             (set-intersect! s0 s))
+           (for* ([s (in-list ss)]
+                  [x (in-set s)] #:when (not (set-member? s0 x)))
+             (fail x))
+           s0)]
+
+        [(∪) (apply set-union ss)]))
+
+    (set-clear! (linear-scope))
+    (set-union! (linear-scope) s0))
+
+
+
+  ;; a mode that contains submodes, for use
+  ;; in branching (if, cond, etc.)
+  (struct branch-mode mode (sub-modes))
+
+  ;; for use as `#:submode (branch-nth n)`
+  (define ((branch-nth n) bm)
+    (list-ref (branch-mode-sub-modes bm) n))
+  (define branch-then (branch-nth 0))
+  (define branch-else (branch-nth 1))
+
+  ;; creates a branch-mode with n branches (default: 2)
+  ;; which merges the linear sub-scopes during teardown.
+  ;; see 'if' syntax.
+  ;;
+  ;; make-linear-branch : Int -> BranchMode
+  (define (make-linear-branch-mode [n 2])
+    (define scopes
+      (for/list ([i (in-range n)])
+        (set-copy (linear-scope))))
+
+    (branch-mode void
+                 (λ () (linear-merge-scopes*! '∩ scopes))
+                 (for/list ([s (in-list scopes)])
+                   (linear-mode void void s))))
+
+
+  ;; creates a linear mode that disallows (on teardown) use
+  ;; of variables from outside of the current scope.
+  ;; see unrestricted λ syntax.
+  ;;
+  ;; make-fresh-linear-context : -> linear-mode?
+  (define (make-fresh-linear-mode #:fail [fail fail/unrestricted-fn])
+    (let ([ls #f])
+      (linear-mode (λ () (set! ls (set-copy (linear-scope))))
+                   (λ () (linear-merge-scopes! '∩ (linear-scope) ls #:fail fail))
+                   (linear-scope))))
+
+
+  ;; creates an empty linear mode.
+  ;;
+  ;; make-empty-linear-mode : -> LinearMode
+  (define (make-empty-linear-mode)
+    (linear-mode void void (mutable-free-id-set)))
+
+  (current-mode (make-empty-linear-mode))
+
+  )
+
+;; this function resets the mode to be an empty
+;; linear-mode. this should ONLY be used by tests
+;; that screw up the state of current-mode, and
+;; need to reset it for the next test. this is because
+;; we don't have proper backtracking facilities, so
+;; errors in the middle of inference screw up the
+;; global state
+(define-syntax %%reset-linear-mode
+  (syntax-parser
+    [(_)
+     #:do [(current-mode (make-empty-linear-mode))]
+     #'(#%app- void-)]))
+
+
+
+(define-typed-syntax begin
+  [(begin e ... e0) ≫
+   [⊢ [e ≫ e- ⇐ Unit] ... [e0 ≫ e0- ⇒ σ]]
+   --------
+   [⊢ (begin- e- ... e0-) ⇒ σ]]
+
+  [(begin e ... e0) ⇐ σ ≫
+   [⊢ [e ≫ e- ⇐ Unit] ... [e0 ≫ e0- ⇐ σ]]
+   --------
+   [⊢ (begin- e- ... e0-)]])
+
+
+
+(define-typed-syntax drop
+  [(drop e) ≫
+   [⊢ e ≫ e- ⇒ _]
+   --------
+   [⊢ (#%app- void- e-) ⇒ Unit]])
+
+
+
+(define-typed-syntax #%app
+  [(_) ≫
+   --------
+   [⊢ (#%app- void-) ⇒ Unit]]
+
+  [(#%app fun arg ...) ≫
+   [⊢ fun ≫ fun- ⇒ σ_fun]
+   #:with (~or (~-o σ_in ... σ_out)
+               (~→ σ_in ... σ_out)
+               (~post (~fail "expected linear function type")))
+          #'σ_fun
+   [⊢ [arg ≫ arg- ⇐ σ_in] ...]
+   --------
+   [⊢ (#%app- fun- arg- ...) ⇒ σ_out]])
+
+
+
+(define-typed-variable-syntax
+  #:name #%lin-var
+  [(#%var x- : σ) ≫
+   #:do [(linear-use-var! #'x- #'σ)]
+   ----------
+   [⊢ x- ⇒ σ]])
+
+
+(define-typed-syntax λ
+  #:datum-literals (: !)
+  ;; linear lambda; annotations
+  [(λ ([x:id : T:type] ...) b) ≫
+   #:with [σ ...] #'[T.norm ...]
+   [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
+   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
+   --------
+   [⊢ (λ- (x- ...) b-) ⇒ (-o σ ... σ_out)]]
+
+  ;; unrestricted lambda; annotations
+  [(λ ! ([x:id : T:type] ...) b) ≫
+   #:with [σ ...] #'[T.norm ...]
+   #:mode (make-fresh-linear-mode)
+     ([[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
+      #:do [(linear-out-of-scope! #'([x- : σ] ...))])
+   --------
+   [⊢ (λ- (x- ...) b-) ⇒ (→ σ ... σ_out)]]
+
+  ;; linear lambda; inferred
+  [(λ (x:id ...) b) ⇐ (~-o σ ... σ_out) ≫
+   #:fail-unless (stx-length=? #'[x ...] #'[σ ...])
+                 (num-args-fail-msg this-syntax #'[x ...] #'[σ ...])
+   [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇐ σ_out]
+   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
+   --------
+   [⊢ (λ- (x- ...) b-)]]
+
+  ;; unrestricted lambda; inferred
+  [(λ (x:id ...) b) ⇐ (~→ σ ... σ_out) ≫
+   #:fail-unless (stx-length=? #'[x ...] #'[σ ...])
+                 (num-args-fail-msg this-syntax #'[x ...] #'[σ ...])
+   #:mode (make-fresh-linear-mode)
+     ([[x ≫ x- : σ] ... ⊢ b ≫ b- ⇐ σ_out]
+      #:do [(linear-out-of-scope! #'([x- : σ] ...))])
+   --------
+   [⊢ (λ- (x- ...) b-)]])
+
+
+
+(define-typed-syntax let
+  [(let ([x e] ...) b) ≫
+   [⊢ [e ≫ e- ⇒ σ] ...]
+   [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
+   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
+   --------
+   [⊢ (let- ([x- e-] ...) b-) ⇒ σ_out]])
+
+
+
+(define-typed-syntax letrec
+  [(letrec ([b:type-bind rhs] ...) e ...) ≫
+   #:fail-when (ormap linear-type? (stx->list #'[b.type ...]))
+               (format "may not bind linear type ~a in letrec"
+                       (type->str (findf linear-type? (stx->list #'[b.type ...]))))
+   [[b.x ≫ x- : b.type] ...
+    ⊢ [rhs ≫ rhs- ⇐ b.type] ...
+       [(begin e ...) ≫ e- ⇒ σ_out]]
+   #:do [(linear-out-of-scope! #'([x- : b.type] ...))]
+   --------
+   [⊢ (letrec- ([x- rhs-] ...) e-) ⇒ σ_out]])
+
+
+
+(define-typed-syntax if
+  [(_ c e1 e2) ⇐ σ ≫
+   [⊢ c ≫ c- ⇐ Bool]
+   #:mode (make-linear-branch-mode 2)
+     ([⊢ [e1 ≫ e1- ⇐ σ] #:submode branch-then]
+      [⊢ [e2 ≫ e2- ⇐ σ] #:submode branch-else])
+   --------
+   [⊢ (if- c- e1- e2-)]]
+
+  [(_ c e1 e2) ≫
+   [⊢ c ≫ c- ⇐ Bool]
+   #:mode (make-linear-branch-mode 2)
+     ([⊢ [e1 ≫ e1- ⇒ σ1] #:submode branch-then]
+      [⊢ [e2 ≫ e2- ⇒ σ2] #:submode branch-else])
+   --------
+   [⊢ (if- c- e1- e2-) ⇒ (⊔ σ1 σ2)]])
+
+
+
+(define-typed-syntax define
+  #:datum-literals (:)
+  [(define (f [x:id : ty] ...) ret
+     e ...+) ≫
+   --------
+   [≻ (define f : (→ ty ... ret)
+        (letrec ([{f : (→ ty ... ret)}
+                  (λ ! ([x : ty] ...)
+                    (begin e ...))])
+          f))]]
+
+  [(_ x:id : τ:type e:expr) ≫
+   #:fail-when (linear-type? #'τ.norm)
+               "cannot define linear type globally"
+   #:with y (generate-temporary #'x)
+   --------
+   [≻ (begin-
+        (define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
+        (define- y (ann e : τ.norm)))]])

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

@@ -0,0 +1,75 @@
+#lang s-exp turnstile/examples/linear/fabul
+(require turnstile/rackunit-typechecking)
+
+(%U (define birthday : (× Int Int Int)
+     (tup 10 10 97)))
+
+(%U (check-type birthday : (× Int Int Int)))
+(%L (check-type (%U birthday) : (⊗ Int Int Int) ⇒ (tup 10 10 97)))
+
+(%U (typecheck-fail
+    (%L (let ([bday (%U birthday)]) 0))
+    #:with-msg "bday: linear variable unused"))
+
+(%L (typecheck-fail
+    (let ([x (%U birthday)]) (%U x))
+    #:with-msg "x: cannot use linear variable from unrestricted language"))
+
+(%L (check-type (let ([bday (%U birthday)])
+                  (%U (%L bday)))
+               : (⊗ Int Int Int)))
+
+(%L (check-type (%U (cons 1 (cons 2 (nil {Int}))))
+               : (MList Int)
+               ⇒ (cons 1 (cons 2 (nil)))))
+
+(%U (check-type (%L (cons 1 (cons 2 (nil))))
+               : (List Int)
+               ⇒ (cons 1 (cons 2 (nil {Int})))))
+
+(%L (check-type (let ([f (%U (λ () (cons 1 (nil {Int}))))]) f)
+               : (→ (MList Int))))
+
+(%L (check-type (let ([f (%U (λ () (cons 1 (nil {Int}))))]) (f))
+               : (MList Int)
+               ⇒ (cons 1 (nil))))
+
+
+
+(%L (define (partition [pred : (→ Int Bool)]
+                      [lst : (MList Int)]) (⊗ (MList Int) (MList Int))
+     (match-list lst
+       [(cons x xs @ l)
+        (let* ([(yes no) (partition pred xs)])
+          (if (pred x)
+              (tup (cons x yes @ l) no)
+              (tup yes (cons x no @ l))))]
+       [(nil)
+        (tup (nil {Int}) (nil {Int}))])))
+
+(%L (check-type (partition (λ (n) (< n 3))
+                          (cons 1 (cons 2 (cons 4 (cons 5 (nil))))))
+               : (⊗ (MList Int) (MList Int))
+               ⇒ (tup (cons 1 (cons 2 (nil)))
+                      (cons 4 (cons 5 (nil))))))
+
+
+(%L (define (mqsort [lst : (MList Int)] [acc : (MList Int)]) (MList Int)
+     (match-list lst
+       [(cons piv xs @ l)
+        (let* ([(lt gt) (partition (λ (x) (< x piv)) xs)])
+          (mqsort lt (cons piv (mqsort gt acc) @ l)))]
+       [(nil) acc])))
+
+(%L (check-type (mqsort (cons 4 (cons 7 (cons 2 (cons 1 (nil))))) (nil))
+               : (MList Int)
+               ⇒ (cons 1 (cons 2 (cons 4 (cons 7 (nil)))))))
+
+
+
+(%U (define (qsort [lst : (List Int)]) (List Int)
+     (%L (mqsort (%U lst) (nil)))))
+
+(%U (check-type (qsort (cons 4 (cons 7 (cons 2 (cons 1 (nil {Int}))))))
+               : (List Int)
+               ⇒ (cons 1 (cons 2 (cons 4 (cons 7 (nil {Int})))))))

turnstile/examples/tests/linear/lin+chan-tests.rkt

@@ -0,0 +1,18 @@
+#lang s-exp turnstile/examples/linear/lin+chan
+(require turnstile/rackunit-typechecking)
+
+(check-type
+ (let* ([(c c-out) (make-channel {Int})])
+   (thread (λ () (channel-put c-out 5)))
+   (thread (λ () (channel-put c-out 4)))
+   (let* ([(c1 x) (channel-get c)]
+          [(c2 y) (channel-get c1)])
+     (drop c2)
+     (+ x y)))
+ : Int -> 9)
+
+(typecheck-fail
+ (let* ([(c-in c-out) (make-channel {String})])
+   (thread (λ () (channel-get c-in)))
+   (channel-get c-in))
+ #:with-msg "c-in: linear variable used more than once")

turnstile/examples/tests/linear/lin+cons-tests.rkt

@@ -0,0 +1,28 @@
+#lang s-exp turnstile/examples/linear/lin+cons
+(require turnstile/rackunit-typechecking)
+
+
+(define (length [lst : (MList Int)]) Int
+  (match-list lst
+    [(cons _ xs @ l)
+     (begin (drop l)
+            (add1 (length xs)))]
+    [(nil) 0]))
+
+(check-type (length (cons 9 (cons 8 (cons 7 (nil))))) : Int -> 3)
+
+
+
+(define (rev-append [lst : (MList String)]
+                    [acc : (MList String)]) (MList String)
+  (match-list lst
+    [(cons x xs @ l) (rev-append xs (cons x acc @ l))]
+    [(nil) acc]))
+
+(define (rev [lst : (MList String)]) (MList String)
+  (rev-append lst (nil)))
+
+
+(check-type (rev (cons "a" (cons "b" (cons "c" (nil)))))
+            : (MList String)
+            -> (cons "c" (cons "b" (cons "a" (nil)))))

turnstile/examples/tests/linear/lin+tup-tests.rkt

@@ -0,0 +1,29 @@
+#lang s-exp turnstile/examples/linear/lin+tup
+
+(require turnstile/rackunit-typechecking
+         (only-in racket/base quote))
+
+(check-type (tup 1 #t) : (⊗ Int Bool) -> '(1 #t))
+(check-type (tup 1 2 3) : (⊗ Int Int Int) -> '(1 2 3))
+
+(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 (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")
+
+(check-type (λ ([x : Int]) (tup x x)) : (-o 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 (let* ([x 3] [y x]) y) : Int -> 3)
+(check-type (let* ([(x y) (tup 1 #f)]) x) : Int -> 1)
+(typecheck-fail (let* ([(x y) (tup (tup 1 2) 3)]) y)
+                #:with-msg "x: linear variable unused")

turnstile/examples/tests/linear/lin+var-tests.rkt

@@ -0,0 +1,67 @@
+#lang s-exp turnstile/examples/linear/lin+var
+(require turnstile/rackunit-typechecking)
+
+(check-type (var [left 3]) : (⊕ [left Int] [right String]))
+(check-type (var [right "a"]) : (⊕ [left Int] [right String]))
+
+(typecheck-fail (var [left 3] as (⊕ [yes] [no]))
+                #:with-msg "type \\(⊕ \\(yes\\) \\(no\\)\\) does not have variant named 'left'")
+
+(typecheck-fail (var [left 3] as (⊕ [left Int Int] [right String]))
+                #:with-msg "wrong number of arguments to variant: expected 2, got 1")
+
+(define-type-alias (Either A B) (⊕ [left A] [right B]))
+(define-type-alias (Option A) (⊕ [some A] [none]))
+
+(typecheck-fail (var [middle 3] as (Either Int Float))
+                #:with-msg "type \\(Either Int Float\\) does not have variant named 'middle'")
+
+(check-type (λ (x) x) : (→ (Either Int Float) (Either Int Float)))
+(check-type (λ (x) x) : (→ (Either Int Float) (⊕ [left Int] [right Float])))
+
+(typecheck-fail (let ([x (var [left 3] as (Either Int Int))]) 0)
+                #:with-msg "x: linear variable unused")
+
+(check-type (match (var [left 3] as (Either Int Int))
+              [(left x) x]
+              [(right y) (+ y 1)])
+            : Int ⇒ 3)
+
+(check-type (match (var [right 5] as (Either Int Int))
+              [(left x) x]
+              [(right y) (+ y 1)])
+            : Int ⇒ 6)
+
+(typecheck-fail (match (var [left 3] as (Either Int (-o Int Int)))
+                  [(left x) x]
+                  [(right f) 0])
+                #:with-msg "f: linear variable unused")
+
+(check-type (match (var [right (λ (x) (+ x x))] as (Either Int (-o Int Int)))
+              [(left x) x]
+              [(right f) (f 2)])
+            : Int ⇒ 4)
+
+(typecheck-fail (match (var [left 0] as (Either Int String))
+                  [(left x) x]
+                  [(right y) y])
+                #:with-msg "branches have incompatible types: Int and String")
+
+(typecheck-fail (match (var [some ()] as (Option Unit))
+                  [(left x) x]
+                  [(right y) y])
+                #:with-msg "type \\(Option Unit\\) does not have variant named 'left'")
+(%%reset-linear-mode)
+
+(typecheck-fail (match (var [left 0] as (Either Int Int))
+                  [(left x) x]
+                  [(right y z) y])
+                #:with-msg "wrong number of arguments to variant: expected 1, got 2")
+(%%reset-linear-mode)
+
+(typecheck-fail (let ([f (λ ([x : Int]) x)])
+                  (match (var [left 0] as (Either Int Int))
+                    [(left x) (f x)]
+                    [(right y) y]))
+                #:with-msg "f: linear variable may be unused in certain branches")
+(%%reset-linear-mode)

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

@@ -0,0 +1,76 @@
+#lang s-exp turnstile/examples/linear/lin
+(require turnstile/rackunit-typechecking
+         (only-in racket/base quote))
+
+(check-type #t : Bool)
+(check-type 4 : Int)
+(check-type () : Unit)
+
+(check-type (let ([x 3] [y 4]) y) : Int -> 4)
+
+(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 "branches have incompatible types: Int and Unit")
+(%%reset-linear-mode)
+
+(check-type (λ ([x : Int]) x) : (-o Int Int))
+(check-type (λ ! ([x : Int]) x) : (→ Int Int))
+(check-type (λ (x) x) : (-o String String))
+(check-type (λ (x) x) : (→ String String))
+
+(check-type + : (→ Int Int Int))
+(check-type (+ 1 2) : Int -> 3)
+(check-type ((λ ([x : Int]) (+ x 1)) 4) : Int -> 5)
+
+
+(typecheck-fail (λ ([p : (-o Int Bool)]) 0)
+                #:with-msg "p: linear variable unused")
+
+(typecheck-fail (let ([f (λ ([x : Int]) x)])
+                  0)
+                #:with-msg "f: linear variable unused")
+
+(typecheck-fail (let ([f (λ ([x : Int]) x)])
+                  (f (f 3)))
+                #:with-msg "f: linear variable used more than once")
+
+(typecheck-fail (let ([f (λ ([x : Int]) x)])
+                  (if #t
+                      (f 3)
+                      4))
+                #:with-msg "f: linear variable may be unused in certain branches")
+
+(typecheck-fail (let ([f (λ ([x : Int]) x)])
+                  (λ ! ([x : Int]) f))
+                #:with-msg "f: linear variable may not be used by unrestricted function")
+(%%reset-linear-mode)
+
+(check-type (let ([twice (λ ! ([x : Int]) (+ x x))])
+              (+ (twice 8)
+                 (twice 9)))
+            : Int -> 34)
+
+(check-type (let ([f (λ ([x : Int]) #t)])
+              (begin (drop f)
+                     3))
+            : Int -> 3)
+
+(check-type (letrec ([{<= : (→ Int Int Bool)}
+                      (λ (n m)
+                         (if (zero? n)
+                             #t
+                             (if (zero? m)
+                                 #f
+                                 (<= (sub1 n) (sub1 m)))))])
+              (if (<= 4 1) 999
+                  (if (<= 3 3)
+                      0
+                      888)))
+            : Int -> 0)
+
+(typecheck-fail (letrec ([{f : (-o Int Int)}
+                          (λ (x) (f x))])
+                  (f 3))
+                #:with-msg "may not bind linear type \\(-o Int Int\\) in letrec")

turnstile/mode.rkt

@@ -0,0 +1,70 @@
+#lang racket/base
+(provide (struct-out mode)
+         make-mode
+         current-mode
+         with-mode
+         make-param-mode)
+
+
+;; mode object. contains setup routine and teardown routine
+;; as fields.
+(struct mode (setup-fn teardown-fn))
+
+(define (make-mode #:setup [setup-fn void]
+                   #:teardown [teardown-fn void])
+  (mode setup-fn teardown-fn))
+
+
+;; apply the given mode for the successive expressions.
+;; e.g.
+;; (with-mode (mode (λ () (display "before "))
+;;                        (λ () (display "after\n")))
+;;   (display "middle "))
+;; ->
+;;   before middle after
+;;
+;; (with-mode <mode> <body> ...)
+(define-syntax-rule (with-mode mode-expr body ...)
+  (let* ([the-mode mode-expr])
+    ((mode-setup-fn the-mode))
+    (begin0 (parameterize ([current-mode the-mode]) body ...)
+      ((mode-teardown-fn the-mode)))))
+
+
+;; the current set mode. useful for #:submode/mode
+(define current-mode
+  (make-parameter (mode void void)))
+
+
+;; returns a mode that sets the given
+;; parameter to the given value, for its duration.
+;; similar to (parameterize ([P value]) ...)
+;;
+;; make-param-mode : ∀T. (parameterof T) T -> mode?
+(define (make-param-mode P value)
+  (let* ([swap! (λ ()
+                  (let ([cur (P)])
+                    (P value)
+                    (set! value cur)))])
+    (mode swap! swap!)))
+
+
+
+(module+ test
+  (require rackunit)
+
+  (define color (make-parameter 'red))
+
+  (define ->blue (make-param-mode color 'blue))
+  (define ->green (make-param-mode color 'green))
+
+  (with-mode ->blue
+    (check-equal? (color) 'blue))
+  (check-equal? (color) 'red)
+
+  (with-mode ->green
+    (check-equal? (color) 'green)
+    (with-mode ->blue
+      (check-equal? (color) 'blue))
+    (check-equal? (color) 'green))
+  )

turnstile/scribblings/reference.scrbl

@@ -2,6 +2,7 @@
 
 @(require scribble/example racket/sandbox
           (for-label racket/base
+                     turnstile/mode
                      (except-in turnstile/turnstile ⊢ stx mk-~ mk-?))
           "doc-utils.rkt" "common.rkt")
 
@@ -59,15 +60,17 @@ and then press Control-@litchar{\}.
    [expr-template (code:line @#,racket[quasisyntax] @#,tech:template)]
    [type-template (code:line @#,racket[quasisyntax] @#,tech:template)]
    [key identifier?]
-   [premise (code:line [⊢ tc ...] ooo ...)
-            (code:line [ctx ⊢ tc ...] ooo ...)
-            (code:line [ctx-elem ... ⊢ tc ...] ooo ...)
-            (code:line [ctx ctx ⊢ tc ...] ooo ...)
+   [premise (code:line [⊢ tc ... prem-options] ooo ...)
+            (code:line [ctx-elem ... ⊢ tc ... prem-options] ooo ...)
+            (code:line [ctx ⊢ tc ... prem-options] ooo ...)
+            (code:line [ctx ctx ⊢ tc ... prem-options] ooo ...)
             (code:line [⊢ . tc-elem] ooo ...)
-            (code:line [ctx ⊢ . tc-elem] ooo ...)
             (code:line [ctx-elem ... ⊢ . tc-elem] ooo ...)
+            (code:line [ctx ⊢ . tc-elem] ooo ...)
             (code:line [ctx ctx ⊢ . tc-elem] ooo ...)
             type-relation
+            (code:line #:mode mode-expr (premise ...))
+            (code:line #:submode fn-expr (premise ...))
             (code:line @#,racket[syntax-parse] @#,tech:pat-directive)]
    [ctx (ctx-elem ...)]
    [ctx-elem (code:line [id ≫ id key template ... ...] ooo ...)
@@ -83,6 +86,9 @@ and then press Control-@litchar{\}.
                   (code:line [type-template τ= type-template #:for expr-template] ooo ...)
                   (code:line [type-template τ⊑ type-template] ooo ...)
                   (code:line [type-template τ⊑ type-template #:for expr-template] ooo ...)]
+   [prem-options (code:line)
+                 (code:line #:mode mode-expr)
+                 (code:line #:submode fn-expr)]
    [conclusion [⊢ expr-template ⇒ type-template]
                [⊢ expr-template ⇒ key template]
                [⊢ expr-template (⇒ key template) ooo ...]
@@ -142,6 +148,26 @@ pattern @racket[x ... y ...] will not work as expected.
 For convenience, lone identifiers written to the left of the turnstile are
 automatically treated as type variables.
 
+@italic{Modes}
+
+The keyword @racket[#:mode], when appearing at end of a typechecking rule,
+sets the parameter @racket[current-mode] to the @racket[mode] object supplied
+by @racket[_mode-expr], for the extent of that rule. @racket[#:mode], when
+appearing as its own premise, sets the @racket[current-mode] parameter for the
+extent of all the grouped sub-premises.
+
+The keyword @racket[#:submode] is similar to @racket[#:mode], but it calls
+@racket[(_fn-expr (current-mode))] to obtain the new mode object. Thus,
+@racket[#:mode (_fn-expr (current-mode))] is identical to @racket[#:submode
+_fn-expr].
+
+See @secref{Modes} for more details.
+
+WARNING: @racket[#:mode] is unaware of the backtracking behavior of
+@racket[syntax-parse]. If pattern backtracking escapes a @racket[#:mode] group, it may
+leave @racket[current-mode] in an undesirable state.
+
+
 @; ----------------------------------------------------------------------------
 @bold{Conclusion}
 
@@ -692,7 +718,70 @@ The possible variances are:
 
 @defproc[(variance? [v any/c]) boolean/c]{
  Predicate that recognizes the variance values.}
-                                      
+
+
+@section{Modes}
+
+@defmodule[turnstile/mode #:use-sources (turnstile/mode)]
+@(define mode-ev
+   (let ([ev (make-base-eval)])
+     (ev '(require turnstile/mode))
+     ev))
+
+Modes are typically used by the @racket[#:mode] and @racket[#:submode]
+keywords in @racket[define-typed-syntax] (and related forms). When judgements
+are parameterized by a @racket[mode] value, the parameter
+@racket[current-mode] is set to that value for the extend of the
+sub-premises. Additionally, the function @racket[mode-setup-fn] is called
+before setting @racket[current-mode], and the function
+@racket[mode-teardown-fn] is called after @racket[current-mode] is restored to
+its previous value.
+
+@defstruct*[mode ([setup-fn (-> any)] [teardown-fn (-> any)])]{
+  Structure type for modes. Modes can be used to parameterize type judgements
+  or groups of type judgements, to give additional context and to help enable
+  flow-sensitive languages.
+
+  User defined modes should be defined as structs that inherit from @racket[mode].
+}
+
+@defproc[(make-mode [#:setup setup-fn (-> any) void]
+                    [#:teardown teardown-fn (-> any) void]) mode?]{
+  Constructs a new @racket[mode] object with the given setup and teardown functions.
+}
+
+@defparam[current-mode mode mode? #:value (make-mode)]{
+  A parameter that holds the current mode. Typically parameterized using the keywords
+  @racket[#:mode] and @racket[#:submode] from @racket[define-typed-syntax] forms.
+}
+
+@defform[(with-mode mode-expr body ...+)
+         #:contracts ([mode-expr mode?])]{
+  The result of @racket[with-mode] is the result of the last @racket[_body].
+  The parameter @racket[current-mode] is assigned to the result of
+  @racket[_mode-expr] for the extent of the @racket[_body] expressions. The
+  function @racket[mode-setup-fn] is called on the result of
+  @racket[_mode-expr] before @racket[current-mode] is set, and the function
+  @racket[mode-teardown-fn] is called after @racket[current-mode] is restored
+  to its previous value.
+
+  @examples[#:eval mode-ev
+    (define-struct (my-mode mode) ())
+    (define M (make-my-mode (λ () (displayln "M setup"))
+                            (λ () (displayln "M teardown"))))
+    (with-mode M
+      (displayln (current-mode)))]}
+
+@defproc[(make-param-mode [param parameter?] [value any/c]) mode?]{
+  Creates a @racket[mode] that assigns the given parameter to the given
+  value for the extent of the mode.
+
+  @examples[#:eval mode-ev
+    (define current-scope (make-parameter 'outer))
+    (with-mode (make-param-mode current-scope 'inner)
+      (displayln (current-scope)))]}
+
+
 @section{Miscellaneous Syntax Object Functions}
 
 These are all phase 1 functions.

turnstile/turnstile.rkt

@@ -1,8 +1,10 @@
 #lang racket/base
 
-(provide (except-out (all-from-out macrotypes/typecheck) 
+(provide (except-out (all-from-out macrotypes/typecheck)
                      -define-typed-syntax -define-syntax-category)
-         define-typed-syntax define-syntax-category
+         define-typed-syntax
+         define-typed-variable-syntax
+         define-syntax-category
          (rename-out [define-typed-syntax define-typerule]
                      [define-typed-syntax define-syntax/typecheck])
          (for-syntax syntax-parse/typecheck
@@ -64,8 +66,9 @@
 (module syntax-classes racket/base
   (provide (all-defined-out))
   (require (for-meta 0 (submod ".." typecheck+))
-           (for-meta -1 (submod ".." typecheck+) 
-                     (except-in macrotypes/typecheck #%module-begin mk-~ mk-?))
+           (for-meta -1 (submod ".." typecheck+)
+                     (except-in macrotypes/typecheck #%module-begin mk-~ mk-?)
+                     "mode.rkt")
            (for-meta -2 (except-in macrotypes/typecheck #%module-begin)))
   (define-syntax-class ---
     [pattern dashes:id
@@ -89,7 +92,7 @@
   (define (add-lists stx n)
     (cond [(zero? n) stx]
           [else (add-lists (list stx) (sub1 n))]))
-  
+
   (define-splicing-syntax-class props
     [pattern (~and (~seq stuff ...) (~seq (~seq k:id v) ...))])
   (define-splicing-syntax-class ⇒-prop
@@ -197,13 +200,14 @@
              #`(~post
                 #,(with-depth #'tc.e-pat #'[ooo ...]))])
   (define-syntax-class tc*
-    #:attributes (depth es-stx es-stx-orig es-pat)
+    #:attributes (depth es-stx es-stx-orig es-pat wrap-computation)
     [pattern tc:tc-elem
              #:with depth 0
              #:with es-stx #'tc.e-stx
              #:with es-stx-orig #'tc.e-stx-orig
-             #:with es-pat #'tc.e-pat]
-    [pattern (tc:tc ...)
+             #:with es-pat #'tc.e-pat
+             #:attr wrap-computation (λ (stx) stx)]
+    [pattern (tc:tc ... opts:tc-post-options ...)
              #:do [(define ds (stx-map syntax-e #'[tc.depth ...]))
                    (define max-d (apply max 0 ds))]
              #:with depth (add1 max-d)
@@ -218,7 +222,19 @@
                 (add-lists tc-es-pat (- max-d d))))
              #:with es-stx #'[es-stx* ...]
              #:with es-stx-orig #'[es-stx-orig* ...]
-             #:with es-pat #'[es-pat* ...]])
+             #:with es-pat #'[es-pat* ...]
+             #:attr wrap-computation
+             (λ (stx)
+               (foldr (λ (fun stx) (fun stx))
+                      stx
+                      (attribute opts.wrap)))])
+  (define-splicing-syntax-class tc-post-options
+    #:attributes (wrap)
+    [pattern (~seq #:mode mode-expr)
+             #:attr wrap (λ (stx) #`(with-mode mode-expr #,stx))]
+    [pattern (~seq #:submode fn-expr)
+             #:attr wrap (λ (stx) #`(with-mode (fn-expr (current-mode)) #,stx))]
+    )
   (define-splicing-syntax-class tc-clause
     #:attributes (pat)
     #:datum-literals (⊢)
@@ -238,13 +254,12 @@
              (with-depth
               #`[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig]
               #'[ooo ...])
-             #:with pat
-             #`(~post
-                (~post
-                 (~parse
-                  tcs-pat
-                  (infers/depths 'clause-depth 'tc.depth #`tvctxs/ctxs/ess/origs
-                                 #:tag (current-tag)))))]
+             #:with inf #'(infers/depths 'clause-depth
+                                         'tc.depth
+                                         #`tvctxs/ctxs/ess/origs
+                                         #:tag (current-tag))
+             #:with inf+ ((attribute tc.wrap-computation) #'inf)
+             #:with pat #`(~post (~post (~parse tcs-pat inf+)))]
     )
   (define-splicing-syntax-class clause
     #:attributes (pat)
@@ -305,6 +320,26 @@
     [pattern (~seq #:fail-unless condition:expr message:expr)
              #:with pat
              #'(~post (~fail #:unless condition message))]
+    [pattern (~seq #:mode mode-expr (sub-clause:clause ...))
+             #:with (the-mode tmp) (generate-temporaries #'(the-mode tmp))
+             #:with pat
+             #'(~and (~do (define the-mode mode-expr)
+                          ((mode-setup-fn the-mode))
+                          (define tmp (current-mode))
+                          (current-mode the-mode))
+                     sub-clause.pat ...
+                     (~do (current-mode tmp)
+                          ((mode-teardown-fn the-mode))))]
+    [pattern (~seq #:submode fn-expr (sub-clause:clause ...))
+             #:with (the-mode tmp) (generate-temporaries #'(the-mode tmp))
+             #:with pat
+             #'(~and (~do (define the-mode (fn-expr (current-mode)))
+                          ((mode-setup-fn the-mode))
+                          (define tmp (current-mode))
+                          (current-mode the-mode))
+                     sub-clause.pat ...
+                     (~do (current-mode tmp)
+                          ((mode-teardown-fn the-mode))))]
     )
   (define-syntax-class last-clause
     #:datum-literals (⊢ ≫ ≻ ⇒ ⇐)
@@ -442,6 +477,16 @@
                         [current-tag (type-key1)])
            (syntax-parse/typecheck stx kw-stuff ... rule ...)))]))
 
+(define-syntax define-typed-variable-syntax
+  (syntax-parser
+    [(_ (~optional (~seq #:name name:id) #:defaults ([name (generate-temporary '#%var)]))
+        (~and (~seq kw-stuff ...) :stxparse-kws)
+        rule:rule ...+)
+     #'(begin
+         (define-typed-syntax name kw-stuff ... rule ...)
+         (begin-for-syntax
+           (current-var-assign (macro-var-assign #'name))))]))
+
 (define-syntax define-syntax-category
   (syntax-parser
     [(_ name:id)        ; default key1 = ': for types