Configurable var transformers & better ellipsis grouping for Turnstile

macrotypes/typecheck.rkt

@@ -919,42 +919,78 @@
   ;;       but I'm not sure it properly generalizes
   ;;       eg, what if I need separate type-eval and kind-eval fns?
   ;; - should infer be moved into define-syntax-category?
-  (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
-       #:with (~or (~and (tv:id ...)
+  ;; added: '#:var-stx lst' specifies the variable transformers used to bind
+  ;;   ctx in the expansion of the expressions.
+  ;; TODO: delete #:tev and #:kev?
+  (define (infer es
+                 #:tvctx [tvctx '()]
+                 #:ctx [ctx '()]
+                 #:tag [tag (current-tag)]
+                 #:expa [expa expand/df]
+                 #:tev [tev #'(current-type-eval)]
+                 #:kev [kev #'(current-type-eval)]
+                 #:var-stx [var-stxs (var-transformers-for-context ctx tag tev kev)])
+    (syntax-parse es
+      [(e ...)
+       #:with (var-stx ...) var-stxs
+       #:with (x ...) (stx-map (lambda (ctx-elem)
+                                 (if (identifier? ctx-elem)
+                                     ctx-elem
+                                     (stx-car ctx-elem)))
+                               ctx)
+       ; TODO: turnstile syntax no longer uses tvctx.
+       ; is it obsolete? should we just prepend tvctx to ctx?
+       #:with (~or ([tv:id (~seq tvsep:id tvk) ...] ...)
+                   (~and (tv:id ...)
                          (~parse ([(tvsep ...) (tvk ...)] ...)
-                                 (stx-map (λ _ #'[(::) (#%type)]) #'(tv ...))))
-                   ([tv (~seq tvsep:id tvk) ...] ...))
-                   tvctx
-       #:with (e ...) es
+                                 (stx-map (λ _ #'[(::) (#%type)]) #'(tv ...)))))
+              tvctx
        #:with ((~literal #%plain-lambda) tvs+
                (~let*-syntax
                 ((~literal #%expression)
                  ((~literal #%plain-lambda) xs+
                   (~let*-syntax
                    ((~literal #%expression) e+) ... (~literal void))))))
-        (expa
+       (expa
         #`(λ (tv ...)
-            (let*-syntax ([tv (make-rename-transformer
+            (let*-syntax ([tv (make-rename-transformer ; TODO: make this an argument too?
                                (mk-tyvar
                                 (attachs #'tv '(tvsep ...) #'(tvk ...)
                                          #:ev #,kev)))] ...)
-              (λ (X ... x ...)
-                (let*-syntax ([X (make-variable-like-transformer
-                                 (mk-tyvar (attach #'X ':: (#,kev #'#%type))))] ...
-                              [x (make-variable-like-transformer
-                                  (attachs #'x '(sep ...) #'(τ ...)
-                                           #:ev #,tev))] ...)
+              (λ (x ...)
+                (let*-syntax ([x var-stx] ...)
                   (#%expression e) ... void)))))
-       (list #'tvs+ #'xs+ 
-             #'(e+ ...) 
-             (stx-map (λ (e) (detach e tag)) #'(e+ ...)))]
-      [([x τ] ...) (infer es #:ctx #`([x #,tag τ] ...) #:tvctx tvctx #:tag tag)]))
+       (list #'tvs+
+             #'xs+
+             #'(e+ ...)
+             (stx-map (λ (e) (detach e tag)) #'(e+ ...)))]))
+
+  (define (var-transformers-for-context ctx tag tev kev)
+    (stx-map (syntax-parser
+               ; missing seperator
+               [[x:id τ] #'(VAR x : τ)]
+               ; seperators given
+               [[x:id . props] #'(VAR x . props)]
+               ; just variable; interpreted as type variable
+               [X:id #'(TYVAR X)])
+             ctx))
+
+  ; variable syntax for regular typed variables
+  (define-syntax VAR
+    (syntax-parser
+      [(_ x (~seq tag prop) ...)
+       #`(make-variable-like-transformer
+          (attachs #'x '(tag ...) #'(prop ...)
+                   #:ev (current-type-eval)))]))
+
+  ; variable syntax for regular kinded type variables
+  (define-syntax TYVAR
+    (syntax-parser
+      [(_ X)
+       #`(make-variable-like-transformer
+          (mk-tyvar (attach #'X ':: ((current-type-eval) #'#%type))))]))
+
+
 
   ;; fns derived from infer ---------------------------------------------------
   ;; some are syntactic shortcuts, some are for backwards compat

turnstile/examples/linear.rkt

@@ -0,0 +1,191 @@
+#lang turnstile
+
+(provide (type-out Unit Int Str Bool -o ⊗ !!)
+         #%top-interaction #%module-begin require only-in
+         #%datum begin tup let λ #%app if
+         (rename-out [λ lambda]))
+
+(provide (typed-out [+ : (!! (-o Int Int Int))]
+                    [< : (!! (-o Int Int Bool))]
+                    [displayln : (!! (-o Str Unit))]))
+
+(define-base-types Unit Int Str Bool)
+(define-type-constructor -o #:arity >= 1)
+(define-type-constructor ⊗ #:arity = 2)
+(define-type-constructor !! #:arity = 1)
+
+(begin-for-syntax
+  (require syntax/id-set)
+  (define (sym-diff s0 . ss)
+    (for*/fold ([s0 s0])
+               ([s (in-list ss)]
+                [x (in-set s)])
+      (if (set-member? s0 x)
+          (set-remove s0 x)
+          (set-add s0 x))))
+
+
+  (define unrestricted-type?
+    (or/c Int? Str? !!?))
+
+
+  (define used-vars (immutable-free-id-set))
+
+  (define (lin-var-in-scope? x)
+    (not (set-member? used-vars x)))
+
+  (define (use-lin-var x)
+    (unless (lin-var-in-scope? x)
+      (raise-syntax-error #f "linear variable used more than once" x))
+    (set! used-vars (set-add used-vars x)))
+
+  (define (pop-vars xs ts)
+    (set! used-vars
+          (for/fold ([uv used-vars])
+                    ([x (in-syntax xs)]
+                     [t (in-syntax ts)])
+            (unless (unrestricted-type? t)
+              (when (lin-var-in-scope? x)
+                (raise-syntax-error #f "linear variable unused" x)))
+            (set-remove uv x))))
+
+
+
+  (define scope-stack '())
+
+  (define (save-scope)
+    (set! scope-stack (cons used-vars scope-stack)))
+
+  (define (merge-scope #:fail-msg fail-msg
+                       #:fail-src [fail-src #f])
+    (for ([x (in-set (sym-diff used-vars (car scope-stack)))])
+      (raise-syntax-error #f fail-msg fail-src x))
+    (set! scope-stack (cdr scope-stack)))
+
+  (define (swap-scope)
+    (set! used-vars
+          (begin0 (car scope-stack)
+            (set! scope-stack
+                  (cons used-vars (cdr scope-stack))))))
+
+  )
+
+
+(define-typed-syntax #%top-interaction
+  [(_ . e) ≫
+   [⊢ e ≫ e- ⇒ τ]
+   --------
+   [≻ (#%app- printf- '"~a : ~a\n"
+              e-
+              '#,(type->str #'τ))]])
+
+
+(define-typed-variable-syntax (LIN x- : σ)
+  [x ≫
+   #:when (unrestricted-type? #'σ)
+   --------
+   [⊢ x- ⇒ σ]]
+  [x ≫
+   #:do [(use-lin-var #'x-)]
+   --------
+   [⊢ x- ⇒ σ]])
+
+
+(define-typed-syntax #%datum
+  [(_ . n:exact-integer) ≫
+   --------
+   [⊢ (#%datum- . n) ⇒ Int]]
+  [(_ . b:boolean) ≫
+   --------
+   [⊢ (#%datum- . b) ⇒ Bool]]
+  [(_ . s:str) ≫
+   --------
+   [⊢ (#%datum- . s) ⇒ Str]]
+  [(_ . x) ≫
+   --------
+   [#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
+
+
+(define-typed-syntax begin
+  [(_ e ... e0) ≫
+   [⊢ [e ≫ e- ⇒ _] ... [e0 ≫ e0- ⇒ σ]]
+   --------
+   [⊢ (begin- e- ... e0-) ⇒ σ]])
+
+
+(define-typed-syntax tup
+  #:datum-literals (!)
+  [(_ e1 e2) ≫
+   [⊢ e1 ≫ e1- ⇒ σ1]
+   [⊢ e2 ≫ e2- ⇒ σ2]
+   --------
+   [⊢ (#%app- list- e1- e2-) ⇒ (⊗ σ1 σ2)]]
+
+  [(_ ! e1 e2) ≫
+   #:do [(save-scope)]
+   [⊢ e1 ≫ e1- ⇒ σ1]
+   [⊢ e2 ≫ e2- ⇒ σ2]
+   #:do [(merge-scope #:fail-msg "linear variable may not be used by unrestricted tuple"
+                      #:fail-src this-syntax)]
+   --------
+   [⊢ (#%app- list- e1- e2-) ⇒ (!! (⊗ σ1 σ2))]])
+
+
+(define-typed-syntax let
+  [(let ([x rhs] ...) e) ≫
+   [⊢ [rhs ≫ rhs- ⇒ σ] ...]
+   [[LIN x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
+   #:do [(pop-vars #'(x- ...) #'(σ ...))]
+   --------
+   [⊢ (let- ([x- rhs-] ...) e-) ⇒ σ_out]])
+
+
+(define-typed-syntax λ
+  #:datum-literals (: !)
+  ; linear function
+  [(λ ([x:id : ty:type] ...) e) ≫
+   #:with (σ ...) #'(ty.norm ...)
+   [[LIN x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
+   #:do [(pop-vars #'(x- ...) #'(σ ...))]
+   --------
+   [⊢ (λ- (x- ...) e-) ⇒ (-o σ ... σ_out)]]
+
+  ; unrestricted function
+  [(λ ! ([x:id : ty:type] ...) e) ≫
+   #:do [(save-scope)]
+   #:with (σ ...) #'(ty.norm ...)
+   [[LIN x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
+   #:do [(pop-vars #'(x- ...) #'(σ ...))
+         (merge-scope #:fail-msg "linear variable may not be used by unrestricted function"
+                      #:fail-src this-syntax)]
+   --------
+   [⊢ (λ- (x- ...) e-) ⇒ (!! (-o σ ... σ_out))]])
+
+
+(define-typed-syntax #%app
+  [(_) ≫
+   --------
+   [⊢ (#%app- void-) ⇒ Unit]]
+
+  [(#%app fun arg ...) ≫
+   [⊢ fun ≫ fun- ⇒ σ_fun]
+   #:with (~or (~-o σ_in ... σ_out)
+               (~!! (~-o σ_in ... σ_out))
+               (~post (~fail "expected function type")))
+   #'σ_fun
+   [⊢ [arg ≫ arg- ⇐ σ_in] ...]
+   --------
+   [⊢ (#%app- fun- arg- ...) ⇒ σ_out]])
+
+
+(define-typed-syntax if
+  [(if c e1 e2) ≫
+   [⊢ c ≫ c- ⇐ Bool]
+   #:do [(save-scope)]
+   [⊢ e1 ≫ e1- ⇒ σ]
+   #:do [(swap-scope)]
+   [⊢ e2 ≫ e2- ⇐ σ]
+   #:do [(merge-scope #:fail-msg "linear variable may be unused in certain branches"
+                      #:fail-src this-syntax)]
+   --------
+   [⊢ (if- c- e1- e2-) ⇒ σ]])

turnstile/examples/tests/linear-tests.rkt

@@ -0,0 +1,62 @@
+#lang s-exp "../linear.rkt"
+(require "rackunit-typechecking.rkt")
+(require (only-in racket/base quote))
+
+(check-type #t : Bool)
+(check-type 4 : Int)
+(check-type () : Unit)
+
+(check-type (tup 1 #t) : (⊗ Int Bool) -> '(1 #t))
+(check-type (tup 1 (tup 2 3)) : (⊗ Int (⊗ Int Int)) -> '(1 (2 3)))
+
+(check-type (let ([x 3] [y 4]) y) : Int -> 4)
+(check-type (let ([p (tup 1 2)]) p) : (⊗ Int Int) -> '(1 2))
+
+(typecheck-fail (let ([p (tup 1 2)]) ())
+                #:with-msg "p: linear variable unused")
+(typecheck-fail (let ([p (tup 1 2)]) (tup p p))
+                #:with-msg "p: linear variable used more than once")
+
+(check-type (if #t 1 2) : Int -> 1)
+(typecheck-fail (if 1 2 3)
+                #:with-msg "expected Bool, given Int")
+(typecheck-fail (if #t 2 ())
+                #:with-msg "expected Int, given Unit")
+
+(check-type (let ([p (tup 1 ())]) (if #t p p)) : (⊗ Int Unit))
+(typecheck-fail (let ([p (tup 1 ())]) (if #t p (tup 2 ())))
+                #:with-msg "linear variable may be unused in certain branches")
+(typecheck-fail (let ([p (tup 1 ())]) (if #t p (begin p p)))
+                #:with-msg "p: linear variable used more than once")
+
+
+(check-type (λ ([x : Int]) (tup x x)) : (-o Int (⊗ Int Int)))
+(check-type (λ ([x : (⊗ Int Int)]) x) : (-o (⊗ Int Int) (⊗ Int Int)))
+(typecheck-fail (λ ([x : (⊗ Int Int)]) ())
+                #:with-msg "x: linear variable unused")
+
+(check-type (let ([p (tup 1 2)]) (λ ([x : Int]) p))
+            : (-o Int (⊗ Int Int)))
+
+(check-type (λ ! ([x : Int]) x) : (!! (-o Int Int)))
+(typecheck-fail (let ([p (tup 1 2)]) (λ ! ([x : Int]) p))
+                #:with-msg "linear variable may not be used by unrestricted function\n  at: p")
+
+
+(check-type (let ([f (λ ([x : Int] [y : Int]) y)])
+              (f 3 4))
+            : Int -> 4)
+(check-type + : (!! (-o Int Int Int)))
+(check-type (+ 1 2) : Int -> 3)
+(check-type (< 3 4) : Bool -> #t)
+
+
+(check-type (let ([×2 (λ ! ([x : Int]) (+ x x))])
+              (+ (×2 8)
+                 (×2 9)))
+            : Int -> 34)
+
+(typecheck-fail (let ([×2 (λ ([x : Int]) (+ x x))])
+                  (+ (×2 8)
+                     (×2 9)))
+                #:with-msg "×2: linear variable used more than once")