From a64ba6c07598f3772193b7596011b047db2751a5 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Mon, 30 Jan 2017 17:16:28 -0500 Subject: [PATCH] WIP: dont overload ': key, eg use separate key for kinds --- macrotypes/examples/fomega.rkt | 24 ++-- macrotypes/examples/tests/fomega-tests.rkt | 124 +++++++++++---------- macrotypes/typecheck.rkt | 10 +- 3 files changed, 83 insertions(+), 75 deletions(-) diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt index 338916b..edbe824 100644 --- a/macrotypes/examples/fomega.rkt +++ b/macrotypes/examples/fomega.rkt @@ -34,13 +34,18 @@ (current-type? (λ (t) (define k (kindof t)) #;(or (type? t) (★? (typeof t)) (∀★? (typeof t))) - (and ((current-kind?) k) (not (⇒? k)))))) + (and k ((current-kind?) k) (not (⇒? k))))) + ;; o.w., a valid type is one with any valid kind + (current-any-type? (λ (t) + (define k (kindof t)) + (and k ((current-kind?) k))))) + ; must override, to handle kinds (define-syntax define-type-alias (syntax-parser [(_ alias:id τ) - #:with (τ- k_τ) (infer+erase #'τ) + #:with (τ- k_τ) (infer+erase #'τ #:tag '::) #:fail-unless ((current-kind?) #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ)) #'(define-syntax alias @@ -96,31 +101,32 @@ (⊢ e- : (∀ ([tv- :: bvs.kind] ...) τ_e))]) (define-typed-syntax inst - [(_ e τ ...) + [(_ e τ:any-type ...) #:with [e- τ_e] (infer+erase #'e) #:with (~∀ (tv ...) τ_body) #'τ_e #:with (~∀★ k ...) (kindof #'τ_e) - #:with ([τ- k_τ] ...) (infers+erase #'(τ ...)) +; #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:tag '::) + #:with (k_τ ...) (stx-map kindof #'(τ.norm ...)) #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...)) - #:with τ_inst (substs #'(τ- ...) #'(tv ...) #'τ_body) + #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body) (⊢ e- : τ_inst)]) ;; TODO: merge with regular λ and app? ;; - see fomega2.rkt (define-typed-syntax tyλ [(_ bvs:kind-ctx τ_body) - #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body) - #:do [(displayln (stx->datum #'k_body))] + #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:tag '::) #:fail-unless ((current-kind?) #'k_body) (format "not a valid type: ~a\n" (type->str #'τ_body)) (⊢ (λ- tvs- τ_body-) :: (⇒ bvs.kind ... k_body))]) (define-typed-syntax tyapp [(_ τ_fn τ_arg ...) - #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒) - #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...)) +; #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒) + #:with [τ_fn- (~⇒ k_in ... k_out)] (infer+erase #'τ_fn #:tag '::) + #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:tag '::) #:fail-unless (kindchecks? #'(k_arg ...) #'(k_in ...)) (string-append (format diff --git a/macrotypes/examples/tests/fomega-tests.rkt b/macrotypes/examples/tests/fomega-tests.rkt index fe02edc..3abafe8 100644 --- a/macrotypes/examples/tests/fomega-tests.rkt +++ b/macrotypes/examples/tests/fomega-tests.rkt @@ -28,73 +28,75 @@ (Λ ([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 (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")) +(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\n *expected: +★\n *given: +Int\n *expressions: 1") +;; 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:.*not a valid type: 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") +(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, 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)))) +;; tapl examples, p451 +(define-type-alias Pair (tyλ ([A :: ★] [B :: ★]) (∀ ([X :: ★]) (→ (→ A B X) X)))) -;; ;(check-type Pair : (⇒ ★ ★ ★)) -;; (check-type Pair : (⇒ ★ ★ (∀★ ★))) +;(check-type Pair : (⇒ ★ ★ ★)) +(check-type Pair :: (⇒ ★ ★ (∀★ ★))) ;; (check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X))) ;; ; parametric pair constructor diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index c0812a1..a5185a4 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -322,9 +322,9 @@ #:fail-when #t (format (string-append - "Improperly formatted ~a annotation: ~a; should have shape [x : τ], " + "Improperly formatted ~a annotation: ~a; should have shape [x ~a τ], " "where τ is a valid ~a.") - 'name (type->str #'any) 'name) + 'name (type->str #'any) 'key1 'name) #:attr x #f #:attr type #f)) (define-syntax-class type-ctx #:attributes ((x 1) (type 1)) @@ -657,7 +657,7 @@ (define-internal-binding-type τ . other-options) (define-syntax (τ stx) (syntax-parse stx - [(~var _ id) #'τ-] ; defer to τ- error + [(~var _ id) (add-orig (syntax/loc stx τ-) stx)] ; defer to τ- error [(_ (~or (bv:id (... (... ...))) (~and (~fail #:unless #,(attribute has-annotations?)) bvs+ann)) @@ -689,11 +689,11 @@ ;; Type assignment macro for nicer syntax (define-syntax (⊢ stx) (syntax-parse stx - [(_ e tag τ) #'(assign-type #`e #`τ)] + [(_ e tag τ) #'(attach #`e 'tag ((current-type-eval) #`τ))] [(_ e τ) #'(⊢ e : τ)])) (define-syntax (⊢/no-teval stx) (syntax-parse stx - [(_ e tag τ) #'(fast-assign-type #`e #`τ)] + [(_ e tag τ) #'(attach #`e 'tag ((current-type-eval) #`τ))] [(_ e τ) #'(⊢/no-teval e : τ)])) ;; Actual type assignment function.