commit 98568ceb9984222f42a0f41bb27b28d9aae737b7
parent 1c0fa751d6a8b06e46f663bd468e6ea0d48fcdf2
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 13 Oct 2016 21:21:05 -0400
add define-internal-type-constructor and define-internal-binding-type
- add fomega-no-reuse example
Diffstat:
5 files changed, 422 insertions(+), 8 deletions(-)
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -688,7 +688,9 @@
(syntax/loc stx
(τ-internal* (λ () (#%expression extra-info) . args)))]))
; this is the actual constructor
- (define-syntax (τ stx)
+ #,@(if (attribute no-attach-kind?)
+ #'()
+ #'((define-syntax (τ stx)
(syntax-parse stx
[(_ . args)
#:fail-unless (op (stx-length #'args) n)
@@ -708,7 +710,7 @@
#:msg
(string-append
"Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
- #'τ stx #'op #'n)])))]))
+ #'τ stx #'op #'n)])))))]))
;; Form for defining *binding* types, kinds, etc.
;; The def uses pattern vars "τ" and "kind" but this form is not restricted to
@@ -817,7 +819,9 @@
(syntax/loc stx
(τ-internal* (λ bvs (#%expression extra-info) . args)))]))
; this is the actual constructor
- (define-syntax (τ stx)
+ #,@(if (attribute no-attach-kind?)
+ #'()
+ #`((define-syntax (τ stx)
(syntax-parse stx
[(_ (~or (bv:id (... ...))
(~and (~fail #:unless #,(attribute has-annotations?))
@@ -833,20 +837,23 @@
(format "wrong number of arguments, expected ~a ~a"
'op 'n)
#:with (bvs- τs- _) (infers/ctx+erase #'bvs+ks #'args)
+ ;; the args are validated on the next line, rather than above
+ ;; to ensure enough stx-parse progress so we get a proper err msg,
+ ;; ie, "invalid type" instead of "improper tycon usage"
#:with (~! (~var _ kind) (... ...)) #'τs-
#:with ([tv (~datum :) k_arg] (... ...)) #'bvs+ks
#:with k_result (if #,(attribute has-annotations?)
#'(kindcon k_arg (... ...))
#'#%kind)
-; #:with ty-out (expand/df #'(τ- bvs- . τs-))
- #:with ty-out #'(τ- bvs- . τs-)
- (add-orig (assign-type #'ty-out #'k_result) stx)]
+ (add-orig
+ (assign-type #'(τ- bvs- . τs-) #'k_result)
+ stx)]
;; else fail with err msg
[_
(type-error #:src stx
#:msg (string-append
"Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
- #'τ stx #'op #'n)])))]))
+ #'τ stx #'op #'n)])))))]))
; examples:
; (define-syntax-category type)
@@ -867,6 +874,7 @@
#:with define-name-cons (format-id #'name "define-~a-constructor" #'name)
#:with define-binding-name (format-id #'name "define-binding-~a" #'name)
#:with define-internal-name-cons (format-id #'name "define-internal-~a-constructor" #'name)
+ #:with define-internal-binding-name (format-id #'name "define-internal-binding-~a" #'name)
#:with name-ann (format-id #'name "~a-ann" #'name)
#:with name=? (format-id #'name "~a=?" #'name)
#:with names=? (format-id #'names "~a=?" #'names)
@@ -971,6 +979,10 @@
(syntax-parser
[(_ (~var x id) . rst)
#'(define-basic-checked-stx x : name #:no-attach-kind . rst)]))
+ (define-syntax define-internal-binding-name
+ (syntax-parser
+ [(_ (~var x id) . rst)
+ #'(define-binding-checked-stx x : name #:no-attach-kind . rst)]))
(define-syntax define-name-cons
(syntax-parser
[(_ (~var x id) . rst)
diff --git a/turnstile/examples/fomega-no-reuse.rkt b/turnstile/examples/fomega-no-reuse.rkt
@@ -0,0 +1,165 @@
+#lang turnstile/lang
+
+;; System F_omega, without reusing rules from other languages
+;; - try to avoid using built-in "kind" system (ie #%type)
+;; - not quite there: define-primop and typed-out still use current-type?
+;; - use define-internal- forms instead
+
+;; example suggested by Alexis King
+
+(provide define-type-alias
+ ★ ⇒ Int Bool String Float Char → ∀ tyλ tyapp
+ (typed-out [+ : (→ Int Int Int)])
+ λ #%app #%datum Λ inst ann)
+
+(define-syntax-category kind)
+
+;; redefine:
+;; - current-type? - recognizes types with ★ kind only
+;; - current-type-eval - reduce tylams and tyapps
+;; - current-type=? - must check for any kind annotations
+(begin-for-syntax
+ ;; need this for define-primop (which still uses type stx-class)
+ (current-type? (λ (t) (★? (typeof t))))
+
+ ;; TODO: I think this can be simplified
+ (define (normalize τ)
+ (syntax-parse τ #:literals (#%plain-app #%plain-lambda)
+ [x:id #'x]
+ [(#%plain-app
+ (#%plain-lambda (tv ...) τ_body) τ_arg ...)
+ (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
+ [(#%plain-lambda (x ...) . bodys)
+ #:with bodys_norm (stx-map normalize #'bodys)
+ (transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)]
+ [(#%plain-app x:id . args)
+ #:with args_norm (stx-map normalize #'args)
+ (transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)]
+ [(#%plain-app . args)
+ #:with args_norm (stx-map normalize #'args)
+ #:with res (normalize #'(#%plain-app . args_norm))
+ (transfer-stx-props #'res τ #:ctx τ)]
+ [_ τ]))
+ (define old-eval (current-type-eval))
+ (current-type-eval (lambda (τ) (normalize (old-eval τ))))
+
+ (define old-type=? (current-type=?))
+ ; ty=? == syntax eq and syntax prop eq
+ (define (type=? t1 t2)
+ (let ([k1 (typeof t1)][k2 (typeof t2)])
+ (and (or (and (not k1) (not k2)) ; need this bc there's no current-kindcheck-rel
+ (and k1 k2 ((current-kind=?) k1 k2)))
+ (old-type=? t1 t2))))
+ (current-type=? type=?)
+ ;; TODO: add current-kindcheck-rel
+ (current-typecheck-relation (current-type=?)))
+
+;; kinds ----------------------------------------------------------------------
+(define-internal-kind-constructor ★ #:arity >= 0) ; defines ★-
+(define-syntax (★ stx)
+ (syntax-parse stx
+ [:id (mk-kind #'(★-))]
+ [(_ k:kind ...) (mk-kind #'(★- k.norm ...))]))
+
+(define-kind-constructor ⇒ #:arity >= 1)
+
+;; types ----------------------------------------------------------------------
+(define-typed-syntax (define-type-alias alias:id τ) ≫
+ [⊢ τ ≫ τ- ⇒ k_τ]
+ #:fail-unless ((current-kind?) #'k_τ)
+ (format "not a valid type: ~a\n" (type->str #'τ))
+ ------------------
+ [≻ (define-syntax- alias
+ (make-variable-like-transformer #'τ-))])
+
+(define-base-type Int : ★)
+(define-base-type Bool : ★)
+(define-base-type String : ★)
+(define-base-type Float : ★)
+(define-base-type Char : ★)
+
+(define-internal-type-constructor →) ; defines →-
+(define-typed-syntax (→ ty ...+) ≫
+ [⊢ ty ≫ ty- ⇒ (~★ . _)] ...
+ --------
+ [⊢ (→- ty- ...) ⇒ ★])
+
+(define-internal-binding-type ∀) ; defines ∀-
+(define-typed-syntax ∀ #:datum-literals (:)
+ [(_ ([tv:id : k_in:kind] ...) ty) ≫
+ [[tv ≫ tv- : k_in.norm] ... ⊢ ty ≫ ty- ⇒ (~★ . _)]
+ -------
+ [⊢ (∀- (tv- ...) ty-) ⇒ (★ k_in.norm ...)]])
+
+(define-typed-syntax (tyλ bvs:kind-ctx τ_body) ≫
+ [[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
+ #:fail-unless ((current-kind?) #'k_body)
+ (format "not a valid type: ~a\n" (type->str #'τ_body))
+ --------
+ [⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)])
+
+(define-typed-syntax (tyapp τ_fn τ_arg ...) ≫
+ [⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)]
+ #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
+ (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
+ [⊢ τ_arg ≫ τ_arg- ⇐ k_in] ...
+ --------
+ [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out])
+
+;; terms ----------------------------------------------------------------------
+(define-typed-syntax λ #:datum-literals (:)
+ [(_ ([x:id : τ_in:type] ...) e) ≫
+ [[x ≫ x- : τ_in.norm] ... ⊢ e ≫ e- ⇒ τ_out]
+ -------
+ [⊢ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]]
+ [(_ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫
+ [[x ≫ x- : τ_in] ... ⊢ e ≫ e- ⇐ τ_out]
+ ---------
+ [⊢ (λ- (x- ...) e-)]])
+
+(define-typed-syntax (#%app e_fn e_arg ...) ≫
+ [⊢ e_fn ≫ e_fn- ⇒ (~→ τ_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- ...) ⇒ τ_out])
+
+(define-typed-syntax (ann e (~datum :) τ:type) ≫
+ [⊢ e ≫ e- ⇐ τ.norm]
+ --------
+ [⊢ e- ⇒ τ.norm])
+
+(define-typed-syntax #%datum
+ [(_ . b:boolean) ≫
+ --------
+ [⊢ (#%datum- . b) ⇒ Bool]]
+ [(_ . s:str) ≫
+ --------
+ [⊢ (#%datum- . s) ⇒ String]]
+ [(_ . f) ≫
+ #:when (flonum? (syntax-e #'f))
+ --------
+ [⊢ (#%datum- . f) ⇒ Float]]
+ [(_ . c:char) ≫
+ --------
+ [⊢ (#%datum- . c) ⇒ Char]]
+ [(_ . n:integer) ≫
+ --------
+ [⊢ (#%datum- . n) ⇒ Int]]
+ [(_ . x) ≫
+ --------
+ [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
+
+(define-typed-syntax (Λ bvs:kind-ctx e) ≫
+ [([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
+ --------
+ [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
+
+(define-typed-syntax (inst e τ ...) ≫
+ [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~★ k ...))]
+ [⊢ τ ≫ τ- ⇐ k] ...
+ #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
+ --------
+ [⊢ e- ⇒ τ-inst])
+
diff --git a/turnstile/examples/tests/fomega-no-reuse-tests.rkt b/turnstile/examples/tests/fomega-no-reuse-tests.rkt
@@ -0,0 +1,213 @@
+#lang s-exp "../fomega-no-reuse.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; identical to fomega-tests.rkt
+
+(check-type Int : ★)
+(check-type String : ★)
+(typecheck-fail →)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
+(typecheck-fail (→ 1))
+(check-type 1 : Int)
+
+(typecheck-fail (tyλ ([x : ★]) 1) #:with-msg "not a valid type: 1")
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+(check-not-type (Λ ([X : ★]) (λ ([x : X]) x)) :
+ (∀ ([X : (★ ★)]) (→ X X)))
+
+;(check-type (∀ ([t : ★]) (→ t t)) : ★)
+(check-type (∀ ([t : ★]) (→ t t)) : (★ ★))
+(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+ : (∀ ([X : ★]) (→ X X)))
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
+
+(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
+(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
+(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
+(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
+(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
+(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
+
+(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
+(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+
+;; partial-apply →
+(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
+ : (⇒ ★ ★))
+;; f's type must have kind ★
+(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
+ (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
+(check-type (inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ : (→ (→ Int String) (→ Int String)))
+(typecheck-fail
+ (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
+ #:with-msg "inst: type mismatch: expected ★, given Int\n *expression: 1")
+
+(typecheck-fail
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+ #:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
+;; applied f too early
+(typecheck-fail
+ (inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ #:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
+(check-type ((inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ (λ ([x : Int]) "int")) : (→ Int String))
+(check-type (((inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ (λ ([x : Int]) "int")) 1) : String ⇒ "int")
+
+;; tapl examples, p441
+(typecheck-fail
+ (define-type-alias tmp 1)
+ #:with-msg "not a valid type: 1")
+(define-type-alias Id (tyλ ([X : ★]) X))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
+
+;; tapl examples, p451
+(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+
+;(check-type Pair : (⇒ ★ ★ ★))
+(check-type Pair : (⇒ ★ ★ (★ ★)))
+
+(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+; parametric pair constructor
+(check-type
+ (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X : ★][Y : ★]) (→ X Y (tyapp Pair X Y))))
+; concrete Pair Int String constructor
+(check-type
+ (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String)
+ : (→ Int String (tyapp Pair Int String)))
+;; Pair Int String value
+(check-type
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String) 1 "1")
+ : (tyapp Pair Int String))
+;; fst: parametric
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) X)))
+;; fst: concrete Pair Int String accessor
+(check-type
+ (inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ Int String)
+ : (→ (tyapp Pair Int String) Int))
+;; apply fst
+(check-type
+ ((inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ Int String)
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String) 1 "1"))
+ : Int ⇒ 1)
+;; snd
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) Y)))
+(check-type
+ (inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ Int String)
+ : (→ (tyapp Pair Int String) String))
+(check-type
+ ((inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ Int String)
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String) 1 "1"))
+ : String ⇒ "1")
+
+;; sysf tests wont work, unless augmented with kinds
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+ : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+ : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+ : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
+(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
+; first inst should be discarded
+(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
+; second inst is discarded
+(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
+
+;; polymorphic arguments
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
+(check-type
+ (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
+(check-type
+ ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
+ : Int ⇒ 10)
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
+ (Λ ([s : ★]) (λ ([y : s]) y)))
+ : Int ⇒ 10)
+
+
+;; previous tests -------------------------------------------------------------
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+;(typecheck-fail #f) ; unsupported literal
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+ : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
diff --git a/turnstile/examples/tests/run-all-tests.rkt b/turnstile/examples/tests/run-all-tests.rkt
@@ -26,6 +26,7 @@
(require "fomega-tests.rkt")
(require "fomega2-tests.rkt")
(require "fomega3-tests.rkt")
+(require "fomega-no-reuse-tests.rkt")
;; these are not ported to turnstile yet
;; see macrotypes/examples/tests/run-all-tests.rkt
diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl
@@ -150,7 +150,12 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
Defines a type constructor that does not bind type variables.
Defining a type constructor @racket[τ] defines:
@itemlist[@item{@racket[τ], a macro for constructing an instance of type
- @racket[τ], with the specified arity.}
+ @racket[τ], with the specified arity.
+ Validates inputs and expands to @racket[τ-], attaching kind.}
+ @item{@racket[τ-], an internal macro that expands to the internal
+ (i.e., fully expanded) type representation. Does not validate
+ inputs or attach kinds. This macro is useful when creating
+ a separate kind system, see @racket[define-internal-type-constructor].}
@item{@racket[τ?], a phase 1 predicate recognizing type @racket[τ].}
@item{@racket[~τ], a phase 1 @tech:pat-expander recognizing type @racket[τ].}]
@@ -184,6 +189,15 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
The @racket[#:extra-info] argument is useful for attaching additional
metainformation to types, for example to implement pattern matching.}}
@item{
+ @defform[(define-internal-type-constructor name-id option ...)
+ #:grammar
+ ([option (code:line #:arity op n)
+ (code:line #:arg-variances expr)
+ (code:line #:extra-info stx)])]{
+ Like @racket[define-type-constructor], except the surface macro is not defined.
+ Use this form, for example, when creating a separate kind system so that
+ you can still use other Turnstile conveniences like pattern expanders.}}
+ @item{
@defform[(define-binding-type name-id option ...)
#:grammar
([option (code:line #:arity op n)
@@ -207,6 +221,15 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
on the type variables. The @racket[#:arr] argument is an "arrow" that "saves"
the annotations after a type is expanded and annotations are erased,
analogous to how → "saves" the type annotations on a lambda.}}
+ @item{
+ @defform[(define-internal-binding-type name-id option ...)
+ #:grammar
+ ([option (code:line #:arity op n)
+ (code:line #:bvs op n)
+ (code:line #:arr kindcon)
+ (code:line #:arg-variances expr)
+ (code:line #:extra-info stx)])]{
+ Analogous to @racket[define-internal-type-constructor].}}
@item{
@defform[(type-out ty-id)]{
A @racket[provide]-spec that, given @racket[ty-id], provides @racket[ty-id],
