From 6891da26675beb94f56017644baf74266fafb391 Mon Sep 17 00:00:00 2001
From: Milo Turner <iitalics@gmail.com>
Date: Tue, 13 Jun 2017 13:04:21 -0400
Subject: [PATCH] create example linear language + tests

---
 turnstile/examples/linear.rkt             | 191 ++++++++++++++++++++++
 turnstile/examples/tests/linear-tests.rkt |  62 +++++++
 2 files changed, 253 insertions(+)
 create mode 100644 turnstile/examples/linear.rkt
 create mode 100644 turnstile/examples/tests/linear-tests.rkt

diff --git a/turnstile/examples/linear.rkt b/turnstile/examples/linear.rkt
new file mode 100644
index 00000000..761676b2
--- /dev/null
+++ b/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-) ⇒ σ]])
diff --git a/turnstile/examples/tests/linear-tests.rkt b/turnstile/examples/tests/linear-tests.rkt
new file mode 100644
index 00000000..6eb36e81
--- /dev/null
+++ b/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")