From a0ebecf09a245617ec0bfc4ae8ec48f8b67d0eba Mon Sep 17 00:00:00 2001 From: Mitch Gamburg Date: Mon, 5 Apr 2021 17:40:40 -0400 Subject: [PATCH 1/3] merge conflict --- .../turnstile/examples/cs478/current/stlc-prog.rkt | 2 ++ .../turnstile/examples/cs478/current/stlc.rkt | 14 +++++++++++--- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt b/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt index 3f20a459..f60d420d 100644 --- a/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt +++ b/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt @@ -253,3 +253,5 @@ ;; tuples (check-type (tup 1 #f unit) : (× Nat Bool)) + +;; diff --git a/turnstile-example/turnstile/examples/cs478/current/stlc.rkt b/turnstile-example/turnstile/examples/cs478/current/stlc.rkt index acdd0bed..c854f5c3 100644 --- a/turnstile-example/turnstile/examples/cs478/current/stlc.rkt +++ b/turnstile-example/turnstile/examples/cs478/current/stlc.rkt @@ -5,6 +5,11 @@ (rename-out [typed-datum #%datum] [typed-app #%app] [typed-define define])) + +(define-type-constructor Ref #:arity = 1) +(define-type-constructor Source #:arity = 1) +(define-type-constructor Sink #:arity = 1) +(define-type-constructor List #:arity = 1) (define-base-types Top Int Bool Unit) (define-type-constructor → #:arity = 2) @@ -570,19 +575,20 @@ ;;------- references ----------- -(define-type-constructor Ref #:arity = 1) +(provide Ref Source Sink ref get set!) + (define-typerule (ref e) ≫ [⊢ e ≫ e- ⇒ τ] --------------- [⊢ (box- e-) ⇒ (Ref τ)]) (define-typerule (get b) ≫ - [⊢ b ≫ b- ⇒ (~Ref τ)] + [⊢ b ≫ b- ⇒ (~Source τ)] ---------------------- [⊢ (unbox- b-) ⇒ τ]) (define-typerule (set! b v) ≫ - [⊢ b ≫ b- ⇒ (~Ref τ)] + [⊢ b ≫ b- ⇒ (~Sink τ)] [⊢ v ≫ v- ⇐ τ] ---------------------- [⊢ (set-box!- b- v-) ⇒ Unit]) @@ -624,6 +630,8 @@ [((~List τ1) (~List τ2)) (subtype? #'τ1 #'τ2)] [((~Ref τ1) (~Ref τ2)) (and (subtype? #'τ1 #'τ2) (subtype? #'τ2 #'τ1))] + [((~Ref τ1) (~Source τ2)) (subtype? #'τ1 #'τ2)] + [((~Ref τ1) (~Sink τ2)) (subtype? #'τ2 #'τ1)] [(_ ~Top) #t] [(_ _) #f]))) From 38a0f8420f3b6297dc223570fc32ddc9991e2535 Mon Sep 17 00:00:00 2001 From: Mitch Gamburg Date: Thu, 8 Apr 2021 10:56:02 -0400 Subject: [PATCH 2/3] intersection --- .../turnstile/examples/cs478/current/stlc-prog.rkt | 12 +++++++++++- .../turnstile/examples/cs478/current/stlc.rkt | 8 ++++++-- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt b/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt index f60d420d..8582417c 100644 --- a/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt +++ b/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt @@ -254,4 +254,14 @@ ;; tuples (check-type (tup 1 #f unit) : (× Nat Bool)) -;; +;; new Ref type +(define getter (λ [x : (Source Int)] (get x))) +(define int-ref (ref 5)) + +(check-type (getter int-ref) : Int) + +(define add-record-values (λ [r : (∩ (Rec [x = Int]) (Rec [y = Int]))] (* (proj r x) (proj r y)))) + +(define arbitrary-record (rec [x = 3] [y = 4] [z = 5])) + +(check-type (add-record-values arbitrary-record) : Int -> 12) diff --git a/turnstile-example/turnstile/examples/cs478/current/stlc.rkt b/turnstile-example/turnstile/examples/cs478/current/stlc.rkt index c854f5c3..2d18f09e 100644 --- a/turnstile-example/turnstile/examples/cs478/current/stlc.rkt +++ b/turnstile-example/turnstile/examples/cs478/current/stlc.rkt @@ -13,6 +13,10 @@ (define-base-types Top Int Bool Unit) (define-type-constructor → #:arity = 2) +(define-type-constructor ∩ #:arity = 2) + +(provide ∩) + (define-typed-variable unit '() ⇒ Unit) (define-typerule (typed-define x:id e) ≫ @@ -483,8 +487,6 @@ (provide List nil cons isnil head tail) -(define-type-constructor List #:arity = 1) - (define-typerule nil [nil:id ≫ ------ @@ -632,6 +634,8 @@ (and (subtype? #'τ1 #'τ2) (subtype? #'τ2 #'τ1))] [((~Ref τ1) (~Source τ2)) (subtype? #'τ1 #'τ2)] [((~Ref τ1) (~Sink τ2)) (subtype? #'τ2 #'τ1)] + [((∩ τ1 τ2) τ3) (or (subtype? #'τ1 #'τ3) (subtype? #'τ2 #'τ3))] + [(τ (∩ τ1 τ2)) (and (subtype? #'τ #'τ1) (subtype? #'τ #'τ2))] [(_ ~Top) #t] [(_ _) #f]))) From a66b088a58cbe2d5d90df5bba057bd473f0a8092 Mon Sep 17 00:00:00 2001 From: Mitch Gamburg Date: Thu, 22 Apr 2021 11:00:57 -0400 Subject: [PATCH 3/3] polymorphism wip --- .../examples/cs478/current/stlc-prog.rkt | 2 ++ .../turnstile/examples/cs478/current/stlc.rkt | 35 +++++++++++++------ 2 files changed, 27 insertions(+), 10 deletions(-) diff --git a/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt b/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt index b973b998..c4d734e7 100644 --- a/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt +++ b/turnstile-example/turnstile/examples/cs478/current/stlc-prog.rkt @@ -396,3 +396,5 @@ (check-type (cons 1 (cons 3 nil)) : IntList) (check-type (isnil nil) : Bool) (check-type (isnil nil) : Bool -> #t) + +(check-type (Λ V (λ ([x : V]) x)) : (∀ (V) (→ V V))) diff --git a/turnstile-example/turnstile/examples/cs478/current/stlc.rkt b/turnstile-example/turnstile/examples/cs478/current/stlc.rkt index bed441d9..a41c7f7f 100644 --- a/turnstile-example/turnstile/examples/cs478/current/stlc.rkt +++ b/turnstile-example/turnstile/examples/cs478/current/stlc.rkt @@ -1,6 +1,6 @@ #lang turnstile/quicklang -(provide Int Bool Unit → #%type +(provide Int Bool Unit → #%type Λ ∀ λ unit ascribe if succ pred iszero vals * fix (rename-out [typed-datum #%datum] [typed-app #%app] [typed-define define])) @@ -12,6 +12,7 @@ (define-type-constructor List #:arity = 1) (define-base-types Top Int Bool Unit) (define-type-constructor → #:arity >= 1) +(define-binding-type ∀ #:arity = 1 #:bvs = 1) (define-type-constructor ∩ #:arity = 2) @@ -150,13 +151,19 @@ ------------ [#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]]) -(define-typed-syntax (typed-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 typed-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]] + [(_ e τ) ≫ + [⊢ τ ≫ τ- ⇐ :: #%type] + [⊢ e ≫ e- ⇒ (~∀ (X) τ2)] + ------------------------- + [⊢ e- ⇒ ($subst τ2 X τ)]]) #;(define-typerule (typed-app e1 e2) ≫ [⊢ e1 ≫ e1- ⇒ (~→ T1 T2)] @@ -617,8 +624,6 @@ ;; either: invariant, covariant, contravariant (define current-ref-variance (make-parameter 'covariant))) -(define-type-constructor Ref #:arity = 1) - (define-typerule (ref e) ≫ [⊢ e ≫ e- ⇒ τ] --------------- @@ -793,3 +798,13 @@ #:fail-when (stx-contains-id? #'ty #'f) "cannot have self-reference" #'(define-syntax f (make-type-alias-transformer #'(x ...) #'ty))])) + +;; What needs to happen? +;; - We introduce a new type of expression that introduces a type variable +;; - We have a new type of expression that does type application + + +(define-typerule (Λ X e) ≫ + [[X ≫ X- :: #%type] ⊢ e ≫ e- ⇒ τ] + ----------------- + [⊢ e- ⇒ (∀ (X) τ)])