start dependent types example

macrotypes/stx-utils.rkt

@@ -107,14 +107,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.

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

@@ -69,9 +69,13 @@
 
 (define-syntax (typecheck-fail stx)
   (syntax-parse stx #:datum-literals (:)
-    [(_ e (~optional (~seq #:with-msg msg-pat) #:defaults ([msg-pat #'""])))
-     #:with msg:str 
-            (eval-syntax (datum->syntax #'here (syntax->datum #'msg-pat)))
+    [(_ 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))