WIP: dont overload ': key, eg use separate key for kinds
This commit is contained in:
Stephen Chang
parent
127a194e77
commit
a64ba6c075
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user