created fabUL-like langauge using lin + ext-stlc

closes #21

macrotypes/examples/mlish+adhoc.rkt

@@ -1,7 +1,8 @@
 #lang s-exp "../typecheck.rkt"
 (require (only-in "../typecheck.rkt"
                   [define-typed-syntax def-typed-stx/no-provide]))
-(require racket/fixnum racket/flonum)
+(require (postfix-in - racket/fixnum)
+         (postfix-in - racket/flonum))
 
 (extends
  "ext-stlc.rkt"

macrotypes/examples/mlish.rkt

@@ -1,6 +1,7 @@
 #lang s-exp macrotypes/typecheck
 (require
- racket/fixnum racket/flonum
+ (postfix-in - racket/fixnum)
+ (postfix-in - racket/flonum)
  (for-syntax macrotypes/type-constraints macrotypes/variance-constraints))
 
 (extends

macrotypes/examples/tests/mlish/chameneos.mlish

@@ -118,9 +118,16 @@
   ;;          (list 66 0)
   ;;          (list 67 0)))
 
-(check-type (map (λ ([x : Result]) (proj x 0))
-                 (go 1000 (list Blue Red Yellow Red Yellow Blue)))
-  : (List Int) -> (list 333 333 333 333 334 334))
+(define res2 
+  (map (λ ([x : Result]) (proj x 0))
+       (go 1000 (list Blue Red Yellow Red Yellow Blue))))
+(check-type res2 : (List Int))
+(define (=333/4 [x : Int] -> Bool) (or (= x 333) (= x 334)))
+(define (andmap [p? : (→ X Bool)] [xs : (List X)] → Bool)
+  (match2 xs with
+   [nil -> #t]
+   [x :: rst -> (and (p? x) (andmap p? rst))]))         
+(check-type (andmap =333/4 res2) : Bool -> #t)
   ;; -> (list (list 333 0)
   ;;          (list 333 0)
   ;;          (list 333 0)

macrotypes/info.rkt

@@ -14,4 +14,4 @@
     "examples/tests/mlish/bg/README.md"))
 
 (define test-timeouts
-  '(("examples/tests/mlish/generic.mlish" 200)))
+  '(("examples/tests/mlish/generic.mlish" 300)))

macrotypes/stx-utils.rkt

@@ -6,6 +6,7 @@
 ;; shorthands
 (define id? identifier?)
 (define free-id=? free-identifier=?)
+(define fmt format)
 
 (define (stx-cadr stx) (stx-car (stx-cdr stx)))
 (define (stx-caddr stx) (stx-cadr (stx-cdr stx)))
@@ -13,9 +14,9 @@
 
 (define datum->stx datum->syntax)
 (define (stx->datum stx)
-  (if (syntax? stx)
-      (syntax->datum stx)
-      (map syntax->datum stx)))
+  (cond [(syntax? stx) (syntax->datum stx)]
+        [(list? stx) (map stx->datum stx)]
+        [else stx]))
 
 (define (stx-rev stx)
   (reverse (stx->list stx)))
@@ -34,11 +35,17 @@
   (define paren-prop (syntax-property stx 'paren-shape))
   (and paren-prop (char=? #\{ paren-prop)))
 
-(define (stx-member v stx)
-  (member v (stx->list stx) free-identifier=?))
+(define (stx-datum-equal? x y [eq equal?])
+  (eq (stx->datum x) (stx->datum y)))
+
+(define (stx-member v stx [eq free-id=?])
+  (member v (stx->list stx) eq))
+
+(define (stx-datum-member v stx [eq stx-datum-equal?])
+  (stx-member v stx eq))
 
 (define (str-stx-member v stx)
-  (member (datum->syntax v) (map datum->syntax (stx->list stx)) string=?))
+  (stx-datum-member v stx))
 (define (str-stx-assoc v stx)
   (assoc v (map stx->list (stx->list stx)) stx-str=?))
 (define (stx-assoc v stx [cmp free-identifier=?]) ; v = id
@@ -47,8 +54,9 @@
   (findf f (stx->list stx)))
 
 (define (stx-length stx) (length (stx->list stx)))
-(define (stx-length=? stx1 stx2)
-  (= (stx-length stx1) (stx-length stx2)))
+(define (stx-length=? stx1 stx2)   (= (stx-length stx1) (stx-length stx2)))
+(define (stx-length>=? stx1 stx2)  (>= (stx-length stx1) (stx-length stx2)))
+(define (stx-length<=? stx1 stx2)  (<= (stx-length stx1) (stx-length stx2)))
 
 (define (stx-last stx) (last (stx->list stx)))
 
@@ -79,10 +87,28 @@
 
 (define (stx-remove-dups Xs)
   (remove-duplicates (stx->list Xs) free-identifier=?))
+(define (stx-remove v lst [f free-id=?])
+  (remove v (stx->list lst) f))
 
 (define (stx-drop stx n)
   (drop (stx->list stx) n))
 
+(define (id-lower-case? stx)
+  (unless (identifier? stx)
+    (error 'stx-upcase "Expected identifier, given ~a" stx))
+  (char-lower-case? 
+   (car (string->list (symbol->string (syntax->datum stx))))))
+
+(define (id-upcase stx)
+  (unless (identifier? stx)
+    (error 'stx-upcase "Expected identifier, given ~a" stx))
+  (define chars (string->list (symbol->string (syntax->datum stx))))
+  (define fst (car chars))
+  (define rst (cdr chars))
+  (datum->syntax 
+   stx 
+   (string->symbol (apply string (cons (char-upcase fst) rst)))))
+
 (define (generate-temporariess stx)
   (stx-map generate-temporaries stx))
 (define (generate-temporariesss stx)
@@ -107,14 +133,23 @@
 (define (get-stx-prop/cd*r stx tag)
   (cd*r (syntax-property stx tag)))
 
-  
-
 ;; transfers properties and src loc from orig to new
 (define (transfer-stx-props new orig #:ctx [ctx new])
   (datum->syntax ctx (syntax-e new) orig orig))
 (define (replace-stx-loc old new)
   (datum->syntax (syntax-disarm old #f) (syntax-e (syntax-disarm old #f)) new old))
 
+;; transfer single prop
+(define (transfer-prop p from to)
+  (define v (syntax-property from p))
+  (syntax-property to p v))
+;; transfer all props except 'origin, 'orig, and ':
+(define (transfer-props from to #:except [dont-transfer '(origin orig :)])
+  (define (transfer-from prop to) (transfer-prop prop from to))
+  (define props (syntax-property-symbol-keys from))
+  (define props/filtered (foldr remove props dont-transfer))
+  (foldl transfer-from to props/filtered))
+
 ;; set-stx-prop/preserved : Stx Any Any -> Stx
 ;; Returns a new syntax object with the prop property set to val. If preserved
 ;; syntax properties are supported, this also marks the property as preserved.

macrotypes/typecheck.rkt

@@ -56,7 +56,8 @@
      (syntax/loc this-syntax
        (#%module-begin
         ; auto-provide some useful racket forms
-        (provide #%module-begin #%top-interaction #%top require only-in)
+        (provide #%module-begin #%top-interaction #%top
+         require only-in prefix-in rename-in)
         . stuff))]))
 
 (struct exn:fail:type:runtime exn:fail:user ())
@@ -73,10 +74,14 @@
   ;; drop-file-ext : String -> String
   (define (drop-file-ext filename)
     (car (string-split filename ".")))
-  ;; extract-filename : PathString -> String
-  (define (extract-filename f)
+  ;; extract-filename : PathString or Symbol -> String
+  (define (extract-filename file)
+    (define f (if (string? file) file (symbol->string file)))
     (path->string (path-replace-suffix (file-name-from-path f) "")))
-  (define-syntax-parameter stx (syntax-rules ())))
+  (define-syntax-parameter stx (syntax-rules ()))
+
+  ;; parameter is an identifier transformer
+  (define current-host-lang (make-parameter mk--)))
 
 ;; non-Turnstile define-typed-syntax
 ;; TODO: potentially confusing? get rid of this?
@@ -99,15 +104,19 @@
 (define-syntax extends
   (syntax-parser
     [(_ base-lang
+        (~optional (~seq #:prefix pre))
         (~optional (~seq #:except (~and x:id (~not _:keyword)) ...) 
                    #:defaults ([(x 1) null]))
         (~optional (~seq #:rename [old new] ...) 
                    #:defaults ([(old 1) null][(new 1) null])))
      #:with pre: 
+           (or
+            (attribute pre)
             (let ([pre (or (let ([dat (syntax-e #'base-lang)])
-                             (and (string? dat) (extract-filename dat)))
+                             (and (or (string? dat) (symbol? dat))
+                                  (extract-filename dat)))
                            #'base-lang)])
-              (format-id #'base-lang "~a:" pre))
+              (format-id #'base-lang "~a:" pre)))
      #:with internal-pre (generate-temporary)
      #:with non-excluded-imports #'(except-in base-lang x ... old ...)
      #:with conflicted? #'(λ (n) (member (string->symbol n) '(#%app λ #%datum begin let let* letrec if define)))
@@ -154,7 +163,8 @@
     [(_ (~or x:id [old:id new:id]) ... #:from base-lang)
      #:with pre: 
             (let ([pre (or (let ([dat (syntax-e #'base-lang)])
-                             (and (string? dat) (extract-filename dat)))
+                             (and (or (string? dat) (symbol? dat))
+                                  (extract-filename dat)))
                            #'base-lang)])
               (format-id #'base-lang "~a:" pre))
      #`(begin
@@ -360,6 +370,9 @@
              ;; (printf "(τ=) t2 = ~a\n" #;τ2 (stx->datum t2))
              (or (and (id? t1) (id? t2) (free-id=? t1 t2))
                  (and (stx-null? t1) (stx-null? t2))
+                 (and (not (stx-pair? t1)) (not (id? t1))
+                      (not (stx-pair? t2)) (not (id? t1)) ; datums
+                      (equal? (stx->datum t1) (stx->datum t2)))
                  (syntax-parse (list t1 t2) ; handle binding types
                    [(((~literal #%plain-lambda) (~and (_:id (... ...)) xs) . ts1)
                      ((~literal #%plain-lambda) (~and (_:id (... ...)) ys) . ts2))
@@ -546,7 +559,7 @@
                      ;; to ensure enough stx-parse progress for proper err msg,
                      ;; ie, "invalid type" instead of "improper tycon usage"
                      #:with (~! (~var _ type) (... (... ...))) #'(arg- (... (... ...)))
-                     (add-orig (mk-type #'(τ- arg- (... (... ...)))) stx)]
+                     (add-orig (mk-type (syntax/loc stx (τ- arg- (... (... ...))))) stx)]
                     [_ ;; else fail with err msg
                      (type-error #:src stx
                       #:msg
@@ -715,7 +728,7 @@
    (lambda (stx modes)
      (syntax-parse stx #:datum-literals (:)
        ;; cannot write ty:type bc provides might precede type def
-       [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x))
+       [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x ((current-host-lang)#'out-x)))
                       [[x:id (~optional :) ty] out-x:id])) ...)
         #:with (x/tc ...) (generate-temporaries #'(x ...))
         #:when (stx-map
@@ -729,7 +742,7 @@
 (define-syntax define-primop
   (syntax-parser #:datum-literals (:)
     [(define-primop op:id (~optional :) τ)
-     #:with op- (format-id #'op "~a-" #'op)
+     #:with op- ((current-host-lang) #'op)
      #'(define-primop op op- τ)]
     [(define-primop op/tc:id (~optional #:as) op:id (~optional :) τ:type)
      ; rename-transformer doesnt seem to expand at the right time
@@ -754,11 +767,42 @@
   (define current-tag (make-parameter (type-key1))))
 
 ;; type assignment utilities --------------------------------------------------
+(define-simple-macro (with-ctx ([x x- ty] ...) e ...)
+  (let-syntax
+      ([x (make-variable-like-transformer (assign-type #'x- #'ty))] ...)
+    e ...))
+
 (define-syntax (let*-syntax stx)
   (syntax-parse stx
     [(_ () . body) #'(let-syntax () . body)]
     [(_ (b . bs) . es) #'(let-syntax (b) (let*-syntax bs . es))]))
+
+(define-syntax (⊢m stx)
+  (syntax-parse stx #:datum-literals (:)
+   [(_ e : τ) (assign-type #`e #`τ)]
+   [(_ 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
@@ -898,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
@@ -924,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/dep.rkt

@@ -0,0 +1,113 @@
+#lang turnstile/lang
+
+; Π  λ ≻ ⊢ ≫ ⇒ ∧ (bidir ⇒ ⇐)
+
+(provide (rename-out [#%type *]) Π → ∀ λ #%app ann define define-type-alias)
+
+#;(begin-for-syntax
+  (define old-ty= (current-type=?))
+  (current-type=?
+   (λ (t1 t2)
+     (displayln (stx->datum t1))
+     (displayln (stx->datum t2))
+     (old-ty= t1 t2)))
+  (current-typecheck-relation (current-type=?)))
+
+;(define-syntax-category : kind)
+(define-internal-type-constructor →)
+(define-internal-binding-type ∀)
+;; TODO: how to do Type : Type
+(define-typed-syntax (Π ([X:id : τ_in] ...) τ_out) ≫
+  [[X ≫ X- : τ_in] ... ⊢ [τ_out ≫ τ_out- ⇒ _][τ_in ≫ τ_in- ⇒ _] ...]
+  -------
+  [⊢ (∀- (X- ...) (→- τ_in- ... τ_out-)) ⇒ #,(expand/df #'#%type)])
+;; abbrevs for Π
+(define-simple-macro (→ τ_in ... τ_out)
+  #:with (X ...) (generate-temporaries #'(τ_in ...))
+  (Π ([X : τ_in] ...) τ_out))
+(define-simple-macro (∀ (X ...)  τ)
+  (Π ([X : #%type] ...) τ))
+;; ~Π pattern expander
+(begin-for-syntax
+  (define-syntax ~Π
+    (pattern-expander
+     (syntax-parser
+       [(_ ([x:id : τ_in] ... (~and (~literal ...) ooo)) τ_out)
+        #'(~∀ (x ... ooo) (~→ τ_in ... ooo τ_out))]
+       [(_ ([x:id : τ_in] ...)  τ_out)
+        #'(~∀ (x ...) (~→ τ_in ... τ_out))]))))
+
+;; TODO: add case with expected type + annotations
+;; - check that annotations match expected types
+(define-typed-syntax λ
+  [(_ ([x:id : τ_in] ...) e) ≫
+   [[x ≫ x- : τ_in] ... ⊢ [e ≫ e- ⇒ τ_out][τ_in ≫ τ_in- ⇒ _] ...]
+   -------
+   [⊢ (λ- (x- ...) e-) ⇒ (Π ([x- : τ_in-] ...) τ_out)]]
+  [(_ (y:id ...) e) ⇐ (~Π ([x:id : τ_in] ...) τ_out) ≫
+   [[x ≫ x- : τ_in] ... ⊢ #,(substs #'(x ...) #'(y ...) #'e) ≫ e- ⇐ τ_out]
+   ---------
+   [⊢ (λ- (x- ...) e-)]])
+
+;; TODO: do beta on terms?
+(define-typed-syntax #%app
+  [(_ e_fn e_arg ...) ≫ ; apply lambda
+   [⊢ e_fn ≫ (_ (x ...) e ~!) ⇒ (~Π ([X : τ_in] ...) τ_out)]
+   #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+                 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
+   [⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
+   --------
+   [⊢ #,(substs #'(e_arg- ...) #'(x ...) #'e) ⇒
+      #,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]]
+  [(_ e_fn e_arg ... ~!) ≫ ; apply var
+   [⊢ e_fn ≫ e_fn- ⇒ (~Π ([X : τ_in] ...) τ_out)]
+   #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+                 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
+   [⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
+   --------
+   [⊢ (#%app- e_fn- e_arg- ...) ⇒
+      #,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]])
+
+(define-typed-syntax (ann e (~datum :) τ) ≫
+  [⊢ e ≫ e- ⇐ τ]
+  --------
+  [⊢ e- ⇒ τ])
+
+(define-syntax define-type-alias
+  (syntax-parser
+    [(_ alias:id τ);τ:any-type)
+     #'(define-syntax- alias
+         (make-variable-like-transformer #'τ))]
+    #;[(_ (f:id x:id ...) ty)
+     #'(define-syntax- (f stx)
+         (syntax-parse stx
+           [(_ x ...)
+            #:with τ:any-type #'ty
+            #'τ.norm]))]))
+
+(define-typed-syntax define
+  #;[(_ x:id (~datum :) τ:type e:expr) ≫
+   ;[⊢ e ≫ e- ⇐ τ.norm]
+   #:with y (generate-temporary #'x)
+   --------
+   [≻ (begin-
+        (define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
+        (define- y (ann e : τ.norm)))]]
+  [(_ x:id e) ≫
+   ;This won't work with mutually recursive definitions
+   [⊢ e ≫ e- ⇒ _]
+   #:with y (generate-temporary #'x)
+   #:with y+props (transfer-props #'e- #'y #:except '(origin))
+   --------
+   [≻ (begin-
+        (define-syntax x (make-rename-transformer #'y+props))
+        (define- y e-))]]
+  #;[(_ (f [x (~datum :) ty] ... (~or (~datum →) (~datum ->)) ty_out) e ...+) ≫
+   #:with f- (add-orig (generate-temporary #'f) #'f)
+   --------
+   [≻ (begin-
+        (define-syntax- f
+          (make-rename-transformer (⊢ f- : (→ ty ... ty_out))))
+        (define- f-
+          (stlc+lit:λ ([x : ty] ...)
+            (stlc+lit:ann (begin e ...) : ty_out))))]])

turnstile/examples/ext-stlc.rkt

@@ -50,17 +50,6 @@
             #:with τ:any-type #'ty
             #'τ.norm]))]))
 
-(begin-for-syntax
-  (define (transfer-prop p from to)
-    (define v (syntax-property from p))
-    (syntax-property to p v))
-  (define (transfer-props from to)
-    (define props (syntax-property-symbol-keys from))
-    (define props/filtered (remove 'origin (remove 'orig (remove ': props))))
-    (foldl (lambda (p stx) (transfer-prop p from stx)) 
-           to 
-           props/filtered)))
-
 (define-typed-syntax define
   [(_ x:id (~datum :) τ:type e:expr) ≫
    ;[⊢ e ≫ e- ⇐ τ.norm]

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/mlish+adhoc.rkt

@@ -1,5 +1,5 @@
 #lang turnstile
-(require racket/fixnum racket/flonum)
+(require (postfix-in - racket/fixnum) (postfix-in - racket/flonum))
 
 (extends
  "ext-stlc.rkt"

turnstile/examples/mlish.rkt

@@ -1,6 +1,7 @@
 #lang turnstile/lang
 (require
- racket/fixnum racket/flonum
+ (postfix-in - racket/fixnum)
+ (postfix-in - racket/flonum)
  (for-syntax macrotypes/type-constraints macrotypes/variance-constraints))
 
 (extends

turnstile/examples/stlc+union.rkt

@@ -3,6 +3,8 @@
  #:except #%app #%datum + add1 sub1 *
           Int Int? ~Int Float Float? ~Float Bool ~Bool Bool?)
 
+(require (for-syntax "util/filter-maximal.rkt"))
+
 ;; Simply-Typed Lambda Calculus, plus union types
 ;; Types:
 ;; - types from and ext+stlc.rkt
@@ -27,7 +29,8 @@
                     [* : (→ Num Num Num)]
                     [add1 : (→ Int Int)]
                     [sub1 : (→ Int Int)])
-         #%datum #%app)
+         #%datum #%app
+         (for-syntax ~PosInt ~Zero ~NegInt ~True ~False))
 
 (define-syntax define-named-type-alias
   (syntax-parser
@@ -44,11 +47,9 @@
 
 (define-for-syntax (prune+sort tys)
   (stx-sort 
-   (remove-duplicates 
+   (filter-maximal 
     (stx->list tys)
-    ;; remove dups keeps first element
-    ;; but we want to keep supertype
-    (lambda (x y) (typecheck? y x)))))
+    typecheck?)))
   
 (define-syntax (U stx)
   (syntax-parse stx
@@ -57,8 +58,8 @@
      #:with ((~or (~U* ty1- ...) ty2-) ...) (stx-map (current-type-eval) #'tys)
      #:with tys- (prune+sort #'(ty1- ... ... ty2- ...))
      (if (= 1 (stx-length #'tys-))
-         (stx-car #'tys)
-         #'(U* . tys-))]))
+         (stx-car #'tys-)
+         (syntax/loc stx (U* . tys-)))]))
 (define-syntax Bool
   (make-variable-like-transformer
    (add-orig #'(U False True) #'Bool)))

turnstile/examples/tests/dep-tests.rkt

@@ -0,0 +1,96 @@
+#lang s-exp "../dep.rkt"
+(require "rackunit-typechecking.rkt")
+
+; Π → λ ∀ ≻ ⊢ ≫ ⇒
+
+;; examples from Prabhakar's Proust paper
+
+(check-type (λ ([x : *]) x) : (Π ([x : *]) *))
+(typecheck-fail ((λ ([x : *]) x) (λ ([x : *]) x))
+ #:verb-msg "expected *, given (Π ([x : *]) *)")
+
+;; transitivity of implication
+(check-type (λ ([A : *][B : *][C : *])
+              (λ ([f : (→ B C)])
+                (λ ([g : (→ A B)])
+                  (λ ([x : A])
+                    (f (g x))))))
+            : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C)))))
+; unnested
+(check-type (λ ([A : *][B : *][C : *])
+              (λ ([f : (→ B C)][g : (→ A B)])
+                (λ ([x : A])
+                  (f (g x)))))
+            : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C))))
+;; no annotations
+(check-type (λ (A B C)
+              (λ (f) (λ (g) (λ (x)
+                (f (g x))))))
+            : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C)))))
+(check-type (λ (A B C)
+              (λ (f g)
+                (λ (x)
+                  (f (g x)))))
+            : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C))))
+;; TODO: partial annotations
+
+;; booleans -------------------------------------------------------------------
+
+;; Bool type
+(define-type-alias Bool (∀ (A) (→ A A A)))
+
+;; Bool terms
+(define T (λ ([A : *]) (λ ([x : A][y : A]) x)))
+(define F (λ ([A : *]) (λ ([x : A][y : A]) y)))
+(check-type T : Bool)
+(check-type F : Bool)
+(define and (λ ([x : Bool][y : Bool]) ((x Bool) y F)))
+(check-type and : (→ Bool Bool Bool))
+
+;; And type constructor, ie type-level fn
+(define-type-alias And
+  (λ ([A : *][B : *])
+    (∀ (C) (→ (→ A B C) C))))
+(check-type And : (→ * * *))
+
+;; And type intro
+(define ∧
+  (λ ([A : *][B : *])
+    (λ ([x : A][y : B])
+      (λ ([C : *])
+        (λ ([f : (→ A B C)])
+          (f x y))))))
+(check-type ∧ : (∀ (A B) (→ A B (And A B))))
+
+;; And type elim
+(define proj1
+  (λ ([A : *][B : *])
+    (λ ([e∧ : (And A B)])
+      ((e∧ A) (λ ([x : A][y : B]) x)))))
+(define proj2
+  (λ ([A : *][B : *])
+    (λ ([e∧ : (And A B)])
+      ((e∧ B) (λ ([x : A][y : B]) y)))))
+;; bad proj2: (e∧ A) should be (e∧ B)
+(typecheck-fail
+ (λ ([A : *][B : *])
+   (λ ([e∧ : (And A B)])
+     ((e∧ A) (λ ([x : A][y : B]) y))))
+ #:verb-msg
+ "expected (→ A B C), given (Π ((x : A) (y : B)) B)")
+(check-type proj1 : (∀ (A B) (→ (And A B) A)))
+(check-type proj2 : (∀ (A B) (→ (And A B) B)))
+
+;((((conj q) p) (((proj2 p) q) a)) (((proj1 p) q) a)))))
+(define and-commutes
+  (λ ([A : *][B : *])
+    (λ ([e∧ : (And A B)])
+      ((∧ B A) ((proj2 A B) e∧) ((proj1 A B) e∧)))))
+;; bad and-commutes, dont flip A and B: (→ (And A B) (And A B))
+(typecheck-fail
+ (λ ([A : *][B : *])
+   (λ ([e∧ : (And A B)])
+     ((∧ A B) ((proj2 A B) e∧) ((proj1 A B) e∧))))
+ #:verb-msg
+ "#%app: type mismatch: expected A, given C") ; TODO: err msg should be B not C?
+(check-type and-commutes : (∀ (A B) (→ (And A B) (And B A))))

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/examples/tests/mlish/chameneos.mlish

@@ -118,9 +118,16 @@
   ;;          (list 66 0)
   ;;          (list 67 0)))
 
-(check-type (map (λ ([x : Result]) (proj x 0))
-                 (go 1000 (list Blue Red Yellow Red Yellow Blue)))
-  : (List Int) -> (list 333 333 333 333 334 334))
+(define res2 
+  (map (λ ([x : Result]) (proj x 0))
+       (go 1000 (list Blue Red Yellow Red Yellow Blue))))
+(check-type res2 : (List Int))
+(define (=333/4 [x : Int] -> Bool) (or (= x 333) (= x 334)))
+(define (andmap [p? : (→ X Bool)] [xs : (List X)] → Bool)
+  (match2 xs with
+   [nil -> #t]
+   [x :: rst -> (and (p? x) (andmap p? rst))]))         
+(check-type (andmap =333/4 res2) : Bool -> #t)
   ;; -> (list (list 333 0)
   ;;          (list 333 0)
   ;;          (list 333 0)

turnstile/examples/tests/pat-expander-tests-def.rkt

@@ -0,0 +1,171 @@
+#lang turnstile
+
+(provide (all-defined-out))
+
+(define-base-type Nothing)
+(define-base-type Bool)
+(define-base-type Int)
+(define-base-type String)
+(define-type-constructor Tuple #:arity >= 0)
+(define-type-constructor Listof #:arity = 1)
+(define-type-constructor Sequenceof #:arity >= 0)
+
+(begin-for-syntax
+  (define-splicing-syntax-class (for-clause-group env)
+    #:attributes [[clause- 1] [env.x 1] [env.τ 1]]
+    [pattern (~seq (~var clause (for-clause env))
+                   ...)
+      #:with [clause- ...] #'[clause.clause- ... ...]
+      #:with [[env.x env.τ] ...] #'[[clause.env.x clause.env.τ] ... ...]])
+
+  (define-splicing-syntax-class (guard-clause env)
+    #:attributes [[clause- 1]]
+    [pattern (~and (~seq #:when bool:expr)
+                   (~typecheck
+                    #:with [[x τ_x] ...] env
+                    [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool]))
+      #:with [clause- ...] #`[#:when (let- ([x- x] ...) bool-)]]
+    [pattern (~and (~seq #:unless bool:expr)
+                   (~typecheck
+                    #:with [[x τ_x] ...] env
+                    [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool]))
+      #:with [clause- ...] #`[#:unless (let- ([x- x] ...) bool-)]]
+    [pattern (~and (~seq #:break bool:expr)
+                   (~typecheck
+                    #:with [[x τ_x] ...] env
+                    [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool]))
+      #:with [clause- ...] #`[#:break (let- ([x- x] ...) bool-)]]
+    [pattern (~and (~seq #:final bool:expr)
+                   (~typecheck
+                    #:with [[x τ_x] ...] env
+                    [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool]))
+      #:with [clause- ...] #`[#:final (let- ([x- x] ...) bool-)]])
+
+  (define-splicing-syntax-class (for-clause env)
+    #:attributes [[clause- 1] [env.x 1] [env.τ 1]]
+    [pattern (~and [x:id seq:expr]
+                   (~typecheck
+                    #:with [[y τ_y] ...] env
+                    [[y ≫ y- : τ_y] ... ⊢ seq ≫ seq- ⇒ (~Sequenceof τ_x)]))
+      #:with [clause- ...] #'[[x (let- ([y- y] ...) seq-)]]
+      #:with [[env.x env.τ] ...] #'[[x τ_x]]]
+    [pattern (~and [(x:id ...) seq:expr]
+                   (~typecheck
+                    #:with [[y τ_y] ...] env
+                    [[y ≫ y- : τ_y] ... ⊢ seq ≫ seq- ⇒ (~Sequenceof τ_x ...)]))
+      #:fail-unless (stx-length=? #'[x ...] #'[τ_x ...])
+      (format "expected a ~v-valued sequence, given a ~v-valued one"
+              (stx-length #'[x ...])
+              (stx-length #'[τ_x ...]))
+      #:with [clause- ...] #'[[(x ...) (let- ([y- y] ...) seq-)]]
+      #:with [[env.x env.τ] ...] #'[[x τ_x] ...]])
+
+  (define-syntax-class (for-clauses env)
+    #:attributes [[clause- 1] [env.x 1] [env.τ 1]]
+    [pattern ((~var group (for-clause-group env)))
+      #:with [clause- ...] #'[group.clause- ...]
+      #:with [[env.x env.τ] ...] #'[[group.env.x group.env.τ] ...]]
+    [pattern ((~var fst (for-clause-group env))
+              (~var guard (guard-clause (stx-append env #'[[fst.env.x fst.env.τ] ...])))
+              .
+              (~var rst (for-clauses (stx-append env #'[[fst.env.x fst.env.τ] ...]))))
+      #:with [clause- ...] #'[fst.clause- ... guard.clause- ... rst.clause- ...]
+      #:with [[env.x env.τ] ...] #'[[fst.env.x fst.env.τ] ... [rst.env.x rst.env.τ] ...]])
+  )
+
+;; ------------------------------------------------------------------------
+
+;; for/list
+
+(define-typed-syntax for/list
+  [(_ (~var clauses (for-clauses #'[]))
+     body) ≫
+   [[clauses.env.x ≫ x- : clauses.env.τ] ...
+    ⊢ body ≫ body- ⇒ τ]
+   --------
+   [⊢ (for/list- (clauses.clause- ...)
+        (let- ([x- clauses.env.x] ...) body-))
+      ⇒ (Listof τ)]])
+
+(define-typed-syntax in-range
+  [(_ n:expr) ≫
+   [⊢ n ≫ n- ⇐ Int]
+   --------
+   [⊢ (in-range- n-) ⇒ (Sequenceof Int)]])
+
+(define-typed-syntax in-naturals
+  [(_) ≫ --- [⊢ (in-naturals-) ⇒ (Sequenceof Int)]]
+  [(_ n:expr) ≫
+   [⊢ n ≫ n- ⇐ Int]
+   --------
+   [⊢ (in-naturals- n-) ⇒ (Sequenceof Int)]])
+
+(define-typed-syntax in-list
+  [(_ lst:expr) ≫
+   [⊢ lst ≫ lst- ⇒ (~Listof τ)]
+   --------
+   [⊢ (in-list- lst-) ⇒ (Sequenceof τ)]])
+
+(define-typed-syntax in-indexed
+  [(_ seq:expr) ≫
+   [⊢ seq ≫ seq- ⇒ (~Sequenceof τ)]
+   --------
+   [⊢ (in-indexed- seq-) ⇒ (Sequenceof τ Int)]])
+
+;; ------------------------------------------------------------------------
+
+;; Constructing Literals, Tuples, and Lists
+
+(define-typed-syntax #%datum
+  [(_ . b:boolean) ≫ --- [⊢ (quote- b) ⇒ Bool]]
+  [(_ . i:integer) ≫ --- [⊢ (quote- i) ⇒ Int]]
+  [(_ . s:str) ≫ --- [⊢ (quote- s) ⇒ String]])
+
+(define-typed-syntax tuple
+  [(_ e:expr ...) ≫
+   [⊢ [e ≫ e- ⇒ τ] ...]
+   --------
+   [⊢ (vector-immutable- e- ...) ⇒ (Tuple τ ...)]])
+
+(define-typed-syntax list
+  [(_) ≫ --- [⊢ (quote- ()) ⇒ (Listof Nothing)]]
+  [(_ e0:expr e:expr ...) ≫
+   [⊢ e0 ≫ e0- ⇒ τ]
+   [⊢ [e ≫ e- ⇐ τ] ...]
+   --------
+   [⊢ (list- e0- e- ...) ⇒ (Listof τ)]])
+
+;; ------------------------------------------------------------------------
+
+;; Basic Bool Forms
+
+(define-typed-syntax not
+  [(_ b:expr) ≫ [⊢ b ≫ b- ⇐ Bool] --- [⊢ (not- b-) ⇒ Bool]])
+
+(define-typed-syntax and
+  [(_ b:expr ...) ≫
+   [⊢ [b ≫ b- ⇐ Bool] ...]
+   --------
+   [⊢ (and- b- ...) ⇒ Bool]])
+
+;; ------------------------------------------------------------------------
+
+;; Basic Int Forms
+
+(define-typed-syntax even?
+  [(_ i:expr) ≫ [⊢ i ≫ i- ⇐ Int] --- [⊢ (even?- i-) ⇒ Bool]])
+
+(define-typed-syntax odd?
+  [(_ i:expr) ≫ [⊢ i ≫ i- ⇐ Int] --- [⊢ (odd?- i-) ⇒ Bool]])
+
+;; ------------------------------------------------------------------------
+
+;; Basic String Forms
+
+(define-typed-syntax string=?
+  [(_ a:expr b:expr) ≫
+   [⊢ a ≫ a- ⇐ String]
+   [⊢ b ≫ b- ⇐ String]
+   --------
+   [⊢ (string=?- a- b-) ⇒ Bool]])
+

turnstile/examples/tests/pat-expander-tests.rkt

@@ -0,0 +1,143 @@
+#lang turnstile
+
+(require turnstile/rackunit-typechecking
+         "pat-expander-tests-def.rkt")
+
+;; The for/list macro defined in "pat-expander-tests-def.rkt" uses the
+;; ~typecheck pattern-expander to typecheck the for clauses within a
+;; syntax class.
+
+;; These tests make sure that #:when conditions can refer to
+;; identifiers defined in previous clauses.
+
+(check-type (for/list () 1) : (Listof Int) -> (list 1))
+(check-type (for/list () #t) : (Listof Bool) -> (list #t))
+(check-type (for/list () #f) : (Listof Bool) -> (list #f))
+
+(check-type (for/list (#:when #t) 1) : (Listof Int) -> (list 1))
+(check-type (for/list (#:when #f) 1) : (Listof Int) -> (list))
+(check-type (for/list ([x (in-range 5)]) x)
+            : (Listof Int)
+            -> (list 0 1 2 3 4))
+
+(check-type (for/list ([(s i) (in-indexed (in-list (list "a" "b" "c")))])
+              (tuple s i))
+            : (Listof (Tuple String Int))
+            -> (list (tuple "a" 0) (tuple "b" 1) (tuple "c" 2)))
+
+(check-type (for/list ([(s i) (in-indexed (in-list (list "a" "b" "c")))]
+                       #:when (even? i))
+              (tuple s i))
+            : (Listof (Tuple String Int))
+            -> (list (tuple "a" 0) (tuple "c" 2)))
+
+(check-type (for/list ([(s i) (in-indexed (in-list (list "a" "b" "c" "d" "e")))]
+                       #:when (even? i)
+                       [j (in-range i)])
+              (tuple s i j))
+            : (Listof (Tuple String Int Int))
+            -> (list (tuple "c" 2 0)
+                     (tuple "c" 2 1)
+                     (tuple "e" 4 0)
+                     (tuple "e" 4 1)
+                     (tuple "e" 4 2)
+                     (tuple "e" 4 3)))
+
+;; ------------------------------------------------------------------------
+
+;; Test based on section 11 of the racket guide
+
+(check-type (for/list ([book (in-list (list "Guide" "Reference" "Notes"))]
+                       #:when (not (string=? book "Notes"))
+                       [i (in-naturals 1)]
+                       [chapter (in-list (list "Intro" "Details" "Conclusion" "Index"))]
+                       #:when (not (string=? chapter "Index")))
+              (tuple book i chapter))
+            : (Listof (Tuple String Int String))
+            -> (list (tuple "Guide" 1 "Intro")
+                     (tuple "Guide" 2 "Details")
+                     (tuple "Guide" 3 "Conclusion")
+                     (tuple "Reference" 1 "Intro")
+                     (tuple "Reference" 2 "Details")
+                     (tuple "Reference" 3 "Conclusion")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+                       #:break (string=? book "Story")
+                       [chapter (in-list (list "Intro" "Details" "Conclusion"))])
+              (tuple book chapter))
+            : (Listof (Tuple String String))
+            -> (list (tuple "Guide" "Intro")
+                     (tuple "Guide" "Details")
+                     (tuple "Guide" "Conclusion")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+                       #:when #true
+                       [chapter (in-list (list "Intro" "Details" "Conclusion"))]
+                       #:break (and (string=? book "Story")
+                                    (string=? chapter "Conclusion")))
+              (tuple book chapter))
+            : (Listof (Tuple String String))
+            -> (list (tuple "Guide" "Intro")
+                     (tuple "Guide" "Details")
+                     (tuple "Guide" "Conclusion")
+                     (tuple "Story" "Intro")
+                     (tuple "Story" "Details")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+                       #:when #true
+                       [chapter (in-list (list "Intro" "Details" "Conclusion"))]
+                       #:final (and (string=? book "Story")
+                                    (string=? chapter "Conclusion")))
+              (tuple book chapter))
+            : (Listof (Tuple String String))
+            -> (list (tuple "Guide" "Intro")
+                     (tuple "Guide" "Details")
+                     (tuple "Guide" "Conclusion")
+                     (tuple "Story" "Intro")
+                     (tuple "Story" "Details")
+                     (tuple "Story" "Conclusion")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+                       #:final (string=? book "Story")
+                       [chapter (in-list (list "Intro" "Details" "Conclusion"))])
+              (tuple book chapter))
+            : (Listof (Tuple String String))
+            -> (list (tuple "Guide" "Intro")
+                     (tuple "Guide" "Details")
+                     (tuple "Guide" "Conclusion")
+                     (tuple "Story" "Intro")))
+
+;; ------------------------------------------------------------------------
+
+;; Tests based on section 3.18 of the racket reference
+
+(check-type (for/list ([i (in-list (list 1 2 3))]
+                       [j (in-list (list "a" "b" "c"))]
+                       #:when (odd? i)
+                       [k (in-list (list #t #f))])
+              (tuple i j k))
+            : (Listof (Tuple Int String Bool))
+            -> (list (tuple 1 "a" #t)
+                     (tuple 1 "a" #f)
+                     (tuple 3 "c" #t)
+                     (tuple 3 "c" #f)))
+
+(check-type (for/list ([i (in-list (list 1 2 3))]
+                       [j (in-list (list "a" "b" "c"))]
+                       #:break (not (odd? i))
+                       [k (in-list (list #t #f))])
+              (tuple i j k))
+            : (Listof (Tuple Int String Bool))
+            -> (list (tuple 1 "a" #true)
+                     (tuple 1 "a" #false)))
+
+(check-type (for/list ([i (in-list (list 1 2 3))]
+                       [j (in-list (list "a" "b" "c"))]
+                       #:final (not (odd? i))
+                       [k (in-list (list #t #f))])
+              (tuple i j k))
+            : (Listof (Tuple Int String Bool))
+            -> (list (tuple 1 "a" #true)
+                     (tuple 1 "a" #false)
+                     (tuple 2 "b" #true)))
+

turnstile/examples/tests/rackunit-typechecking.rkt

@@ -1,17 +1,17 @@
 #lang racket/base
 (require (for-syntax rackunit syntax/srcloc) rackunit macrotypes/typecheck)
 (provide check-type typecheck-fail check-not-type check-props check-runtime-exn
-         check-equal/rand
+         check-equal/rand typecheck-fail/toplvl
          (rename-out [typecheck-fail check-stx-err]))
 
 (begin-for-syntax
   (define (add-esc s) (string-append "\\" s))
-  (define escs (map add-esc '("(" ")" "[" "]")))
+  (define escs (map add-esc '("(" ")" "[" "]" "+" "*")))
   (define (replace-brackets str)
     (regexp-replace* "\\]" (regexp-replace* "\\[" str "(") ")"))
   (define (add-escs str)
     (replace-brackets
-        (foldl (lambda (c s) (regexp-replace* c s (add-esc c))) str escs)))
+     (foldl (lambda (c s) (regexp-replace* c s (add-esc c))) str escs)))
   (define (expected tys #:given [givens ""] #:note [note ""])
     (string-append  
      note ".*Expected.+argument\\(s\\) with type\\(s\\).+" 
@@ -68,6 +68,31 @@
      #'(void)]))
 
 (define-syntax (typecheck-fail stx)
+  (syntax-parse stx #:datum-literals (:)
+    [(_ e (~or
+           (~optional (~seq #:with-msg msg-pat) #:defaults ([msg-pat #'""]))
+           (~optional (~seq #:verb-msg vmsg) #:defaults ([vmsg #'""]))))
+     #:with msg:str
+            (if (attribute msg-pat)
+                (eval-syntax (datum->stx #'h (stx->datum #'msg-pat)))
+                (eval-syntax (datum->stx #'h `(add-escs ,(stx->datum #'vmsg)))))
+     #:when (with-check-info*
+             (list (make-check-expected (syntax-e #'msg))
+                   (make-check-expression (syntax->datum stx))
+                   (make-check-location (build-source-location-list stx))
+                   (make-check-name 'typecheck-fail)
+                   (make-check-params (list (syntax->datum #'e) (syntax-e #'msg))))
+             (λ ()
+               (check-exn
+                (λ (ex)
+                  (and (or (exn:fail? ex) (exn:test:check? ex))
+                       ; check err msg matches
+                       (regexp-match? (syntax-e #'msg) (exn-message ex))))
+                (λ ()
+                  (expand/df #'e)))))
+     #'(void)]))
+
+(define-syntax (typecheck-fail/toplvl stx)
   (syntax-parse stx #:datum-literals (:)
     [(_ e (~optional (~seq #:with-msg msg-pat) #:defaults ([msg-pat #'""])))
      #:with msg:str 
@@ -85,7 +110,7 @@
                        ; check err msg matches
                        (regexp-match? (syntax-e #'msg) (exn-message ex))))
                 (λ ()
-                  (expand/df #'e)))))
+                  (local-expand #'e 'top-level null)))))
      #'(void)]))
 
 (define-syntax (check-runtime-exn stx)

turnstile/examples/tests/stlc+union+case.rkt

@@ -37,6 +37,14 @@
 (define-type-alias NNN (U (U Nat Nat) (U (U Nat Nat Nat) (U Nat Nat))))
 (check-type ((λ ([x : NNN]) x) 1) : Nat -> 1)
 
+; check that pruning and collapsing don't throw away types when the union
+; contains another empty union
+(typecheck-fail
+ (λ ([x : (U (U) String)])
+   (ann x : (U)))
+ #:with-msg
+ "expected \\(U\\), given \\(U \\(U\\) String\\)")
+
 
 ;; tests from stlc+sub ---------------------
 (check-type 1 : Num)

turnstile/examples/tests/stlc+union.rkt

@@ -27,6 +27,14 @@
 (define-type-alias NNN (U (U Nat Nat) (U (U Nat Nat Nat) (U Nat Nat))))
 (check-type ((λ ([x : NNN]) x) 1) : Nat -> 1)
 
+; check that pruning and collapsing don't throw away types when the union
+; contains another empty union
+(typecheck-fail
+ (λ ([x : (U (U) String)])
+   (ann x : (U)))
+ #:with-msg
+ "expected \\(U\\), given \\(U \\(U\\) String\\)")
+
 
 ;; tests from stlc+sub ---------------------
 (check-type 1 : Num)

turnstile/examples/util/filter-maximal.rkt

@@ -0,0 +1,54 @@
+#lang racket/base
+
+(provide filter-maximal)
+
+(module+ test
+  (require rackunit
+           (only-in racket/list in-permutations)
+           (only-in racket/set set=? subset?)))
+
+;; filter-maximal : [Listof X] [X X -> Bool] -> [Listof X]
+;; <? is a partial ordering predicate
+(define (filter-maximal xs <?)
+  (reverse
+   (for/fold ([acc '()])
+             ([x (in-list xs)])
+     (merge-with x acc <?))))
+
+;; merge-with : X [Listof X] [X X -> Bool] -> [Listof X]
+;; <? is a partial ordering predicate
+(define (merge-with x ys <?)
+  (define (greater? y) (<? x y))
+  (cond [(ormap greater? ys) ys]
+        [else
+         (define (not-lesser? y) (not (<? y x)))
+         (cons x (filter not-lesser? ys))]))
+
+;; ----------------------------------------------------------------------------
+
+(module+ test
+  (define-check (check-filter-maximal lst <? expected)
+    (test-begin
+     (for ([p (in-permutations lst)])
+       (check set=? (filter-maximal p <?) expected))))
+
+  (check-equal? (filter-maximal '(1 2 3 2 3 2 1) <) '(3 3))
+  (check-equal? (filter-maximal '(1 2 3 2 3.0 2 1) <) '(3 3.0))
+  (check-equal? (filter-maximal '(1 2 3.0 2 3 2 1) <) '(3.0 3))
+
+  (check-equal? (filter-maximal '({} {a} {b} {c}) subset?) '({a} {b} {c}))
+  (check-equal? (filter-maximal '({b} {} {a} {c}) subset?) '({b} {a} {c}))
+  (check-equal? (filter-maximal '({c} {b} {a} {}) subset?) '({c} {b} {a}))
+
+  (check-filter-maximal '({} {a} {b}) subset? '({a} {b}))
+  (check-filter-maximal '({} {a} {b} {a b}) subset? '({a b}))
+  (check-filter-maximal '({} {a} {b} {c} {a b}) subset? '({a b} {c}))
+  (check-filter-maximal '({} {a} {b} {c} {a b} {c a} {b c}) subset?
+                        '({a b} {c a} {b c}))
+  (check-filter-maximal '({} {a} {b} {c} {a b} {c a} {b c}) subset?
+                        '({a b} {c a} {b c}))
+  (check-filter-maximal '({} {a} {b} {c} {b c d} {a b} {c a} {b c}) subset?
+                        '({a b} {c a} {b c d}))
+  (check-filter-maximal '({} {a} {b} {c} {a b c d} {a b} {c a} {b c}) subset?
+                        '({a b c d}))
+  )

turnstile/info.rkt

@@ -7,6 +7,7 @@
   '("examples/rosette"
     "examples/fomega3.rkt"
     "examples/tests"
+    "rackunit-typechecking.rkt"
     "examples/trivial.rkt")) ; needs typed racket
 
 (define test-include-paths
@@ -22,5 +23,5 @@
     "examples/tests/mlish/bg/README.md"))
 
 (define test-timeouts
-  '(("examples/tests/mlish/generic.mlish" 200)
+  '(("examples/tests/mlish/generic.mlish" 300)
     ("examples/tests/tlb-infer-tests.rkt" 1800)))

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/rackunit-typechecking.rkt

@@ -0,0 +1,4 @@
+#lang racket/base
+;; extends some rackunit forms to test type-checking
+(require "examples/tests/rackunit-typechecking.rkt")
+(provide (all-from-out "examples/tests/rackunit-typechecking.rkt"))

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}
 
@@ -234,11 +260,73 @@ A @racket[syntax-parse]-like form that supports
 @racket[define-typed-syntax]-style clauses. In particular, see the
 "rule" part of @racket[define-typed-syntax]'s grammar above.}
 
+@; ~typecheck and ~⊢
+
+@defform[(~typecheck premise ...)]{
+A @racket[syntax-parse] @tech[#:doc '(lib "syntax/scribblings/syntax.scrbl")]{pattern expander}
+that supports typechecking syntax.
+
+For example the pattern
+
+@racketblock[
+  (~typecheck
+   [⊢ a ≫ a- ⇒ τ_a]
+   [⊢ b ≫ b- ⇐ τ_a])]
+
+typechecks @racket[a] and @racket[b], expecting @racket[b] to have the
+type of @racket[a], and binding @racket[a-] and @racket[b-] to the
+expanded versions.
+
+This is most useful in places where you want to do typechecking in
+something other than a type rule, like in a function or a syntax
+class.
+
+@(let ([ev (make-base-eval)])
+   (ev '(require turnstile/turnstile))
+   @examples[
+     #:eval ev
+     (begin-for-syntax
+       (struct clause [stx- result-type])
+       (code:comment "f : Stx -> Clause")
+       (define (f stx)
+         (syntax-parse stx
+           [(~and [condition:expr body:expr]
+                  (~typecheck
+                   [⊢ condition ≫ condition- ⇐ Bool]
+                   [⊢ body ≫ body- ⇒ τ_body]))
+            (clause #'[condition- body-] #'τ_body)])))
+     ])}
+
+@defform*[[(~⊢ tc ...)]]{
+A shorthand @tech[#:doc '(lib "syntax/scribblings/syntax.scrbl")]{pattern expander}
+for @racket[(~typcheck [⊢ tc ...])].
+
+For example the pattern @racket[(~⊢ a ≫ a- ⇒ τ_a)] typechecks
+@racket[a], binding the expanded version to @racket[a-] and the type
+to @racket[τ_a].
+
+@(let ([ev (make-base-eval)])
+   (ev '(require turnstile/turnstile))
+   @examples[
+     #:eval ev
+     (begin-for-syntax
+       (struct clause [stx- result-type])
+       (code:comment "f : Stx -> Clause")
+       (define (f stx)
+         (syntax-parse stx
+           [(~and [condition:expr body:expr]
+                  (~⊢ condition ≫ condition- ⇐ Bool)
+                  (~⊢ body ≫ body- ⇒ τ_body))
+            (clause #'[condition- body-] #'τ_body)])))
+     ])}
+
 @; define-primop --------------------------------------------------------------
 @defform*[((define-primop typed-op-id τ)
            (define-primop typed-op-id : τ)
            (define-primop typed-op-id op-id τ)
-           (define-primop typed-op-id op-id : τ))]{
+           (define-primop typed-op-id op-id : τ)
+           (define-primop typed-op-id #:as op-id τ)
+           (define-primop typed-op-id #:as op-id : τ))]{
 Defines @racket[typed-op-id] by attaching type @racket[τ] to (untyped) 
 identifier @racket[op-id], e.g.:
 
@@ -396,8 +484,8 @@ that you can still use other Turnstile conveniences like pattern expanders.}}
                     (code:line #:extra-info stx)])]{
   Analogous to @racket[define-internal-type-constructor], but for binding types.}}
 @item{
-@defform[(type-out ty-id)]{
-A @racket[provide]-spec that, given @racket[ty-id], provides @racket[ty-id], 
+@defform[(type-out ty-id ...)]{
+A @racket[provide]-spec that, for each given @racket[ty-id], provides @racket[ty-id],
 and provides @racket[for-syntax] a predicate @racket[ty-id?] and a @tech:pat-expander @racket[~ty-id].}}
 
 @item{@defparam[current-type-eval type-eval type-eval]{
@@ -493,11 +581,16 @@ equality, but includes alpha-equivalence.
     to validate types.
   Binds a @racket[norm] attribute to the type's expanded representation.}}
  @item{@defthing[type-bind stx-class]{A syntax class recognizing
-     syntax objects with shape @racket[[x:id (~datum :) τ:type]].}}
+     syntax objects with shape @racket[[x:id (~datum :) τ:type]].
+  Binds a @racket[x] attribute to the binding identifier, and a @racket[type] attribute
+  to the type's expanded representation.}}
  @item{@defthing[type-ctx stx-class]{A syntax class recognizing
-      syntax objects with shape @racket[(b:type-bind ...)].}}
+      syntax objects with shape @racket[(b:type-bind ...)].
+  Binds a @racket[x] attribute to the binding identifiers, and a @racket[type] attribute
+  to the expanded representation of the types.}}
  @item{@defthing[type-ann stx-class]{A syntax class recognizing
-       syntax objects with shape @racket[{τ:type}] where the braces are required.}}
+       syntax objects with shape @racket[{τ:type}] where the braces are required.
+  Binds a @racket[norm] attribute to the type's expanded representation.}}
 
  @item{@defproc[(assign-type [e syntax?] [τ syntax?]) syntax?]{
 Phase 1 function that calls @racket[current-type-eval] on @racket[τ] and attaches it to @racket[e] using @tt{key1}.}}
@@ -582,7 +675,7 @@ expanded identifiers from the contexts, e.g.
 
 might return
 
-@racket[(list '() (list #'x-) (list #'(#%plain-app x- 1))(list #'Int))].
+@racket[(list #'() #'(x-) #'((#%plain-app x- 1)) #'(Int))].
 
 The context elements have the same shape as in @racket[define-typed-syntax].
 The contexts use @racket[let*] semantics, where each binding is in scope for
@@ -594,14 +687,14 @@ want to specify a @litchar{::} key when using @racket[infer] to compute the
 kinds on types.}
 
 @defproc[(subst [τ type-stx]
-                [x id]
+                [x identifier?]
                 [e expr-stx]
                 [cmp (-> identifier? identifier? boolean?) bound-identifier=?]) expr-stx]{
 Phase 1 function that replaces occurrences of @racket[x], as determined by @racket[cmp], with
  @racket[τ] in @racket[e].}
 
 @defproc[(substs [τs (listof type-stx)]
-                 [xs (listof id)]
+                 [xs (listof identifier?)]
                  [e expr-stx]
                  [cmp (-> identifier? identifier? boolean?) bound-identifier=?]) expr-stx]{
 Phase 1 function folding @racket[subst] over the given @racket[τs] and @racket[xs].}
@@ -625,12 +718,75 @@ 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.
 
-@defproc[(stx-length [stx syntax?]) Nat]{Analogous to @racket[length].}
+@defproc[(stx-length [stx syntax?]) exact-nonnegative-integer?]{Analogous to @racket[length].}
 @defproc[(stx-length=? [stx1 syntax?] [stx2 syntax?]) boolean?]{
  Returns true if two syntax objects are of equal length.}
 @defproc[(stx-andmap [p? (-> syntax? boolean?)] [stx syntax?]) (listof syntax?)]{

turnstile/turnstile.rkt

@@ -1,11 +1,14 @@
 #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
+                     ~typecheck ~⊢
                      (rename-out
                       [syntax-parse/typecheck syntax-parse/typed-syntax])))
 
@@ -63,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
@@ -88,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
@@ -196,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)
@@ -217,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 (⊢)
@@ -237,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)
@@ -304,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 (⊢ ≫ ≻ ⇒ ⇐)
@@ -403,6 +439,17 @@
          (for-meta 2 'syntax-classes))
 
 (begin-for-syntax
+  (define-syntax ~typecheck
+    (pattern-expander
+     (syntax-parser
+       [(_ clause:clause ...)
+        #'(~and clause.pat ...)])))
+  (define-syntax ~⊢
+    (pattern-expander
+     (syntax-parser
+       [(_ . stuff)
+        #'(~typecheck [⊢ . stuff])])))
+
   (define-syntax syntax-parse/typecheck
     (syntax-parser
       [(_ stx-expr
@@ -430,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