diff --git a/macrotypes/examples/exist.rkt b/macrotypes/examples/exist.rkt index 4ae06aa..47370ef 100644 --- a/macrotypes/examples/exist.rkt +++ b/macrotypes/examples/exist.rkt @@ -9,17 +9,19 @@ ;; - terms from stlc+reco+var.rkt ;; - pack and open +(provide ∃ pack open) + (define-type-constructor ∃ #:bvs = 1) (define-typed-syntax pack - [(pack (τ:type e) as ∃τ:type) + [(_ (τ:type e) as ∃τ:type) #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm #:with [e- τ_e] (infer+erase #'e) #:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body)) (⊢ e- : ∃τ.norm)]) (define-typed-syntax open #:datum-literals (<=) - [(open [x:id <= e_packed with X:id] e) + [(_ [x:id <= e_packed with X:id] e) ;; The subst below appears to be a hack, but it's not really. ;; It's the (TaPL) type rule itself that is fast and loose. ;; Leveraging the macro system's management of binding reveals this. diff --git a/macrotypes/examples/ext-stlc.rkt b/macrotypes/examples/ext-stlc.rkt index 48e5774..509ac1e 100644 --- a/macrotypes/examples/ext-stlc.rkt +++ b/macrotypes/examples/ext-stlc.rkt @@ -15,15 +15,21 @@ ;; - begin ;; - ascription (ann) ;; - let, let*, letrec +;; Top-level: +;; - define (values only) +;; - define-type-alias -(provide (for-syntax current-join) - ⊔ zero? = +(provide define-type-alias + (for-syntax current-join) ⊔ + (type-out Bool String Float Char Unit) + zero? = (rename-out [typed- -] [typed* *]) ;; test all variations of typed-out (typed-out [add1 (→ Int Int)] [sub1 : (→ Int Int)] [[not- (→ Bool Bool)] not] - [[void- : (→ Unit)] void])) + [[void- : (→ Unit)] void]) + define #%datum and or if begin ann let let* letrec) (define-base-types Bool String Float Char Unit) @@ -33,28 +39,51 @@ (define-primop typed- - (→ Int Int Int)) (define-primop typed* * : (→ Int Int Int)) +;; Using τ.norm leads to a "not valid type" error when file is compiled +(define-syntax define-type-alias + (syntax-parser + [(_ alias:id τ:type) + #'(define-syntax- alias + (make-variable-like-transformer #'τ))] + [(_ (f:id x:id ...) ty) + #'(define-syntax- (f stx) + (syntax-parse stx + [(_ x ...) #'ty]))])) + +(define-typed-syntax define + [(_ x:id e) + #:with (e- τ) (infer+erase #'e) + #:with y (generate-temporary) + #'(begin- + (define-syntax x (make-rename-transformer (⊢ y : τ))) + (define- y e-))]) + (define-typed-syntax #%datum - [(#%datum . b:boolean) (⊢ #,(syntax/loc stx (#%datum- . b)) : Bool)] - [(#%datum . s:str) (⊢ #,(syntax/loc stx (#%datum- . s)) : String)] - [(#%datum . f) #:when (flonum? (syntax-e #'f)) (⊢ #,(syntax/loc stx (#%datum- . f)) : Float)] - [(#%datum . c:char) (⊢ #,(syntax/loc stx (#%datum- . c)) : Char)] - [(#%datum . x) (syntax/loc stx (stlc+lit:#%datum . x))]) + [(_ . b:boolean) (⊢ #,(syntax/loc stx (#%datum- . b)) : Bool)] + [(_ . s:str) (⊢ #,(syntax/loc stx (#%datum- . s)) : String)] + [(_ . f) #:when (flonum? (syntax-e #'f)) + (⊢ #,(syntax/loc stx (#%datum- . f)) : Float)] + [(_ . c:char) (⊢ #,(syntax/loc stx (#%datum- . c)) : Char)] + [(_ . x) (syntax/loc stx (stlc+lit:#%datum . x))]) (define-typed-syntax and - [(and e1 e2) + [(_ e1 e2) #:with Bool* ((current-type-eval) #'Bool) #:with [e1- τ_e1] (infer+erase #'e1) #:with [e2- τ_e2] (infer+erase #'e2) - #:fail-unless (typecheck? #'τ_e1 #'Bool*) (typecheck-fail-msg/1 #'Bool* #'τ_e1 #'e1) - #:fail-unless (typecheck? #'τ_e2 #'Bool*) (typecheck-fail-msg/1 #'Bool* #'τ_e2 #'e2) + #:fail-unless (typecheck? #'τ_e1 #'Bool*) + (typecheck-fail-msg/1 #'Bool* #'τ_e1 #'e1) + #:fail-unless (typecheck? #'τ_e2 #'Bool*) + (typecheck-fail-msg/1 #'Bool* #'τ_e2 #'e2) (⊢ (and- e1- e2-) : Bool)]) (define-typed-syntax or - [(or e ...) + [(_ e ...) #:with ([_ Bool*] ...) #`([e #,((current-type-eval) #'Bool)] ...) #:with ([e- τ_e] ...) (infers+erase #'(e ...)) #:fail-unless (typechecks? #'(τ_e ...) #'(Bool* ...)) - (typecheck-fail-msg/multi #'(Bool* ...) #'(τ_e ...) #'(e ...)) + (typecheck-fail-msg/multi + #'(Bool* ...) #'(τ_e ...) #'(e ...)) (⊢ (or- e- ...) : Bool)]) (begin-for-syntax @@ -75,7 +104,7 @@ ((current-join) τ τ2))])) (define-typed-syntax if - [(if e_tst e1 e2) + [(_ e_tst e1 e2) #:with τ-expected (get-expected-type stx) #:with [e_tst- _] (infer+erase #'e_tst) #:with e1_ann #'(add-expected e1 τ-expected) @@ -85,24 +114,24 @@ (⊢ (if- e_tst- e1- e2-) : (⊔ τ1 τ2))]) (define-typed-syntax begin - [(begin e_unit ... e) - #:with ([e_unit- _] ...) (infers+erase #'(e_unit ...)) ;(⇑s (e_unit ...) as Unit) + [(_ e_unit ... e) + #:with ([e_unit- _] ...) (infers+erase #'(e_unit ...)) #:with (e- τ) (infer+erase #'e) (⊢ (begin- e_unit- ... e-) : τ)]) -(define-typed-syntax ann - #:datum-literals (:) - [(ann e : ascribed-τ:type) +(define-typed-syntax ann #:datum-literals (:) + [(_ e : ascribed-τ:type) #:with (e- τ) (infer+erase #'(add-expected e ascribed-τ.norm)) #:fail-unless (typecheck? #'τ #'ascribed-τ.norm) (typecheck-fail-msg/1 #'ascribed-τ.norm #'τ #'e) (⊢ e- : ascribed-τ)]) (define-typed-syntax let - [(let ([x e] ...) e_body) + [(_ ([x e] ...) e_body) #:with τ-expected (get-expected-type stx) #:with ((e- τ) ...) (infers+erase #'(e ...)) - #:with ((x- ...) e_body- τ_body) (infer/ctx+erase #'([x τ] ...) #'(add-expected e_body τ-expected)) + #:with ((x- ...) e_body- τ_body) + (infer/ctx+erase #'([x τ] ...) #'(add-expected e_body τ-expected)) #:fail-unless (or (not (syntax-e #'τ-expected)) ; no expected type (typecheck? #'τ_body ((current-type-eval) #'τ-expected))) (typecheck-fail-msg/1 #'τ-expected #'τ_body #'e_body) @@ -113,19 +142,17 @@ ; - only need to transfer expected type when local expanding an expression ; - see let/tc (define-typed-syntax let* - [(let* () e_body) + [(_ () e_body) #:with τ-expected (get-expected-type stx) #'e_body] - [(let* ([x e] [x_rst e_rst] ...) e_body) + [(_ ([x e] [x_rst e_rst] ...) e_body) #:with τ-expected (get-expected-type stx) #'(let ([x e]) (let* ([x_rst e_rst] ...) e_body))]) (define-typed-syntax letrec - [(letrec ([b:type-bind e] ...) e_body) + [(_ ([b:type-bind e] ...) e_body) #:with ((x- ...) (e- ... e_body-) (τ ... τ_body)) (infers/ctx+erase #'(b ...) #'((add-expected e b.type) ... e_body)) #:fail-unless (typechecks? #'(b.type ...) #'(τ ...)) (typecheck-fail-msg/multi #'(b.type ...) #'(τ ...) #'(e ...)) (⊢ (letrec- ([x- e-] ...) e_body-) : τ_body)]) - - diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt index 9fe72b5..56585c5 100644 --- a/macrotypes/examples/fomega.rkt +++ b/macrotypes/examples/fomega.rkt @@ -1,5 +1,5 @@ #lang s-exp macrotypes/typecheck -(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst) +(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst) (reuse String #%datum #:from "stlc+reco+var.rkt") ;; System F_omega @@ -12,6 +12,11 @@ ;; - add tyλ and tyapp ;; - #%datum from stlc+reco+var +(provide (for-syntax current-kind?) + define-type-alias + (type-out ★ ⇒ ∀★ ∀) + Λ inst tyλ tyapp) + (define-syntax-category kind) ; want #%type to be equiv to★ @@ -24,23 +29,26 @@ ;; eg in the definition of λ or previous type constuctors. ;; (However, this is not completely possible, eg define-type-alias) ;; So now "type?" no longer validates types, rather it's a subset. - ;; But we no longer need type? to validate types, instead we can use (kind? (typeof t)) + ;; But we no longer need type? to validate types, instead we can use + ;; (kind? (typeof t)) (current-type? (λ (t) (define k (typeof t)) #;(or (type? t) (★? (typeof t)) (∀★? (typeof t))) (and ((current-kind?) k) (not (⇒? k)))))) ; must override, to handle kinds -(provide define-type-alias) (define-syntax define-type-alias (syntax-parser [(_ alias:id τ) #:with (τ- k_τ) (infer+erase #'τ) - #:fail-unless ((current-kind?) #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ)) - #'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))])) + #:fail-unless ((current-kind?) #'k_τ) + (format "not a valid type: ~a\n" (type->str #'τ)) + #'(define-syntax alias + (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))])) -(provide ★ (for-syntax ★?)) -(define-for-syntax ★? #%type?) +(begin-for-syntax + (define ★? #%type?) + (define-syntax ~★ (lambda _ (error "~★ not implemented")))) ; placeholder (define-syntax ★ (make-rename-transformer #'#%type)) (define-kind-constructor ⇒ #:arity >= 1) (define-kind-constructor ∀★ #:arity >= 0) @@ -83,39 +91,41 @@ (current-typecheck-relation (current-type=?))) (define-typed-syntax Λ - [(Λ bvs:kind-ctx e) + [(_ bvs:kind-ctx e) #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e) (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]) (define-typed-syntax inst - [(inst e τ ...) + [(_ e τ ...) #:with [e- τ_e] (infer+erase #'e) #:with (~∀ (tv ...) τ_body) #'τ_e #:with (~∀★ k ...) (typeof #'τ_e) #:with ([τ- k_τ] ...) (infers+erase #'(τ ...)) #:fail-unless (typechecks? #'(k_τ ...) #'(k ...)) - (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...)) + (typecheck-fail-msg/multi + #'(k ...) #'(k_τ ...) #'(τ ...)) #:with τ_inst (substs #'(τ- ...) #'(tv ...) #'τ_body) (⊢ e- : τ_inst)]) ;; TODO: merge with regular λ and app? ;; - see fomega2.rkt (define-typed-syntax tyλ - [(tyλ bvs:kind-ctx τ_body) + [(_ bvs:kind-ctx τ_body) #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body) #: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 - [(tyapp τ_fn τ_arg ...) + [(_ τ_fn τ_arg ...) #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒) #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...)) #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...)) (string-append - (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), " - (syntax-source stx) (syntax-line stx) (syntax-column stx) - (syntax->datum #'τ_fn)) + (format + "~a (~a:~a) Arguments to function ~a have wrong kinds(s), " + (syntax-source stx) (syntax-line stx) (syntax-column stx) + (syntax->datum #'τ_fn)) "or wrong number of arguments:\nGiven:\n" (string-join (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line diff --git a/macrotypes/examples/fomega2.rkt b/macrotypes/examples/fomega2.rkt index 27aef1d..6f6ec00 100644 --- a/macrotypes/examples/fomega2.rkt +++ b/macrotypes/examples/fomega2.rkt @@ -1,5 +1,5 @@ #lang s-exp macrotypes/typecheck -(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst) +(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst) (reuse String #%datum #:from "stlc+reco+var.rkt") ; same as fomega.rkt except here λ and #%app works as both type and terms @@ -15,6 +15,10 @@ ;; - extend ∀ Λ inst from sysf ;; - #%datum from stlc+reco+var +(provide define-type-alias + ★ ∀★ ∀ + Λ inst) + (define-syntax-category kind) (begin-for-syntax @@ -23,19 +27,20 @@ ;; eg in the definition of λ or previous type constuctors. ;; (However, this is not completely possible, eg define-type-alias) ;; So now "type?" no longer validates types, rather it's a subset. - ;; But we no longer need type? to validate types, instead we can use (kind? (typeof t)) + ;; But we no longer need type? to validate types, instead we can use + ;;(kind? (typeof t)) (current-type? (λ (t) (or (type? t) (let ([k (typeof t)]) (or (★? k) (∀★? k))) ((current-kind?) t))))) ; must override -(provide define-type-alias) (define-syntax define-type-alias (syntax-parser [(_ alias:id τ) #:with (τ- k_τ) (infer+erase #'τ) - #'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))])) + #'(define-syntax alias + (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))])) (define-base-kind ★) (define-kind-constructor ∀★ #:arity >= 0) @@ -79,17 +84,18 @@ (current-typecheck-relation (current-type=?))) (define-typed-syntax Λ - [(Λ bvs:kind-ctx e) + [(_ bvs:kind-ctx e) #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e) (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]) (define-typed-syntax inst - [(inst e τ ...) + [(_ e τ ...) #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀) #:with ([τ- k_τ] ...) (infers+erase #'(τ ...)) - #:when (stx-andmap (λ (t k) (or ((current-kind?) k) - (type-error #:src t #:msg "not a valid type: ~a" t))) - #'(τ ...) #'(k_τ ...)) + #:when (stx-andmap + (λ (t k) (or ((current-kind?) k) + (type-error #:src t #:msg "not a valid type: ~a" t))) + #'(τ ...) #'(k_τ ...)) #:when (typechecks? #'(k_τ ...) #'(k ...)) (⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]) diff --git a/macrotypes/examples/fomega3.rkt b/macrotypes/examples/fomega3.rkt index 956f16a..2287210 100644 --- a/macrotypes/examples/fomega3.rkt +++ b/macrotypes/examples/fomega3.rkt @@ -1,8 +1,5 @@ #lang s-exp macrotypes/typecheck -(extends "sysf.rkt" #:except #%datum ∀ Λ inst) -(reuse String #%datum #:from "stlc+reco+var.rkt") -(require (only-in "fomega.rkt" current-kind? ∀★? ★? kind?)) -(reuse ★ ∀ Λ inst define-type-alias ∀★ #:from "fomega.rkt") +(extends "fomega.rkt" #:except tyapp tyλ) ; same as fomega2.rkt --- λ and #%app works as both regular and type versions, ; → is both type and kind --- but reuses parts of fomega.rkt, @@ -21,12 +18,14 @@ ;; types and kinds are now mixed, due to #%app and λ (begin-for-syntax - (current-kind? (λ (k) (or (#%type? k) (kind? k) (#%type? (typeof k))))) + (define old-kind? (current-kind?)) + (current-kind? (λ (k) (or (#%type? k) (old-kind? k) (#%type? (typeof k))))) ;; Try to keep "type?" backward compatible with its uses so far, ;; eg in the definition of λ or previous type constuctors. ;; (However, this is not completely possible, eg define-type-alias) ;; So now "type?" no longer validates types, rather it's a subset. - ;; But we no longer need type? to validate types, instead we can use (kind? (typeof t)) + ;; But we no longer need type? to validate types, instead we can use + ;; (kind? (typeof t)) (current-type? (λ (t) (or (type? t) (let ([k (typeof t)]) (or (★? k) (∀★? k))) diff --git a/macrotypes/examples/fsub.rkt b/macrotypes/examples/fsub.rkt index 1fe99cc..c7c79be 100644 --- a/macrotypes/examples/fsub.rkt +++ b/macrotypes/examples/fsub.rkt @@ -14,7 +14,9 @@ ;; - current-promote, expose ;; - extend current-sub? to call current-promote -(provide (typed-out [+ : (→ Nat Nat Nat)])) +(provide <: ∀ + (typed-out [+ : (→ Nat Nat Nat)]) + Λ inst) ; can't just call expose in type-eval, ; otherwise typevars will have bound as type, rather than instantiated type @@ -73,15 +75,16 @@ #:msg "Expected ∀ type, got: ~a" #'any))))])))) (define-typed-syntax Λ #:datum-literals (<:) - [(Λ ([tv:id <: τsub:type] ...) e) + [(_ ([tv:id <: τsub:type] ...) e) ;; NOTE: store the subtyping relation of tv and τsub in another ;; "environment", ie, a syntax property with another tag: '<: ;; The "expose" function looks for this tag to enforce the bound, ;; as in TaPL (fig 28-1) - #:with ((tv- ...) _ (e-) (τ_e)) (infer #'(e) #:tvctx #'([tv : #%type <: τsub] ...)) + #:with ((tv- ...) _ (e-) (τ_e)) + (infer #'(e) #:tvctx #'([tv : #%type <: τsub] ...)) (⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))]) (define-typed-syntax inst - [(inst e τ:type ...) + [(_ e τ:type ...) #:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀) #:when (typechecks? #'(τ.norm ...) #'(τ_sub ...)) (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]) diff --git a/macrotypes/examples/infer.rkt b/macrotypes/examples/infer.rkt index c7e388f..0f00879 100644 --- a/macrotypes/examples/infer.rkt +++ b/macrotypes/examples/infer.rkt @@ -1,33 +1,34 @@ #lang s-exp macrotypes/typecheck -(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not +(extends "ext-stlc.rkt" + #:except define #%app λ → + - void = zero? sub1 add1 not #:rename [~→ ~ext-stlc:→]) +(reuse cons [head hd] [tail tl] nil [isnil nil?] List list + #:from "stlc+cons.rkt") +(reuse tup × proj + #:from "stlc+tup.rkt") (require (only-in "sysf.rkt" ∀ ~∀ ∀? Λ)) -(reuse cons [head hd] [tail tl] nil [isnil nil?] List list #:from "stlc+cons.rkt") -(require (only-in "stlc+cons.rkt" ~List)) -(reuse tup × proj #:from "stlc+tup.rkt") -(reuse define-type-alias #:from "stlc+reco+var.rkt") (require (for-syntax "../type-constraints.rkt")) -(provide hd tl nil?) -(provide →) -;; a language with partial (local) type inference using bidirectional type checking +;; a language with local type inference using bidirectional type checking -(provide (typed-out [+ : (→ Int Int Int)] - [- : (→ Int Int Int)] - [void : (→ Unit)] - [= : (→ Int Int Bool)] - [zero? : (→ Int Bool)] - [sub1 : (→ Int Int)] - [add1 : (→ Int Int)] - [not : (→ Bool Bool)] - [abs : (→ Int Int)])) +(provide → + (typed-out [+ : (→ Int Int Int)] + [- : (→ Int Int Int)] + [void : (→ Unit)] + [= : (→ Int Int Bool)] + [zero? : (→ Int Bool)] + [sub1 : (→ Int Int)] + [add1 : (→ Int Int)] + [not : (→ Bool Bool)] + [abs : (→ Int Int)]) + define λ #%app) (define-syntax → ; wrapping → (syntax-parser - [(→ (~and Xs {X:id ...}) . rst) + [(_ (~and Xs {X:id ...}) . rst) #:when (brace? #'Xs) (add-orig #'(∀ (X ...) (ext-stlc:→ . rst)) (get-orig this-syntax))] - [(→ . rst) (add-orig #'(∀ () (ext-stlc:→ . rst)) (get-orig this-syntax))])) + [(_ . rst) (add-orig #'(∀ () (ext-stlc:→ . rst)) (get-orig this-syntax))])) (begin-for-syntax ;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id) @@ -61,22 +62,23 @@ (list cs (reverse (stx->list e+τs)))))) (define-typed-syntax define - [(define x:id e) + [(_ x:id e) #:with (e- τ) (infer+erase #'e) #:with y (generate-temporary) #'(begin- (define-syntax x (make-rename-transformer (⊢ y : τ))) (define- y e-))] - [(define (~and Xs {X:id ...}) (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e) + [(_ (~and Xs {X:id ...}) (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e) #:when (brace? #'Xs) #:with g (generate-temporary #'f) #:with e_ann #'(add-expected e τ_out) #'(begin- - (define-syntax f (make-rename-transformer - (⊢ g : #,(add-orig #'(∀ (X ...) (ext-stlc:→ τ ... τ_out)) - #'(→ τ ... τ_out))))) + (define-syntax f + (make-rename-transformer + (⊢ g : #,(add-orig #'(∀ (X ...) (ext-stlc:→ τ ... τ_out)) + #'(→ τ ... τ_out))))) (define- g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))] - [(define (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e) + [(_ (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e) #:with g (generate-temporary #'f) #:with e_ann #'(add-expected e τ_out) #'(begin- @@ -85,11 +87,12 @@ ; all λs have type (∀ (X ...) (→ τ_in ... τ_out)) (define-typed-syntax λ #:datum-literals (:) - [(λ (x:id ...) e) ; no annotations, try to infer from outer ctx, ie an application + [(_ (x:id ...) e) ; no annotations, try to infer from outer ctx, ie an app #:with given-τ-args (syntax-property stx 'given-τ-args) - #:fail-unless (syntax-e #'given-τ-args) ; no inferred types or annotations, so error - (format "input types for ~a could not be inferred; add annotations" - (syntax->datum stx)) + #:fail-unless (syntax-e #'given-τ-args) ; cant infer type and no annotations + (format + "input types for ~a could not be inferred; add annotations" + (syntax->datum stx)) #:with (τ_arg ...) #'given-τ-args #:with [fn- τ_fn] (infer+erase #'(ext-stlc:λ ([x : τ_arg] ...) e)) (⊢ fn- : #,(add-orig #'(∀ () τ_fn) (get-orig #'τ_fn)))] @@ -97,23 +100,25 @@ #:with (xs- e- τ_res) (infer/ctx+erase #'([x : x] ...) #'e) #:with env (get-env #'e-) #:fail-unless (syntax-e #'env) - (format "input types for ~a could not be inferred; add annotations" - (syntax->datum stx)) + (format + "input types for ~a could not be inferred; add annotations" + (syntax->datum stx)) #:with (τ_arg ...) (stx-map (λ (y) (lookup y #'env)) #'xs-) #:fail-unless (stx-andmap syntax-e #'(τ_arg ...)) - (format "some input types for ~a could not be inferred; add annotations" - (syntax->datum stx)) + (format + "some input types for ~a could not be inferred; add annotations" + (syntax->datum stx)) ;; propagate up inferred types of variables #:with res (add-env #'(λ- xs- e-) #'env) ; #:with [fn- τ_fn] (infer+erase #'(ext-stlc:λ ([x : x] ...) e)) (⊢ res : #,(add-orig #'(∀ () (ext-stlc:→ τ_arg ... τ_res)) #`(→ #,@(stx-map get-orig #'(τ_arg ... τ_res)))))] ;(⊢ (λ- xs- e-) : (∀ () (ext-stlc:→ τ_arg ... τ_res)))] - [(λ . rst) + [(_ . rst) #:with [fn- τ_fn] (infer+erase #'(ext-stlc:λ . rst)) (⊢ fn- : #,(add-orig #'(∀ () τ_fn) (get-orig #'τ_fn)))]) -(define-typed-syntax infer:#%app #:export-as #%app +(define-typed-syntax #%app [(_ e_fn e_arg ...) ; infer args first ; #:when (printf "args first ~a\n" (syntax->datum stx)) #:with maybe-inferred-τs (with-handlers ([exn:fail:type:infer? (λ _ #f)]) diff --git a/macrotypes/examples/mlish+adhoc.rkt b/macrotypes/examples/mlish+adhoc.rkt index 4c27507..bee734d 100644 --- a/macrotypes/examples/mlish+adhoc.rkt +++ b/macrotypes/examples/mlish+adhoc.rkt @@ -1,9 +1,13 @@ #lang s-exp "../typecheck.rkt" +(require (only-in "../typecheck.rkt" + [define-typed-syntax def-typed-stx/no-provide])) (require racket/fixnum racket/flonum) -(extends "ext-stlc.rkt" #:except #%app λ → + - * void = zero? sub1 add1 not let let* and #%datum begin +(extends + "ext-stlc.rkt" + #:except → define begin #%app λ #%datum + + - * void = zero? sub1 add1 not let let* and #:rename [~→ ~ext-stlc:→]) -;(reuse [inst sysf:inst] #:from "sysf.rkt") (require (rename-in (only-in "sysf.rkt" inst) [inst sysf:inst])) (provide inst) (require (only-in "ext-stlc.rkt" →?)) @@ -14,7 +18,6 @@ (reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt") (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil))) (require (only-in "stlc+cons.rkt" ~List List? List)) -(provide List) (reuse ref deref := Ref #:from "stlc+box.rkt") (require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×) [tup rec] [proj get] [× ××])) @@ -23,10 +26,6 @@ (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list))) (require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup))) -(provide → →/test =>/test match2 define-type) - -(provide define-typeclass define-instance) - ;; ML-like language + ad-hoc polymorphism ;; - top level recursive functions ;; - user-definable algebraic datatypes @@ -35,8 +34,23 @@ ;; ;; - type classes +(provide → →/test => =>/test + List Channel Thread Vector Sequence Hash String-Port Input-Port Regexp + define-type define-typeclass define-instance + match2) + (define-type-constructor => #:arity > 0) +;; providing version of define-typed-syntax +(define-syntax (define-typed-syntax stx) + (syntax-parse stx + [(_ name:id #:export-as out-name:id . rst) + #'(begin- + (provide- (rename-out [name out-name])) + (def-typed-stx/no-provide name . rst))] + [(_ name:id . rst) + #'(define-typed-syntax name #:export-as name . rst)])) + ;; type class helper fns (begin-for-syntax (define (mk-app-err-msg stx #:expected [expected-τs #'()] @@ -397,8 +411,7 @@ [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)])) (define-type-constructor Name #:arity = #,(stx-length #'(X ...)) - #:extra-info 'NameExtraInfo - #:no-provide) + #:extra-info 'NameExtraInfo) (struct- StructName (fld ...) #:reflection-name 'Cons #:transparent) ... (define-syntax- (exposed-acc stx) ; accessor for records (syntax-parse stx diff --git a/macrotypes/examples/mlish.rkt b/macrotypes/examples/mlish.rkt index d88f3ec..b3cc585 100644 --- a/macrotypes/examples/mlish.rkt +++ b/macrotypes/examples/mlish.rkt @@ -1,9 +1,13 @@ #lang s-exp macrotypes/typecheck -(require racket/fixnum racket/flonum - (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) +(require + racket/fixnum racket/flonum + (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) -(extends "ext-stlc.rkt" #:except #%app λ → + - * void = zero? sub1 add1 not let let* and #%datum begin - #:rename [~→ ~ext-stlc:→]) +(extends + "ext-stlc.rkt" + #:except → define #%app λ #%datum begin + + - * void = zero? sub1 add1 not let let* and + #:rename [~→ ~ext-stlc:→]) (reuse inst #:from "sysf.rkt") (require (only-in "ext-stlc.rkt" → →?)) (require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ)) @@ -13,7 +17,6 @@ (reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt") (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil))) (require (only-in "stlc+cons.rkt" ~List List? List)) -(provide List) (reuse ref deref := Ref #:from "stlc+box.rkt") (require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×) [tup rec] [proj get] [× ××])) @@ -31,7 +34,8 @@ (module+ test (require (for-syntax rackunit))) -(provide → →/test match2 define-type +(provide define-type + → →/test ; redefine these to use lifted → (typed-out [+ : (→ Int Int Int)] [- : (→ Int Int Int)] @@ -50,7 +54,30 @@ [not : (→ Bool Bool)] [abs : (→ Int Int)] [even? : (→ Int Bool)] - [odd? : (→ Int Bool)])) + [odd? : (→ Int Bool)]) + define match match2 λ + (rename-out [mlish:#%app #%app]) + cond when unless + Channel make-channel channel-get channel-put + Thread thread + List Vector + vector make-vector vector-length vector-ref vector-set! vector-copy! + Sequence in-range in-naturals in-vector in-list in-lines + for for* + for/list for/vector for*/vector for*/list for/fold for/hash for/sum + printf format display displayln list->vector + let let* begin + Hash in-hash hash hash-set! hash-ref hash-has-key? hash-count + String-Port Input-Port + write-string string-length string-copy! + quotient+remainder + set! + provide-type + (rename-out [mlish-provide provide]) + require-typed + Regexp + equal? + read) ;; creating possibly polymorphic types ;; ?∀ only wraps a type in a forall if there's at least one type variable @@ -332,14 +359,14 @@ ;; which is not known to programmers, to make the result slightly more ;; intuitive, we arbitrarily sort the inferred tyvars lexicographically (define-typed-syntax define - [(define x:id e) + [(_ x:id e) #:with (e- τ) (infer+erase #'e) #:with y (generate-temporary) #'(begin- (define-syntax x (make-rename-transformer (⊢ y : τ))) (define- y e-))] ; explicit "forall" - [(define Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) + [(_ Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) e_body ... e) #:when (brace? #'Ys) ;; TODO; remove this code duplication @@ -356,9 +383,9 @@ (define- g (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))] ;; alternate type sig syntax, after parameter names - [(define (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b) + [(_ (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b) #'(define (f [x : ty] ... -> ty_out) . b)] - [(define (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) + [(_ (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) e_body ... e) #:with Ys (compute-tyvars #'(τ ... τ_out)) #:with g (add-orig (generate-temporary #'f) #'f) @@ -455,8 +482,7 @@ #:arg-variances (make-arg-variances-proc arg-variance-vars (list #'X ...) (list #'τ ... ...)) - #:extra-info 'NameExtraInfo - #:no-provide) + #:extra-info 'NameExtraInfo) (struct- StructName (fld ...) #:reflection-name 'Cons #:transparent) ... (define-syntax (exposed-acc stx) ; accessor for records (syntax-parse stx @@ -700,7 +726,7 @@ (define-syntax (match2 stx) (syntax-parse stx #:datum-literals (with) - [(match2 e with . clauses) + [(_ e with . clauses) #:fail-when (null? (syntax->list #'clauses)) "no clauses" #:with [e- τ_e] (infer+erase #'e) (syntax-parse #'clauses #:datum-literals (->) @@ -719,7 +745,7 @@ ])])) (define-typed-syntax match #:datum-literals (with) - [(match e with . clauses) + [(_ e with . clauses) #:fail-when (null? (syntax->list #'clauses)) "no clauses" #:with [e- τ_e] (infer+erase #'e) #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type @@ -832,7 +858,7 @@ ; all λs have type (?∀ (X ...) (→ τ_in ... τ_out)) (define-typed-syntax λ - [(λ (x:id ...) body) + [(_ (x:id ...) body) #:with (~?∀ Xs expected) (get-expected-type stx) #:fail-unless (→? #'expected) (no-expected-type-fail-msg) @@ -841,17 +867,17 @@ (format "expected a function of ~a arguments, got one with ~a arguments" (stx-length #'[arg-ty ...]) (stx-length #'[x ...])) #`(?Λ Xs (ext-stlc:λ ([x : arg-ty] ...) (add-expected body body-ty)))] - [(λ (~and args ([_ (~datum :) ty] ...)) body) + [(_ (~and args ([_ (~datum :) ty] ...)) body) #:with (~?∀ () (~ext-stlc:→ arg-ty ... body-ty)) (get-expected-type stx) #`(?Λ () (ext-stlc:λ args (add-expected body body-ty)))] - [(λ (~and x+tys ([_ (~datum :) ty] ...)) . body) + [(_ (~and x+tys ([_ (~datum :) ty] ...)) . body) #:with Xs (compute-tyvars #'(ty ...)) ;; TODO is there a way to have λs that refer to ids defined after them? #'(?Λ Xs (ext-stlc:λ x+tys . body))]) ;; #%app -------------------------------------------------- -(define-typed-syntax mlish:#%app #:export-as #%app +(define-typed-syntax mlish:#%app [(_ e_fn . e_args) ;; compute fn type (ie ∀ and →) #:with [e_fn- (~?∀ Xs (~ext-stlc:→ . tyX_args))] (infer+erase #'e_fn) @@ -883,7 +909,7 @@ ;; cond and other conditionals (define-typed-syntax cond - [(cond [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t))) + [(_ [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t))) test) b ... body] ...+) #:with (test- ...) (⇑s (test ...) as Bool) @@ -892,13 +918,13 @@ #:with (([b- ty_b] ...) ...) (stx-map infers+erase #'((b ...) ...)) (⊢ (cond- [test- b- ... body-] ...) : (⊔ ty_body ...))]) (define-typed-syntax when - [(when test body ...) + [(_ test body ...) ; #:with test- (⇑ test as Bool) #:with [test- _] (infer+erase #'test) #:with [(body- _) ...] (infers+erase #'(body ...)) (⊢ (when- test- body- ... (void-)) : Unit)]) (define-typed-syntax unless - [(unless test body ...) + [(_ test body ...) ; #:with test- (⇑ test as Bool) #:with [test- _] (infer+erase #'test) #:with [(body- _) ...] (infers+erase #'(body ...)) @@ -908,15 +934,15 @@ (define-type-constructor Channel) (define-typed-syntax make-channel - [(make-channel (~and tys {ty})) + [(_ (~and tys {ty})) #:when (brace? #'tys) (⊢ (make-channel-) : (Channel ty))]) (define-typed-syntax channel-get - [(channel-get c) + [(_ c) #:with [c- (~Channel ty)] (infer+erase #'c) (⊢ (channel-get- c-) : ty)]) (define-typed-syntax channel-put - [(channel-put c v) + [(_ c v) #:with [c- (~Channel ty)] (infer+erase #'c) #:with [v- ty_v] (infer+erase #'v) #:fail-unless (typechecks? #'ty_v #'ty) @@ -927,7 +953,7 @@ ;; threads (define-typed-syntax thread - [(thread th) + [(_ th) #:with (th- (~?∀ () (~ext-stlc:→ τ_out))) (infer+erase #'th) (⊢ (thread- th-) : Thread)]) @@ -937,18 +963,19 @@ [string->number : (→ String Int)])) (define-typed-syntax number->string [f:id (assign-type #'number->string- #'(→ Int String))] - [(number->string n) + [(_ n) #'(number->string n (ext-stlc:#%datum . 10))] - [(number->string n rad) + [(_ n rad) #:with args- (⇑s (n rad) as Int) (⊢ (number->string- . args-) : String)]) -(provide (typed-out [string : (→ Char String)] +(provide number->string string-append + (typed-out [string : (→ Char String)] [sleep : (→ Int Unit)] [string=? : (→ String String Bool)] [string<=? : (→ String String Bool)])) (define-typed-syntax string-append - [(string-append . strs) + [(_ . strs) #:with strs- (⇑s strs as String) (⊢ (string-append- . strs-) : String)]) @@ -956,44 +983,45 @@ (define-type-constructor Vector) (define-typed-syntax vector - [(vector (~and tys {ty})) + [(_ (~and tys {ty})) #:when (brace? #'tys) (⊢ (vector-) : (Vector ty))] - [(vector v ...) + [(_ v ...) #:with ([v- ty] ...) (infers+erase #'(v ...)) #:when (same-types? #'(ty ...)) #:with one-ty (stx-car #'(ty ...)) (⊢ (vector- v- ...) : (Vector one-ty))]) (define-typed-syntax make-vector - [(make-vector n) #'(make-vector n (ext-stlc:#%datum . 0))] - [(make-vector n e) + [(_ n) #'(make-vector n (ext-stlc:#%datum . 0))] + [(_ n e) #:with n- (⇑ n as Int) #:with [e- ty] (infer+erase #'e) (⊢ (make-vector- n- e-) : (Vector ty))]) (define-typed-syntax vector-length - [(vector-length e) + [(_ e) #:with [e- _] (⇑ e as Vector) (⊢ (vector-length- e-) : Int)]) (define-typed-syntax vector-ref - [(vector-ref e n) + [(_ e n) #:with n- (⇑ n as Int) #:with [e- (ty)] (⇑ e as Vector) (⊢ (vector-ref- e- n-) : ty)]) (define-typed-syntax vector-set! - [(vector-set! e n v) + [(_ e n v) #:with n- (⇑ n as Int) #:with [e- (~Vector ty)] (infer+erase #'e) #:with [v- ty_v] (infer+erase #'v) #:fail-unless (typecheck? #'ty_v #'ty) - (typecheck-fail-msg/1 #'ty #'ty_v #'v) + (typecheck-fail-msg/1 #'ty #'ty_v #'v) (⊢ (vector-set!- e- n- v-) : Unit)]) (define-typed-syntax vector-copy! - [(vector-copy! dest start src) + [(_ dest start src) #:with start- (⇑ start as Int) #:with [dest- (~Vector ty_dest)] (infer+erase #'dest) #:with [src- (~Vector ty_src)] (infer+erase #'src) #:fail-unless (typecheck? #'ty_dest #'ty_src) - (typecheck-fail-msg/1 #'(Vector ty_src) #'(Vector ty_dest) #'dest) + (typecheck-fail-msg/1 + #'(Vector ty_src) #'(Vector ty_dest) #'dest) (⊢ (vector-copy!- dest- start- src-) : Unit)]) @@ -1002,11 +1030,11 @@ (define-type-constructor Sequence) (define-typed-syntax in-range - [(in-range end) + [(_ end) #'(in-range (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))] - [(in-range start end) + [(_ start end) #'(in-range start end (ext-stlc:#%datum . 1))] - [(in-range start end step) + [(_ start end step) #:with (e- ...) (⇑s (start end step) as Int) (⊢ (in-range- e- ...) : (Sequence Int))]) @@ -1268,7 +1296,7 @@ (define-typed-syntax provide-type [(provide-type ty ...) #'(provide- ty ...)]) -(define-typed-syntax mlish-provide #:export-as provide +(define-typed-syntax mlish-provide [(provide x:id ...) #:with ([x- ty_x] ...) (infers+erase #'(x ...)) ; TODO: use hash-code to generate this tmp diff --git a/macrotypes/examples/stlc+box.rkt b/macrotypes/examples/stlc+box.rkt index 06a347d..e1d2503 100644 --- a/macrotypes/examples/stlc+box.rkt +++ b/macrotypes/examples/stlc+box.rkt @@ -9,20 +9,22 @@ ;; - terms from stlc+cons.rkt ;; - ref deref := +(provide Ref ref deref :=) + (define-type-constructor Ref) (define-typed-syntax ref - [(ref e) + [(_ e) #:with [e- τ] (infer+erase #'e) (⊢ (box- e-) : (Ref τ))]) (define-typed-syntax deref - [(deref e) + [(_ e) #:with [e- (~Ref τ)] (infer+erase #'e) (⊢ (unbox- e-) : τ)]) (define-typed-syntax := #:literals (:=) - [(:= e_ref e) + [(_ e_ref e) #:with [e_ref- (~Ref τ1)] (infer+erase #'e_ref) #:with [e- τ2] (infer+erase #'e) #:fail-unless (typecheck? #'τ1 #'τ2) - (typecheck-fail-msg/1 #'τ1 #'τ2 #'e) + (typecheck-fail-msg/1 #'τ1 #'τ2 #'e) (⊢ (set-box!- e_ref- e-) : Unit)]) diff --git a/macrotypes/examples/stlc+cons.rkt b/macrotypes/examples/stlc+cons.rkt index 9f6b030..674bcef 100644 --- a/macrotypes/examples/stlc+cons.rkt +++ b/macrotypes/examples/stlc+cons.rkt @@ -10,52 +10,62 @@ ;; TODO: enable HO use of list primitives +(provide (type-out List) + nil isnil cons list head tail + reverse length list-ref member) + (define-type-constructor List) (define-typed-syntax nil - [(nil ~! τi:type-ann) + [(_ ~! τi:type-ann) (⊢ null- : (List τi.norm))] ; minimal type inference - [nil:id #:with expected-τ (get-expected-type #'nil) - #:fail-unless (syntax-e #'expected-τ) ; 'expected-type property exists (ie, not false) - (raise (exn:fail:type:infer - (format "~a (~a:~a): nil: ~a" - (syntax-source stx) (syntax-line stx) (syntax-column stx) - (no-expected-type-fail-msg)) - (current-continuation-marks))) - #:fail-unless (List? #'expected-τ) - (raise (exn:fail:type:infer - (format "~a (~a:~a): Inferred ~a type for nil, which is not a List." - (syntax-source stx) (syntax-line stx) (syntax-column stx) - (type->str #'ty_lst)) - (current-continuation-marks))) - (⊢ null- : expected-τ)]) + [nil:id + #:with expected-τ (get-expected-type #'nil) + ; 'expected-type property exists (ie, not false) + #:fail-unless (syntax-e #'expected-τ) + (raise + (exn:fail:type:infer + (format + "~a (~a:~a): nil: ~a" + (syntax-source stx) (syntax-line stx) (syntax-column stx) + (no-expected-type-fail-msg)) + (current-continuation-marks))) + #:fail-unless (List? #'expected-τ) + (raise + (exn:fail:type:infer + (format + "~a (~a:~a): Inferred ~a type for nil, which is not a List." + (syntax-source stx) (syntax-line stx) (syntax-column stx) + (type->str #'ty_lst)) + (current-continuation-marks))) + (⊢ null- : expected-τ)]) (define-typed-syntax cons - [(cons e1 e2) + [(_ e1 e2) #:with [e1- τ_e1] (infer+erase #'e1) #:with τ_list ((current-type-eval) #'(List τ_e1)) #:with [e2- τ_e2] (infer+erase (add-expected-ty #'e2 #'τ_list)) #:fail-unless (typecheck? #'τ_e2 #'τ_list) - (typecheck-fail-msg/1 #'τ_list #'τ_e2 #'e2) + (typecheck-fail-msg/1 #'τ_list #'τ_e2 #'e2) ;; propagate up inferred types of variables #:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e1- e2-)))) #:with result-cons (add-env #'(cons- e1- e2-) #'env) (⊢ result-cons : τ_list)]) (define-typed-syntax isnil - [(isnil e) + [(_ e) #:with [e- (~List _)] (infer+erase #'e) (⊢ (null?- e-) : Bool)]) (define-typed-syntax head - [(head e) + [(_ e) #:with [e- (~List τ)] (infer+erase #'e) (⊢ (car- e-) : τ)]) (define-typed-syntax tail - [(tail e) + [(_ e) #:with [e- τ_lst] (infer+erase #'e) #:when (List? #'τ_lst) (⊢ (cdr- e-) : τ_lst)]) (define-typed-syntax list - [(list) #'nil] + [(_) #'nil] [(_ x . rst) ; has expected type #:with expected-τ (get-expected-type stx) #:when (syntax-e #'expected-τ) @@ -64,22 +74,22 @@ [(_ x . rst) ; no expected type #'(cons x (list . rst))]) (define-typed-syntax reverse - [(reverse e) + [(_ e) #:with (e- τ-lst) (infer+erase #'e) #:when (List? #'τ-lst) (⊢ (reverse- e-) : τ-lst)]) (define-typed-syntax length - [(length e) + [(_ e) #:with (e- τ-lst) (infer+erase #'e) #:when (List? #'τ-lst) (⊢ (length- e-) : Int)]) (define-typed-syntax list-ref - [(list-ref e n) + [(_ e n) #:with (e- (ty)) (⇑ e as List) #:with n- (⇑ n as Int) (⊢ (list-ref- e- n-) : ty)]) (define-typed-syntax member - [(member v e) + [(_ v e) #:with (e- (ty)) (⇑ e as List) #:with [v- ty_v] (infer+erase #'(add-expected v ty)) #:when (typecheck? #'ty_v #'ty) diff --git a/macrotypes/examples/stlc+effect.rkt b/macrotypes/examples/stlc+effect.rkt index c6a452e..962e3f8 100644 --- a/macrotypes/examples/stlc+effect.rkt +++ b/macrotypes/examples/stlc+effect.rkt @@ -1,7 +1,5 @@ #lang s-exp macrotypes/typecheck -(extends "stlc+box.rkt" #:except ref Ref ~Ref ~Ref* Ref? deref := #%app λ) - -(provide (for-syntax get-new-effects)) +(extends "stlc+box.rkt" #:except Ref ref deref := #%app λ) ;; Simply-Typed Lambda Calculus, plus mutable references ;; Types: @@ -11,6 +9,10 @@ ;; - terms from stlc+cons.rkt ;; - ref deref := +(provide (for-syntax get-new-effects) + Ref + #%app λ ref deref :=) + (begin-for-syntax (define (add-news e locs) (syntax-property e 'ν locs)) (define (add-assigns e locs) (syntax-property e ':= locs)) @@ -24,7 +26,8 @@ (define (get-effects e tag [vs '()]) (or (syntax-property - (local-expand (if (null? vs) e #`(stlc+box:λ #,vs #,e)) 'expression null) + (local-expand + (if (null? vs) e #`(stlc+box:λ #,vs #,e)) 'expression null) tag) null)) (define (get-new-effects e [vs '()]) (get-effects e 'ν vs)) @@ -45,7 +48,7 @@ [else (set-union locs1 locs2)]))) -(define-typed-syntax effect:#%app #:export-as #%app +(define-typed-syntax #%app [(_ efn e ...) #:with [e_fn- ty_fn fns fas fds] (infer+erase/eff #'efn) #:with tyns (get-new-effects #'ty_fn) @@ -54,36 +57,20 @@ #:with (~→ τ_in ... τ_out) #'ty_fn #:with ([e_arg- τ_arg ns as ds] ...) (infers+erase/eff #'(e ...)) #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...)) - (num-args-fail-msg #'efn #'(τ_in ...) #'(e ...)) + (num-args-fail-msg #'efn #'(τ_in ...) #'(e ...)) #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) - (typecheck-fail-msg/multi #'(τ_in ...) #'(τ_arg ...) #'(e ...)) - (assign-type/eff #'(#%app- e_fn- e_arg- ...) #'τ_out - (stx-flatten #'(fns tyns . (ns ...))) - (stx-flatten #'(fas tyas . (as ...))) - (stx-flatten #'(fds tyds . (ds ...)))) - #;(let ([φ-news (stx-map get-new-effects #'(τfn efn e ...))] - [φ-assigns (stx-map get-assign-effects #'(τfn efn e ...))] - [φ-derefs (stx-map get-deref-effects #'(τfn efn e ...))]) - (add-effects #'(stlc+box:#%app efn e ...) - (foldl loc-union (set) φ-news) - (foldl loc-union (set) φ-assigns) - (foldl loc-union (set) φ-derefs)))]) + (typecheck-fail-msg/multi + #'(τ_in ...) #'(τ_arg ...) #'(e ...)) + (assign-type/eff #'(#%app- e_fn- e_arg- ...) #'τ_out + (stx-flatten #'(fns tyns . (ns ...))) + (stx-flatten #'(fas tyas . (as ...))) + (stx-flatten #'(fds tyds . (ds ...))))]) (define-typed-syntax λ - [(λ bvs:type-ctx e) + [(_ bvs:type-ctx e) #:with [xs- e- τ_res ns as ds] (infer/ctx+erase/eff #'bvs #'e) (assign-type #'(λ- xs- e-) - (add-effects #'(→ bvs.type ... τ_res) #'ns #'as #'ds))]) - -#;(define-typed-syntax λ - [(λ bvs:type-ctx e) - #:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e) - (let ([φ-news (get-new-effects #'e-)] - [φ-assigns (get-assign-effects #'e-)] - [φ-derefs (get-deref-effects #'e-)]) - (assign-type - #'(λ- xs- e-) - (add-effects #'(→ bvs.type ... τ_res) φ-news φ-assigns φ-derefs)))]) + (add-effects #'(→ bvs.type ... τ_res) #'ns #'as #'ds))]) (define-type-constructor Ref) @@ -92,43 +79,37 @@ (define/with-syntax [e- ty] (infer+erase e)) (list #'e- #'ty - (get-new-effects #'e-) (get-assign-effects #'e-) (get-deref-effects #'e-))) + (get-new-effects #'e-) + (get-assign-effects #'e-) + (get-deref-effects #'e-))) (define (infers+erase/eff es) (stx-map infer+erase/eff es)) (define (infer/ctx+erase/eff bvs e) (define/with-syntax [xs- e- ty] (infer/ctx+erase bvs e)) (list #'xs- #'e- #'ty - (get-new-effects #'e-) (get-assign-effects #'e-) (get-deref-effects #'e-))) + (get-new-effects #'e-) + (get-assign-effects #'e-) + (get-deref-effects #'e-))) (define (assign-type/eff e ty news assigns derefs) (assign-type (add-effects e news assigns derefs) ty))) (define-typed-syntax ref - [(ref e) + [(_ e) #:with [e- τ ns as ds] (infer+erase/eff #'e) - (assign-type/eff #'(box- e-) #'(Ref τ) + (assign-type/eff #'(#%app- box- e-) #'(Ref τ) (cons (syntax-position stx) #'ns) #'as #'ds)]) (define-typed-syntax deref - [(deref e) + [(_ e) #:with [e- (~Ref ty) ns as ds] (infer+erase/eff #'e) - (assign-type/eff #'(unbox- e-) #'ty + (assign-type/eff #'(#%app- unbox- e-) #'ty #'ns #'as (cons (syntax-position stx) #'ds))]) (define-typed-syntax := #:literals (:=) - [(:= e_ref e) + [(_ e_ref e) #:with [e_ref- (~Ref ty1) ns1 as1 ds1] (infer+erase/eff #'e_ref) #:with [e- ty2 ns2 as2 ds2] (infer+erase/eff #'e) #:fail-unless (typecheck? #'ty1 #'ty2) - (typecheck-fail-msg/1 #'ty1 #'ty2 #'e) - (assign-type/eff #'(set-box!- e_ref- e-) #'Unit + (typecheck-fail-msg/1 #'ty1 #'ty2 #'e) + (assign-type/eff #'(#%app- set-box!- e_ref- e-) #'Unit (stx-append #'ns1 #'ns2) (cons (syntax-position stx) (stx-append #'as1 #'as2)) (stx-append #'ds1 #'ds2))]) -;(define-typed-syntax ref -; [(_ e) -; (syntax-property #'(stlc+box:ref e) 'ν (set (syntax-position stx)))]) -;(define-typed-syntax deref -; [(_ e) -; (syntax-property #'(stlc+box:deref e) '! (set (syntax-position stx)))]) -;(define-typed-syntax := -; [(_ e_ref e) -; (syntax-property #'(stlc+box::= e_ref e) ':= (set (syntax-position stx)))]) - diff --git a/macrotypes/examples/stlc+lit.rkt b/macrotypes/examples/stlc+lit.rkt index ba7fe66..bc1a33c 100644 --- a/macrotypes/examples/stlc+lit.rkt +++ b/macrotypes/examples/stlc+lit.rkt @@ -10,12 +10,14 @@ ;; - numeric literals ;; - prim + -(provide (typed-out [+ : (→ Int Int Int)])) +(provide (type-out Int) + (typed-out [+ : (→ Int Int Int)]) + #%datum) (define-base-type Int) -(define-typed-syntax #%datum #:literals (#%datum) - [(#%datum . n:integer) (⊢ #,(syntax/loc stx (#%datum- . n)) : Int)] - [(#%datum . x) +(define-typed-syntax #%datum + [(_ . n:integer) (⊢ #,(syntax/loc stx (#%datum- . n)) : Int)] + [(_ . x) #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x) #'(#%datum- . x)]) diff --git a/macrotypes/examples/stlc+occurrence.rkt b/macrotypes/examples/stlc+occurrence.rkt index 221129f..298262c 100644 --- a/macrotypes/examples/stlc+occurrence.rkt +++ b/macrotypes/examples/stlc+occurrence.rkt @@ -21,14 +21,16 @@ ;; ============================================================================= +(provide Bot Boolean Str ∪ #%datum test) + (define-base-type Bot) ;; For empty unions (define-base-type Boolean) (define-base-type Str) (define-typed-syntax #%datum - [(#%datum . n:boolean) (⊢ (#%datum- . n) : Boolean)] - [(#%datum . n:str) (⊢ (#%datum- . n) : Str)] - [(#%datum . x) #'(stlc+sub:#%datum . x)]) + [(_ . n:boolean) (⊢ (#%datum- . n) : Boolean)] + [(_ . n:str) (⊢ (#%datum- . n) : Str)] + [(_ . x) #'(stlc+sub:#%datum . x)]) (define-type-constructor ∪ #:arity >= 1) @@ -231,7 +233,7 @@ ;; - allow x not identifier (1. does nothing 2. latent filters) (define-typed-syntax test #:datum-literals (?) ;; -- THIS CASE BELONGS IN A NEW FILE - [(test [τ0+:type ? (unop x-stx:id n-stx:nat)] e1 e2) + [(_ [τ0+:type ? (unop x-stx:id n-stx:nat)] e1 e2) ;; 1. Check that we're using a known eliminator #:when (free-identifier=? #'stlc+tup:proj #'unop) ;; 2. Make sure we're filtering with a valid type @@ -256,7 +258,7 @@ ;; TODO lists ;; For now, we can't express the type (List* A (U A B)), so our filters are too strong ;; -- THE ORIGINAL - [(test [τ0+:type ? x-stx:id] e1 e2) + [(_ [τ0+:type ? x-stx:id] e1 e2) #:with f (type->filter #'τ0+) #:with (x τ0) (infer+erase #'x-stx) #:with τ0- (∖ #'τ0 #'τ0+) diff --git a/macrotypes/examples/stlc+overloading.rkt b/macrotypes/examples/stlc+overloading.rkt index 3b2c9e4..3b6125e 100644 --- a/macrotypes/examples/stlc+overloading.rkt +++ b/macrotypes/examples/stlc+overloading.rkt @@ -1,18 +1,18 @@ #lang s-exp macrotypes/typecheck (reuse List cons nil #:from "stlc+cons.rkt") -(reuse #:from "stlc+rec-iso.rkt") ; to load current-type=? (extends "stlc+sub.rkt" #:except #%datum) ;; Revision of overloading, using identifier macros instead of overriding #%app ;; ============================================================================= -(define-base-type Bot) -(define-base-type Str) +(provide Bot Str #%datum signature resolve instance) + +(define-base-types Bot Str) (define-typed-syntax #%datum - [(#%datum . n:str) (⊢ (#%datum- . n) : Str)] - [(#%datum . x) #'(stlc+sub:#%datum . x)]) + [(_ . n:str) (⊢ (#%datum- . n) : Str)] + [(_ . x) #'(stlc+sub:#%datum . x)]) (define-for-syntax xerox syntax->datum) @@ -105,7 +105,7 @@ ;; === Overloaded signature environment (define-typed-syntax signature - [(signature (name:id α:id) τ) + [(_ (name:id α:id) τ) #:with ((α+) (~→ τ_α:id τ-cod) _) (infer/tyctx+erase #'([α : #%type]) #'τ) (define ℜ (ℜ-init #'name #'τ-cod)) (⊢ (define-syntax name @@ -120,11 +120,11 @@ [(_ e* (... ...)) #'(raise-arity-error- (syntax->datum- name) 1 e* (... ...))])) : Bot)] - [(signature e* ...) + [(_ e* ...) (error 'signature (format "Expected (signature (NAME VAR) (→ VAR τ)), got ~a" (xerox #'(e* ...))))]) (define-typed-syntax resolve - [(resolve name:id τ) + [(_ name:id τ) #:with τ+ ((current-type-eval) #'τ) ;; Extract a resolver from the syntax object (define ℜ (syntax->ℜ #'name)) @@ -132,7 +132,7 @@ (⊢ #,(ℜ #'τ+ #:exact? #t) : #,(ℜ->type ℜ #:subst #'τ+))]) (define-typed-syntax instance - [(instance (name:id τ-stx) e) + [(_ (name:id τ-stx) e) #:with τ ((current-type-eval) #'τ-stx) #:with [e+ τ+] (infer+erase #'e) (define ℜ (syntax->ℜ #'name)) diff --git a/macrotypes/examples/stlc+rec-iso.rkt b/macrotypes/examples/stlc+rec-iso.rkt index 7f28379..e4350de 100644 --- a/macrotypes/examples/stlc+rec-iso.rkt +++ b/macrotypes/examples/stlc+rec-iso.rkt @@ -1,6 +1,6 @@ #lang s-exp macrotypes/typecheck (extends "stlc+tup.rkt") -(reuse ∨ var case define-type-alias define #:from "stlc+reco+var.rkt") +(reuse ∨ var case #:from "stlc+reco+var.rkt") ;; stlc + (iso) recursive types ;; Types: @@ -12,16 +12,18 @@ ;; - also var and case from stlc+reco+var ;; - fld, unfld +(provide μ unfld fld) + (define-type-constructor μ #:bvs = 1) (define-typed-syntax unfld - [(unfld τ:type-ann e) + [(_ τ:type-ann e) #:with (~μ* (tv) τ_body) #'τ.norm #:with [e- τ_e] (infer+erase #'e) #:when (typecheck? #'τ_e #'τ.norm) (⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))]) (define-typed-syntax fld - [(fld τ:type-ann e) + [(_ τ:type-ann e) #:with (~μ* (tv) τ_body) #'τ.norm #:with [e- τ_e] (infer+erase #'e) #:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body)) diff --git a/macrotypes/examples/stlc+reco+sub.rkt b/macrotypes/examples/stlc+reco+sub.rkt index 9ef03a8..3aff3e7 100644 --- a/macrotypes/examples/stlc+reco+sub.rkt +++ b/macrotypes/examples/stlc+reco+sub.rkt @@ -11,9 +11,11 @@ ;; - terms from stlc+sub.rkt ;; - records and variants from stlc+reco+var +(provide #%datum) + (define-typed-syntax #%datum - [(#%datum . n:number) #'(stlc+sub:#%datum . n)] - [(#%datum . x) #'(stlc+reco+var:#%datum . x)]) + [(_ . n:number) #'(stlc+sub:#%datum . n)] + [(_ . x) #'(stlc+reco+var:#%datum . x)]) (begin-for-syntax (define old-sub? (current-sub?)) diff --git a/macrotypes/examples/stlc+reco+var.rkt b/macrotypes/examples/stlc+reco+var.rkt index e8876cc..c05212c 100644 --- a/macrotypes/examples/stlc+reco+var.rkt +++ b/macrotypes/examples/stlc+reco+var.rkt @@ -1,8 +1,6 @@ #lang s-exp macrotypes/typecheck -(extends "stlc+tup.rkt" #:except × ×? tup proj ~× ~×*) +(extends "stlc+tup.rkt" #:except × ×? tup proj ~×) (require (only-in "stlc+tup.rkt" [~× ~stlc:×])) -(provide × ∨ (for-syntax ~× ~×* ~∨ ~∨*)) - ;; Simply-Typed Lambda Calculus, plus records and variants ;; Types: @@ -13,29 +11,8 @@ ;; - terms from stlc+tup.rkt ;; - redefine tup to records ;; - sums (var) -;; TopLevel: -;; - define (values only) -;; - define-type-alias -(provide define-type-alias) -;; Using τ.norm leads to a "not valid type" error when file is compiled -(define-syntax define-type-alias - (syntax-parser - [(_ alias:id τ:type) - #'(define-syntax alias (make-variable-like-transformer #'τ))] - [(_ (f:id x:id ...) ty) - #'(define-syntax (f stx) - (syntax-parse stx - [(_ x ...) #'ty]))])) - -(define-typed-syntax define - [(define x:id e) - #:with (e- τ) (infer+erase #'e) - - #:with y (generate-temporary) - #'(begin- - (define-syntax x (make-rename-transformer (⊢ y : τ))) - (define- y e-))]) +(provide (type-out × ∨) tup proj var case) ; re-define tuples as records ; dont use define-type-constructor because I want the : literal syntax @@ -79,11 +56,11 @@ ;; records (define-typed-syntax tup #:datum-literals (=) - [(tup [l:id = e] ...) + [(_ [l:id = e] ...) #:with ([e- τ] ...) (infers+erase #'(e ...)) (⊢ (list- (list- 'l e-) ...) : (× [l : τ] ...))]) (define-typed-syntax proj #:literals (quote) - [(proj e_rec l:id) + [(_ e_rec l:id) #:with [e_rec- τ_e] (infer+erase #'e_rec) #:fail-unless (×? #'τ_e) (format "Expected expression ~s to have × type, got: ~a" @@ -135,27 +112,36 @@ (add-orig res (get-orig res))]))) (define-typed-syntax var #:datum-literals (as =) - [(var l:id = e as τ:type) + [(_ l:id = e as τ:type) #:fail-unless (∨? #'τ.norm) - (format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ.norm)) + (format + "Expected the expected type to be a ∨ type, got: ~a" + (type->str #'τ.norm)) #:with τ_match - (∨-ref #'τ.norm #'l #:else - (λ () (raise-syntax-error #f - (format "~a field does not exist" (syntax->datum #'l)) - stx))) + (∨-ref + #'τ.norm #'l #:else + (λ () + (raise-syntax-error #f + (format "~a field does not exist" (syntax->datum #'l)) + stx))) #:with [e- τ_e] (infer+erase #'e) #:fail-unless (typecheck? #'τ_e #'τ_match) - (typecheck-fail-msg/1 #'τ_match #'τ_e #'e) + (typecheck-fail-msg/1 #'τ_match #'τ_e #'e) (⊢ (list- 'l e) : τ.norm)]) (define-typed-syntax case #:datum-literals (of =>) - [(case e [l:id x:id => e_l] ...) + [(_ e [l:id x:id => e_l] ...) #:fail-when (null? (syntax->list #'(l ...))) "no clauses" #:with [e- (~∨* [l_x : τ_x] ...)] (infer+erase #'e) - #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses" - #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive" + #:fail-unless (= (stx-length #'(l ...)) + (stx-length #'(l_x ...))) + "wrong number of case clauses" + #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) + "case clauses not exhaustive" #:with (((x-) e_l- τ_el) ...) - (stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...)) + (stx-map + (λ (bs e) (infer/ctx+erase bs e)) + #'(([x : τ_x]) ...) #'(e_l ...)) (⊢ (let- ([l_e (car- e-)]) (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...)) : (⊔ τ_el ...))]) diff --git a/macrotypes/examples/stlc+sub.rkt b/macrotypes/examples/stlc+sub.rkt index e206b6e..cc46e70 100644 --- a/macrotypes/examples/stlc+sub.rkt +++ b/macrotypes/examples/stlc+sub.rkt @@ -3,7 +3,6 @@ (reuse Bool String add1 #:from "ext-stlc.rkt") (require (prefix-in ext: (only-in "ext-stlc.rkt" #%datum)) (only-in "ext-stlc.rkt" current-join)) -(provide (for-syntax subs? current-sub?)) ;; Simply-Typed Lambda Calculus, plus subtyping ;; Types: @@ -20,16 +19,19 @@ ;; - also * ;; Other: sub? current-sub? -(provide (typed-out [+ : (→ Num Num Num)] - [* : (→ Num Num Num)])) +(provide (for-syntax subs? current-sub?) + (type-out Top Num Nat) + (typed-out [+ : (→ Num Num Num)] + [* : (→ Num Num Num)]) + #%datum) (define-base-types Top Num Nat) (define-typed-syntax #%datum - [(#%datum . n:nat) (⊢ (#%datum- . n) : Nat)] - [(#%datum . n:integer) (⊢ (#%datum- . n) : Int)] - [(#%datum . n:number) (⊢ (#%datum- . n) : Num)] - [(#%datum . x) #'(ext:#%datum . x)]) + [(_ . n:nat) (⊢ (#%datum- . n) : Nat)] + [(_ . n:integer) (⊢ (#%datum- . n) : Int)] + [(_ . n:number) (⊢ (#%datum- . n) : Num)] + [(_ . x) #'(ext:#%datum . x)]) (begin-for-syntax (define (sub? t1 t2) @@ -49,8 +51,8 @@ (define-syntax (define-sub-relation stx) (syntax-parse stx #:datum-literals (<: =>) [(_ τ1:id <: τ2:id) - #:with τ1-expander (format-id #'τ1 "~~~a" #'τ1) - #:with τ2-expander (format-id #'τ2 "~~~a" #'τ2) + #:with τ1-expander (mk-~ #'τ1) + #:with τ2-expander (mk-~ #'τ2) #:with fn (generate-temporary) #:with old-sub? (generate-temporary) #'(begin diff --git a/macrotypes/examples/stlc+tup.rkt b/macrotypes/examples/stlc+tup.rkt index 57b05d1..65136c3 100644 --- a/macrotypes/examples/stlc+tup.rkt +++ b/macrotypes/examples/stlc+tup.rkt @@ -9,22 +9,25 @@ ;; - terms from ext-stlc.rkt ;; - tup and proj +(provide (type-out ×) tup proj) + (define-type-constructor × #:arity >= 0 #:arg-variances (λ (stx) (make-list (stx-length (stx-cdr stx)) covariant))) (define-typed-syntax tup - [(tup e ...) + [(_ e ...) #:with ty-expected (get-expected-type stx) - #:with (e_ann ...) (if (syntax-e #'ty-expected) - (syntax-parse (local-expand #'ty-expected 'expression null) - [(~× ty_exp ...) #'((add-expected e ty_exp) ...)] - [_ #'(e ...)]) - #'(e ...)) + #:with (e_ann ...) + (if (syntax-e #'ty-expected) + (syntax-parse (local-expand #'ty-expected 'expression null) + [(~× ty_exp ...) #'((add-expected e ty_exp) ...)] + [_ #'(e ...)]) + #'(e ...)) #:with ([e- τ] ...) (infers+erase #'(e_ann ...)) (⊢ (list- e- ...) : (× τ ...))]) (define-typed-syntax proj - [(proj e_tup n:nat) + [(_ e_tup n:nat) #:with [e_tup- (~× . τs_tup)] (infer+erase #'e_tup) #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large" (⊢ (list-ref- e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))]) diff --git a/macrotypes/examples/stlc.rkt b/macrotypes/examples/stlc.rkt index d2c310d..770a607 100644 --- a/macrotypes/examples/stlc.rkt +++ b/macrotypes/examples/stlc.rkt @@ -8,6 +8,8 @@ ;; - multi-arg λ (0+) ;; - multi-arg #%app (0+) +(provide (type-out →) λ #%app) + (define-type-constructor → #:arity >= 1 #:arg-variances (λ (stx) (syntax-parse stx @@ -17,12 +19,12 @@ (list covariant))]))) (define-typed-syntax λ - [(λ bvs:type-ctx e) + [(_ bvs:type-ctx e) #:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e) (⊢ (λ- xs- e-) : (→ bvs.type ... τ_res))]) -(define-typed-syntax #%app #:literals (#%app) - [(#%app e_fn e_arg ...) +(define-typed-syntax #%app + [(_ e_fn e_arg ...) #:with [e_fn- (~→ τ_in ... τ_out)] (infer+erase #'e_fn) #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...)) #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...)) diff --git a/macrotypes/examples/sysf.rkt b/macrotypes/examples/sysf.rkt index af9d17d..f1734e8 100644 --- a/macrotypes/examples/sysf.rkt +++ b/macrotypes/examples/sysf.rkt @@ -9,15 +9,17 @@ ;; - terms from stlc+lit.rkt ;; - Λ and inst +(provide (type-out ∀) Λ inst) + (define-type-constructor ∀ #:bvs >= 0) (define-typed-syntax Λ - [(Λ (tv:id ...) e) + [(_ (tv:id ...) e) #:with [(tv- ...) e- τ] (infer/tyctx+erase #'([tv : #%type] ...) #'e) (⊢ e- : (∀ (tv- ...) τ))]) (define-typed-syntax inst - [(inst e τ:type ...) + [(_ e τ:type ...) #:with [e- (~∀ tvs τ_body)] (infer+erase #'e) #:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body) (⊢ e- : τ_inst)] - [(inst e) #'e]) + [(_ e) #'e]) diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index fbff9bb..4c67dc2 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -9,7 +9,8 @@ syntax/parse racket/syntax syntax/stx racket/stxparam syntax/parse/define (only-in racket/provide-transform - make-provide-pre-transformer pre-expand-export) + make-provide-pre-transformer pre-expand-export + make-provide-transformer expand-export) "stx-utils.rkt") (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt") @@ -17,17 +18,18 @@ racket/bool racket/provide racket/require racket/match racket/promise syntax/parse/define) (provide - postfix-in - symbol=?- match- delay- + postfix-in symbol=?- match- delay- + (all-defined-out) + (for-syntax (all-defined-out)) + (for-meta 2 (all-defined-out)) (except-out (all-from-out racket/base) #%module-begin) (all-from-out syntax/parse/define) - (for-syntax (all-defined-out)) (all-defined-out) - (rename-out [define-syntax-category define-stx-category]) (for-syntax (all-from-out racket syntax/parse racket/syntax syntax/stx racket/provide-transform "stx-utils.rkt")) - (for-meta 2 (all-from-out racket/base syntax/parse racket/syntax))) + (for-meta 2 (all-from-out racket/base syntax/parse racket/syntax)) + (rename-out [define-syntax-category define-stx-category])) (module+ test (require (for-syntax rackunit))) @@ -57,27 +59,26 @@ (struct exn:fail:type:runtime exn:fail:user ()) -;; drop-file-ext : String -> String -(define-for-syntax (drop-file-ext filename) - (car (string-split filename "."))) -;; extract-filename : PathString -> String -(define-for-syntax (extract-filename f) - (path->string (path-replace-suffix (file-name-from-path f) ""))) - (begin-for-syntax + (define (mk-? id) (format-id id "~a?" id)) + (define (mk-* id) (format-id id "~a*" id)) + (define (mk-~ id) (format-id id "~~~a" id)) + (define-for-syntax (mk-? id) (format-id id "~a?" id)) + (define-for-syntax (mk-~ id) (format-id id "~~~a" id)) + ;; drop-file-ext : String -> String + (define (drop-file-ext filename) + (car (string-split filename "."))) + ;; extract-filename : PathString -> String + (define (extract-filename f) + (path->string (path-replace-suffix (file-name-from-path f) ""))) (define-syntax-parameter stx (syntax-rules ()))) (define-syntax (define-typed-syntax stx) (syntax-parse stx - [(_ name:id #:export-as out-name:id stx-parse-clause ...+) - #'(begin - (provide (rename-out [name out-name])) - (define-syntax (name syntx) - (syntax-parameterize ([stx (make-rename-transformer #'syntx)]) - (syntax-parse syntx stx-parse-clause ...))))] [(_ name:id stx-parse-clause ...+) - #'(define-typed-syntax name #:export-as name - stx-parse-clause ...)])) + #'(define-syntax (name syntx) + (syntax-parameterize ([stx (make-rename-transformer #'syntx)]) + (syntax-parse syntx stx-parse-clause ...)))])) ;; need options for ;; - pass through @@ -158,14 +159,14 @@ (let* ([pre-str #,(string-append (extract-filename (syntax-e #'base-lang)) ":")] [pre-str-len (string-length pre-str)] [drop-pre (λ (s) (substring s pre-str-len))] - [excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))] - [origs (map symbol->string (syntax->datum #'(x ...)))]) +; [excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))] + [origs (map symbol->string (syntax->datum #'(x ... new ...)))]) (λ (name) (define out-name (or (and (string-prefix? name pre-str) (drop-pre name)) name)) - (and (not (member out-name excluded)) + (and #;(not (member out-name excluded)) (member out-name origs) out-name))) (all-from-out base-lang)))))])) @@ -239,7 +240,7 @@ [(_ e as tycon) #:with τ? (mk-? #'tycon) #:with τ-get (format-id #'tycon "~a-get" #'tycon) - #:with τ-expander (format-id #'tycon "~~~a" #'tycon) + #:with τ-expander (mk-~ #'tycon) #'(syntax-parse ;; when type error, prefer outer err msg (with-handlers ([exn:fail? @@ -276,7 +277,7 @@ [(_ es as tycon) #:with τ? (mk-? #'tycon) #:with τ-get (format-id #'tycon "~a-get" #'tycon) - #:with τ-expander (format-id #'tycon "~~~a" #'tycon) + #:with τ-expander (mk-~ #'tycon) #'(syntax-parse (stx-map infer+erase #'es) #:context #'es [((e- τ_e_) (... ...)) #:with (τ_e (... ...)) (stx-map (current-promote) #'(τ_e_ (... ...))) @@ -291,7 +292,6 @@ (quote-syntax tycon) t))) #'es #'(τ_e (... ...))) - ;#:with args (τ-get #'τ_e) #:with res (stx-map (λ (e t) (syntax-parse t @@ -322,7 +322,7 @@ #:with ([tv (~seq sep:id tvk) ...] ...) tvctx #:with (e ...) es #:with - ; old expander pattern + ; old expander pattern (leave commented out) #;((~literal #%plain-lambda) tvs+ ((~literal #%expression) ((~literal #%plain-lambda) xs+ @@ -372,9 +372,7 @@ #:with app (datum->syntax #'o '#%app) (datum->syntax this-syntax (list* #'app (assign-type #'x #'τ) #'rst) - this-syntax)] - #;[(_ . rst) #`(#,(assign-type #'x #'τ) . rst)]) - #;(make-rename-transformer (assign-type #'x #'τ))] ...) + this-syntax)])] ...) (#%expression e) ... void))))) (list #'tvs+ #'xs+ #'(e+ ...) (stx-map ; need this check when combining #%type and kinds @@ -531,8 +529,6 @@ (string-join (stx-map type->str tys) sep))) (begin-for-syntax - (define (mk-? id) (format-id id "~a?" id)) - (define-for-syntax (mk-? id) (format-id id "~a?" id)) (define (brace? stx) (define paren-shape/#f (syntax-property stx 'paren-shape)) (and paren-shape/#f (char=? paren-shape/#f #\{))) @@ -602,18 +598,14 @@ (define-syntax define-basic-checked-id-stx (syntax-parser #:datum-literals (:) - [(_ τ:id : kind - (~optional (~and #:no-provide (~parse no-provide? #'#t)))) + [(_ τ:id : kind) #:with #%tag (format-id #'kind "#%~a" #'kind) #:with τ? (mk-? #'τ) #:with τ-internal (generate-temporary #'τ) - #:with τ-expander (format-id #'τ "~~~a" #'τ) + #:with τ-expander (mk-~ #'τ) #`(begin - #,@(if (attribute no-provide?) - #'() - #'((provide τ (for-syntax τ? τ-expander)))) (begin-for-syntax - (define (τ? t) ;(and (identifier? t) (free-identifier=? t #'τ-internal))) + (define (τ? t) (syntax-parse t [((~literal #%plain-app) (~literal τ-internal)) #t][_ #f])) (define (inferτ+erase e) @@ -628,9 +620,7 @@ (define-syntax τ-expander (pattern-expander (syntax-parser - ;[ty:id #'(~literal τ-internal)] [ty:id #'((~literal #%plain-app) (~literal τ-internal))] - ;[(_ . rst) #'((~literal τ-internal) . rst)])))) [(_ . rst) #'(((~literal #%plain-app) (~literal τ-internal)) . rst)])))) (define τ-internal (λ () (raise (exn:fail:type:runtime @@ -638,7 +628,6 @@ (current-continuation-marks))))) (define-syntax τ (syntax-parser - ;[(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))])) [(~var _ id) (add-orig (assign-type @@ -662,24 +651,20 @@ #`(λ (stx-id) (for/list ([arg (in-list (stx->list (stx-cdr stx-id)))]) invariant))])) (~optional (~seq #:extra-info extra-info) - #:defaults ([extra-info #'void])) - (~optional (~and #:no-provide (~parse no-provide? #'#t)))) + #:defaults ([extra-info #'void]))) #:with #%kind (format-id #'kind "#%~a" #'kind) #:with τ-internal (generate-temporary #'τ) #:with τ? (mk-? #'τ) - #:with τ-expander (format-id #'τ "~~~a" #'τ) - #:with τ-expander* (format-id #'τ-expander "~a*" #'τ-expander) + #:with τ-expander (mk-~ #'τ) + #:with τ-expander* (mk-* #'τ-expander) #`(begin - #,@(if (attribute no-provide?) - #'() - #'((provide τ (for-syntax τ-expander τ-expander* τ?)))) (begin-for-syntax (define-syntax τ-expander (pattern-expander (syntax-parser [(_ . pat:id) #:with expanded-τ (generate-temporary) - #:with tycon-expander (format-id #'tycon "~~~a" #'tycon) + #:with tycon-expander (mk-~ #'tycon) #'(~and expanded-τ (~Any/bvs (~literal/else τ-internal (format "Expected ~a type, got: ~a" @@ -746,7 +731,6 @@ #:with (bvs- τs- _) (infers/ctx+erase #'bvs #'args) #:with (~! (~var _ kind) (... ...)) #'τs- #:with ([tv (~datum :) k_arg] (... ...)) #'bvs -; #:with (k_arg+ (... ...)) (stx-map (current-type-eval) #'(k_arg (... ...))) #:with k_result (if #,(attribute has-annotations?) #'(tycon k_arg (... ...)) #'#%kind) @@ -786,9 +770,10 @@ #:with names=? (format-id #'names "~a=?" #'names) #:with current-name=? (format-id #'name=? "current-~a" #'name=?) #:with same-names? (format-id #'name "same-~as?" #'name) + #:with name-out (format-id #'name "~a-out" #'name) #'(begin - (provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann name-ctx same-names?) - #%tag define-base-name define-base-names define-name-cons) + ;; (provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann name-ctx same-names?) + ;; #%tag define-base-name define-base-names define-name-cons) (define #%tag void) (begin-for-syntax (define (#%tag? t) (and (identifier? t) (free-identifier=? t #'#%tag))) @@ -860,6 +845,20 @@ (define τs-lst (syntax->list τs)) (or (null? τs-lst) (andmap (λ (τ) ((current-name=?) (car τs-lst) τ)) (cdr τs-lst))))) + ;; helps with providing defined types + (define-syntax name-out + (make-provide-transformer + (lambda (stx modes) + (syntax-parse stx + ;; cannot write ty:type bc provides might precede type def + [(_ . ts) + #:with t-expanders (stx-map mk-~ #'ts) + #:with t?s (stx-map mk-? #'ts) + (expand-export + (syntax/loc stx (combine-out + (combine-out . ts) + (for-syntax (combine-out . t-expanders) . t?s))) + modes)])))) (define-syntax define-base-name (syntax-parser [(_ (~var x id) . rst) #'(define-basic-checked-id-stx x : name . rst)])) diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt index 53eba1a..58196d0 100644 --- a/turnstile/examples/exist.rkt +++ b/turnstile/examples/exist.rkt @@ -9,6 +9,8 @@ ;; - terms from stlc+reco+var.rkt ;; - pack and open +(provide ∃ pack open) + (define-type-constructor ∃ #:bvs = 1) (define-typed-syntax (pack (τ:type e) as ∃τ:type) ≫ diff --git a/turnstile/examples/ext-stlc.rkt b/turnstile/examples/ext-stlc.rkt index 58b73a0..17a2a4e 100644 --- a/turnstile/examples/ext-stlc.rkt +++ b/turnstile/examples/ext-stlc.rkt @@ -15,14 +15,20 @@ ;; - begin ;; - ascription (ann) ;; - let, let*, letrec +;; Top-level: +;; - define (values only) +;; - define-type-alias -(provide (for-syntax current-join) - ⊔ zero? = +(provide define-type-alias + (for-syntax current-join) ⊔ + (type-out Bool String Float Char Unit) + zero? = (rename-out [typed- -] [typed* *]) (typed-out [add1 (→ Int Int)] [sub1 : (→ Int Int)] [[not- (→ Bool Bool)] not] - [[void- : (→ Unit)] void])) + [[void- : (→ Unit)] void]) + define #%datum and or if begin ann let let* letrec) (define-base-types Bool String Float Char Unit) @@ -32,6 +38,33 @@ (define-primop typed- - (→ Int Int Int)) (define-primop typed* * : (→ Int Int Int)) +;; Using τ.norm leads to a "not valid type" error when file is compiled +(define-syntax define-type-alias + (syntax-parser + [(define-type-alias alias:id τ:type) + #'(define-syntax alias (make-variable-like-transformer #'τ))] + [(define-type-alias (f:id x:id ...) ty) + #'(define-syntax (f stx) + (syntax-parse stx + [(_ x ...) #'ty]))])) + +(define-typed-syntax define + [(_ x:id : τ:type e:expr) ≫ + ;This wouldn't work with mutually recursive definitions + ;[⊢ [e ≫ e- ⇐ τ.norm]] + ;So expand to an ann form instead. + -------- + [≻ (begin- + (define-syntax x (make-rename-transformer (⊢ y : τ.norm))) + (define- y (ann e : τ.norm)))]] + [(_ x:id e) ≫ + [⊢ e ≫ e- ⇒ τ] + #:with y (generate-temporary #'x) + -------- + [≻ (begin- + (define-syntax x (make-rename-transformer (⊢ y : τ))) + (define- y e-))]]) + (define-typed-syntax #%datum [(_ . b:boolean) ≫ -------- diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt index c5e523a..e6442f8 100644 --- a/turnstile/examples/fomega.rkt +++ b/turnstile/examples/fomega.rkt @@ -1,5 +1,5 @@ #lang turnstile/lang -(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst) +(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst) (reuse String #%datum #:from "stlc+reco+var.rkt") ;; System F_omega @@ -12,6 +12,11 @@ ;; - add tyλ and tyapp ;; - #%datum from stlc+reco+var +(provide (for-syntax current-kind?) + define-type-alias + (type-out ★ ⇒ ∀★ ∀) + Λ inst tyλ tyapp) + (define-syntax-category kind) ; want #%type to be equiv to★ @@ -24,23 +29,26 @@ ;; eg in the definition of λ or previous type constuctors. ;; (However, this is not completely possible, eg define-type-alias) ;; So now "type?" no longer validates types, rather it's a subset. - ;; But we no longer need type? to validate types, instead we can use (kind? (typeof t)) + ;; But we no longer need type? to validate types, instead we can use + ;; (kind? (typeof t)) (current-type? (λ (t) (define k (typeof t)) #;(or (type? t) (★? (typeof t)) (∀★? (typeof t))) (and ((current-kind?) k) (not (⇒? k)))))) ; must override, to handle kinds -(provide define-type-alias) (define-syntax define-type-alias (syntax-parser [(define-type-alias alias:id τ) #:with (τ- k_τ) (infer+erase #'τ) - #:fail-unless ((current-kind?) #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ)) - #'(define-syntax alias (syntax-parser [x:id #'τ-] [(_ . rst) #'(τ- . rst)]))])) + #:fail-unless ((current-kind?) #'k_τ) + (format "not a valid type: ~a\n" (type->str #'τ)) + #'(define-syntax alias + (syntax-parser [x:id #'τ-] [(_ . rst) #'(τ- . rst)]))])) -(provide ★ (for-syntax ★?)) -(define-for-syntax ★? #%type?) +(begin-for-syntax + (define ★? #%type?) + (define-syntax ~★ (lambda _ (error "~★ not implemented")))) ; placeholder (define-syntax ★ (make-rename-transformer #'#%type)) (define-kind-constructor ⇒ #:arity >= 1) (define-kind-constructor ∀★ #:arity >= 0) diff --git a/turnstile/examples/fomega2.rkt b/turnstile/examples/fomega2.rkt index f2ac63a..441ab80 100644 --- a/turnstile/examples/fomega2.rkt +++ b/turnstile/examples/fomega2.rkt @@ -1,5 +1,5 @@ #lang turnstile/lang -(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst) +(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst) (reuse String #%datum #:from "stlc+reco+var.rkt") ; same as fomega.rkt except here λ and #%app works as both type and terms @@ -15,6 +15,10 @@ ;; - extend ∀ Λ inst from sysf ;; - #%datum from stlc+reco+var +(provide define-type-alias + ★ ∀★ ∀ + Λ inst) + (define-syntax-category kind) (begin-for-syntax @@ -23,19 +27,20 @@ ;; eg in the definition of λ or previous type constuctors. ;; (However, this is not completely possible, eg define-type-alias) ;; So now "type?" no longer validates types, rather it's a subset. - ;; But we no longer need type? to validate types, instead we can use (kind? (typeof t)) + ;; But we no longer need type? to validate types, instead we can use + ;; (kind? (typeof t)) (current-type? (λ (t) (or (type? t) (let ([k (typeof t)]) (or (★? k) (∀★? k))) ((current-kind?) t))))) ; must override -(provide define-type-alias) (define-syntax define-type-alias (syntax-parser [(_ alias:id τ) #:with (τ- k_τ) (infer+erase #'τ) - #'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))])) + #'(define-syntax alias + (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))])) (define-base-kind ★) (define-kind-constructor ∀★ #:arity >= 0) diff --git a/turnstile/examples/fomega3.rkt b/turnstile/examples/fomega3.rkt index 6459123..08b5af8 100644 --- a/turnstile/examples/fomega3.rkt +++ b/turnstile/examples/fomega3.rkt @@ -1,8 +1,5 @@ #lang turnstile/lang -(extends "sysf.rkt" #:except #%datum ∀ Λ inst) -(reuse String #%datum #:from "stlc+reco+var.rkt") -(require (only-in "fomega.rkt" current-kind? ∀★? ★? kind?)) -(reuse ★ ∀ Λ inst define-type-alias ∀★ #:from "fomega.rkt") +(extends "fomega.rkt" #:except tyapp tyλ) ; same as fomega2.rkt --- λ and #%app works as both regular and type versions, ; → is both type and kind --- but reuses parts of fomega.rkt, @@ -21,12 +18,14 @@ ;; types and kinds are now mixed, due to #%app and λ (begin-for-syntax - (current-kind? (λ (k) (or (#%type? k) (kind? k) (#%type? (typeof k))))) + (define old-kind? (current-kind?)) + (current-kind? (λ (k) (or (#%type? k) (old-kind? k) (#%type? (typeof k))))) ;; Try to keep "type?" backward compatible with its uses so far, ;; eg in the definition of λ or previous type constuctors. ;; (However, this is not completely possible, eg define-type-alias) ;; So now "type?" no longer validates types, rather it's a subset. - ;; But we no longer need type? to validate types, instead we can use (kind? (typeof t)) + ;; But we no longer need type? to validate types, instead we can use + ;; (kind? (typeof t)) (current-type? (λ (t) (or (type? t) (let ([k (typeof t)]) (or (★? k) (∀★? k))) diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt index 0deaa11..fa55a35 100644 --- a/turnstile/examples/fsub.rkt +++ b/turnstile/examples/fsub.rkt @@ -14,7 +14,9 @@ ;; - current-promote, expose ;; - extend current-sub? to call current-promote -(provide (typed-out [+ : (→ Nat Nat Nat)])) +(provide <: ∀ + (typed-out [+ : (→ Nat Nat Nat)]) + Λ inst) ; can't just call expose in type-eval, ; otherwise typevars will have bound as type, rather than instantiated type diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt index ee95d4a..920de2d 100644 --- a/turnstile/examples/infer.rkt +++ b/turnstile/examples/infer.rkt @@ -1,13 +1,15 @@ #lang turnstile/lang -(extends "ext-stlc.rkt" #:except #%app λ ann) +(extends "ext-stlc.rkt" #:except define #%app λ ann) (reuse inst #:from "sysf.rkt") (require (only-in "sysf.rkt" ∀ ~∀ ∀? Λ)) (reuse cons [head hd] [tail tl] nil [isnil nil?] List list #:from "stlc+cons.rkt") -(require (only-in "stlc+cons.rkt" ~List)) +;(require (only-in "stlc+cons.rkt" ~List)) (reuse tup × proj #:from "stlc+tup.rkt") (reuse define-type-alias #:from "stlc+reco+var.rkt") (require (for-syntax macrotypes/type-constraints)) -(provide hd tl nil? ∀) +;(provide hd tl nil? ∀) + +(provide → ∀ define define/rec λ #%app) ;; (Some [X ...] τ_body (Constraints (Constraint τ_1 τ_2) ...)) (define-type-constructor Some #:arity = 2 #:bvs >= 0) @@ -216,6 +218,3 @@ [_ ≻ (begin- (define-syntax- x (make-rename-transformer (⊢ tmp : τ_x.norm))) (define- tmp (ann e : τ_x.norm)))]]) - - - diff --git a/turnstile/examples/mlish+adhoc.rkt b/turnstile/examples/mlish+adhoc.rkt index 1a9fc0b..97cbf48 100644 --- a/turnstile/examples/mlish+adhoc.rkt +++ b/turnstile/examples/mlish+adhoc.rkt @@ -1,7 +1,10 @@ #lang turnstile (require racket/fixnum racket/flonum) -(extends "ext-stlc.rkt" #:except #%app λ → + - * void = zero? sub1 add1 not let let* and #%datum begin +(extends + "ext-stlc.rkt" + #:except → #%app λ define begin #%datum + + - * void = zero? sub1 add1 not let let* and #:rename [~→ ~ext-stlc:→]) (require (rename-in (only-in "sysf.rkt" inst) [inst sysf:inst])) (require (only-in "ext-stlc.rkt" →?)) @@ -12,7 +15,6 @@ (reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt") (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil))) (require (only-in "stlc+cons.rkt" ~List List? List)) -(provide List) (reuse ref deref := Ref #:from "stlc+box.rkt") (require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×) [tup rec] [proj get] [× ××])) @@ -21,10 +23,6 @@ (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list))) (require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup))) -(provide → →/test =>/test match2 define-type) - -(provide define-typeclass define-instance) - ;; ML-like language + ad-hoc polymorphism ;; - top level recursive functions ;; - user-definable algebraic datatypes @@ -33,8 +31,25 @@ ;; ;; - type classes +(provide → →/test => =>/test + List Channel Thread Vector Sequence Hash String-Port Input-Port Regexp + define-type define-typeclass define-instance + match2) + (define-type-constructor => #:arity > 0) +;; providing version of define-typed-syntax +(define-syntax (define-typed-syntax stx) + (syntax-parse stx + [(_ name:id #:export-as out-name:id . rst) + #'(begin- + (provide- (rename-out [name out-name])) + (define-typerule name . rst))] ; define-typerule doesnt provide + [(_ name:id . rst) + #'(define-typed-syntax name #:export-as name . rst)] + [(_ (name:id . pat) . rst) + #'(define-typed-syntax name #:export-as name [(_ . pat) . rst])])) + ;; type class helper fns (begin-for-syntax (define (mk-app-err-msg stx #:expected [expected-τs #'()] @@ -400,8 +415,7 @@ [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)])) (define-type-constructor Name #:arity = #,(stx-length #'(X ...)) - #:extra-info 'NameExtraInfo - #:no-provide) + #:extra-info 'NameExtraInfo) (struct- StructName (fld ...) #:reflection-name 'Cons #:transparent) ... (define-syntax- (exposed-acc stx) ; accessor for records (syntax-parse stx diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt index 3212d37..d884edc 100644 --- a/turnstile/examples/mlish.rkt +++ b/turnstile/examples/mlish.rkt @@ -1,19 +1,23 @@ #lang turnstile/lang -(require racket/fixnum racket/flonum - (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) +(require + racket/fixnum racket/flonum + (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) -(extends "ext-stlc.rkt" #:except #%app λ → + - * void = zero? sub1 add1 not let let* and #%datum begin - #:rename [~→ ~ext-stlc:→]) +(extends + "ext-stlc.rkt" + #:except → define #%app λ #%datum begin + + - * void = zero? sub1 add1 not let let* and + #:rename [~→ ~ext-stlc:→]) (reuse inst #:from "sysf.rkt") (require (only-in "ext-stlc.rkt" → →?)) (require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ)) (reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt") (require (only-in "stlc+rec-iso.rkt" ~× ×?)) (provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum])) -(reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt") +(reuse member length reverse list-ref cons nil isnil head tail list + #:from "stlc+cons.rkt") (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil))) (require (only-in "stlc+cons.rkt" ~List List? List)) -(provide List) (reuse ref deref := Ref #:from "stlc+box.rkt") (require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×) [tup rec] [proj get] [× ××])) @@ -22,17 +26,32 @@ (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list))) (require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup))) -(module+ test - (require (for-syntax rackunit))) - -(provide → →/test match2 define-type) - ;; ML-like language ;; - top level recursive functions ;; - user-definable algebraic datatypes ;; - pattern matching ;; - (local) type inference +(provide → →/test + define-type + List Channel Thread Vector Sequence Hash String-Port Input-Port Regexp + match2) + +;; providing version of define-typed-syntax +(define-syntax (define-typed-syntax stx) + (syntax-parse stx + [(_ name:id #:export-as out-name:id . rst) + #'(begin- + (provide- (rename-out [name out-name])) + (define-typerule name . rst))] ; define-typerule doesnt provide + [(_ name:id . rst) + #'(define-typed-syntax name #:export-as name . rst)] + [(_ (name:id . pat) . rst) + #'(define-typed-syntax name #:export-as name [(_ . pat) . rst])])) + +(module+ test + (require (for-syntax rackunit))) + ;; creating possibly polymorphic types ;; ?∀ only wraps a type in a forall if there's at least one type variable (define-syntax ?∀ @@ -311,7 +330,7 @@ ;; which is not known to programmers, to make the result slightly more ;; intuitive, we arbitrarily sort the inferred tyvars lexicographically (define-typed-syntax define - [(define x:id e) ≫ + [(_ x:id e) ≫ [⊢ e ≫ e- ⇒ τ] #:with y (generate-temporary) -------- @@ -319,7 +338,7 @@ (define-syntax x (make-rename-transformer (⊢ y : τ))) (define- y e-))]] ; explicit "forall" - [(define Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) + [(_ Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) e_body ... e) ≫ #:when (brace? #'Ys) ;; TODO; remove this code duplication @@ -337,10 +356,10 @@ (define- g (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]] ;; alternate type sig syntax, after parameter names - [(define (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b) ≫ + [(_ (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b) ≫ -------- [≻ (define (f [x : ty] ... -> ty_out) . b)]] - [(define (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) + [(_ (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) e_body ... e) ≫ #:with Ys (compute-tyvars #'(τ ... τ_out)) #:with g (add-orig (generate-temporary #'f) #'f) @@ -438,8 +457,7 @@ #:arg-variances (make-arg-variances-proc arg-variance-vars (list #'X ...) (list #'τ ... ...)) - #:extra-info 'NameExtraInfo - #:no-provide) + #:extra-info 'NameExtraInfo) (struct- StructName (fld ...) #:reflection-name 'Cons #:transparent) ... (define-syntax (exposed-acc stx) ; accessor for records (syntax-parse stx @@ -1226,7 +1244,7 @@ (define-type-constructor Hash #:arity = 2) (define-typed-syntax in-hash - [(in-hash e) ≫ + [(_ e) ≫ [⊢ [e ≫ e- ⇒ : (~Hash ty_k ty_v)]] -------- [⊢ [_ ≫ (hash-map- e- list-) ⇒ : (Sequence (stlc+rec-iso:× ty_k ty_v))]]]) diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt index 9e0d774..042e3ab 100644 --- a/turnstile/examples/rosette/bv.rkt +++ b/turnstile/examples/rosette/bv.rkt @@ -5,7 +5,16 @@ (require (only-in sdsl/bv/lang/bvops bvredand bvredor bv bv*) (prefix-in bv: (only-in sdsl/bv/lang/bvops BV))) (require sdsl/bv/lang/core (prefix-in bv: sdsl/bv/lang/form)) -(provide thunk) + +(provide Prog Lib + (typed-out [bv : (Ccase-> (C→ CInt CBV) + (C→ CInt CBVPred CBV) + (C→ CInt CPosInt CBV))] + [bv* : (Ccase-> (C→ BV) + (C→ CBVPred BV))] + [bvredor : (C→ BV BV)] + [bvredand : (C→ BV BV)]) + current-bvpred define-fragment bvlib thunk) ;; this must be a macro in order to support Racket's overloaded set/get ;; parameter patterns @@ -21,14 +30,6 @@ -------- [⊢ [_ ≫ (bv:BV e-) ⇒ : CUnit]]]) -(provide (typed-out [bv : (Ccase-> (C→ CInt CBV) - (C→ CInt CBVPred CBV) - (C→ CInt CPosInt CBV))] - [bv* : (Ccase-> (C→ BV) - (C→ CBVPred BV))] - [bvredor : (C→ BV BV)] - [bvredand : (C→ BV BV)])) - (define-syntax-rule (bv:bool->bv b) (ro:if b (bv (rosette2:#%datum . 1)) @@ -49,7 +50,8 @@ (define-typed-syntax define-fragment [(_ (id param ...) #:implements spec #:library lib-expr) ≫ -------- - [_ ≻ (define-fragment (id param ...) #:implements spec #:library lib-expr #:minbv (rosette2:#%datum . 4))]] + [_ ≻ (define-fragment (id param ...) + #:implements spec #:library lib-expr #:minbv (rosette2:#%datum . 4))]] [(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv) ≫ [⊢ [spec ≫ spec- ⇒ : ty_spec]] #:fail-unless (C→? #'ty_spec) "spec must be a function" @@ -63,8 +65,10 @@ #:implements spec- #:library lib-expr- #:minbv minbv-)) - (define-syntax id (make-rename-transformer (⊢ id-internal : ty_spec))) - (define-syntax id-stx (make-rename-transformer (⊢ id-stx-internal : CStx))) + (define-syntax id + (make-rename-transformer (⊢ id-internal : ty_spec))) + (define-syntax id-stx + (make-rename-transformer (⊢ id-stx-internal : CStx))) )]]) (define-typed-syntax bvlib diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt index 83a011f..63ea330 100644 --- a/turnstile/examples/rosette/fsm.rkt +++ b/turnstile/examples/rosette/fsm.rkt @@ -3,11 +3,19 @@ (require (prefix-in ro: rosette)) ; untyped (require (prefix-in ro: rosette/lib/synthax)) (require (prefix-in fsm: sdsl/fsm/fsm)) -(require (only-in sdsl/fsm/fsm reject verify-automaton debug-automaton synthesize-automaton)) +(require (only-in sdsl/fsm/fsm + reject verify-automaton debug-automaton synthesize-automaton)) (provide (rename-out [rosette:choose ?])) (require (for-syntax lens unstable/lens)) +(provide FSM State Pict + (typed-out [reject : State] + [verify-automaton : (→ FSM Regexp (List Symbol))] + [debug-automaton : (→ FSM Regexp (List Symbol) Pict)] + [synthesize-automaton : (→ FSM Regexp Unit)]) + #%datum #%app automaton) + (define-base-types FSM State Pict) ;; extend rosette:#%datum to handle regexp literals @@ -21,7 +29,7 @@ [_ ≻ (rosette:#%datum . v)]]) ;; extend rosette:#%app to work with FSM -(define-typed-syntax app #:export-as #%app +(define-typed-syntax #%app [(_ f e) ≫ [⊢ [f ≫ f- ⇐ : FSM]] [⊢ [e ≫ e- ⇐ : (List Symbol)]] @@ -47,11 +55,6 @@ [⊢ [_ ≫ (fsm:automaton init-state- [state- : (label arr target-) ...] ...) ⇒ : FSM]]]) -(provide (typed-out [reject : State] - [verify-automaton : (→ FSM Regexp (List Symbol))] - [debug-automaton : (→ FSM Regexp (List Symbol) Pict)] - [synthesize-automaton : (→ FSM Regexp Unit)])) - ;; (define (apply-FSM f v) (f v)) ;; (define-primop apply-FSM : (→ FSM (List Symbol) Bool)) diff --git a/turnstile/examples/rosette/ifc.rkt b/turnstile/examples/rosette/ifc.rkt index a956bc2..2f1895a 100644 --- a/turnstile/examples/rosette/ifc.rkt +++ b/turnstile/examples/rosette/ifc.rkt @@ -2,7 +2,6 @@ (extends "rosette.rkt" #:except) ; extends typed rosette (require (prefix-in ro: rosette)) ; untyped (require (prefix-in ro: rosette/lib/synthax)) -;(require (prefix-in ifc: sdsl/ifc/instruction)) (require sdsl/ifc/instruction) ; program (require sdsl/ifc/basic) ; Halt, Noop, Push, etc (require (except-in sdsl/ifc/machine write read)) ; init, halted? @@ -11,7 +10,8 @@ (define-base-types Prog Instr Machine Witness) -(provide (typed-out [Halt : Instr] +(provide Prog Instr Machine Witness + (typed-out [Halt : Instr] [Noop : Instr] [Push : Instr] [Pop : Instr] diff --git a/turnstile/examples/rosette/lib/render.rkt b/turnstile/examples/rosette/lib/render.rkt index 4f666e4..f0e46e0 100644 --- a/turnstile/examples/rosette/lib/render.rkt +++ b/turnstile/examples/rosette/lib/render.rkt @@ -2,6 +2,7 @@ (require (prefix-in t/ro: (only-in "../rosette2.rkt" CNat CSolution CPict)) (prefix-in ro: rosette/lib/render)) +(provide render) (define-typed-syntax render [(_ s) ≫ diff --git a/turnstile/examples/rosette/lib/synthax.rkt b/turnstile/examples/rosette/lib/synthax.rkt index bd09473..d8adc5f 100644 --- a/turnstile/examples/rosette/lib/synthax.rkt +++ b/turnstile/examples/rosette/lib/synthax.rkt @@ -4,7 +4,8 @@ (prefix-in t/ro: (only-in "../rosette2.rkt" Int Bool C→ CSolution Unit)) (prefix-in ro: rosette/lib/synthax)) -(provide (rosette-typed-out [print-forms : (t/ro:C→ t/ro:CSolution t/ro:Unit)])) +(provide (rosette-typed-out [print-forms : (t/ro:C→ t/ro:CSolution t/ro:Unit)]) + ??) (define-typed-syntax ?? [(qq) ≫ diff --git a/turnstile/examples/rosette/query/debug.rkt b/turnstile/examples/rosette/query/debug.rkt index a265d33..7d23e55 100644 --- a/turnstile/examples/rosette/query/debug.rkt +++ b/turnstile/examples/rosette/query/debug.rkt @@ -1,8 +1,11 @@ #lang turnstile (require - (prefix-in t/ro: (only-in "../rosette2.rkt" λ ann begin C→ Nothing Bool CSolution)) + (prefix-in t/ro: (only-in "../rosette2.rkt" + λ ann begin C→ Nothing Bool CSolution)) (prefix-in ro: rosette/query/debug)) +(provide define/debug debug) + (define-typed-syntax define/debug #:datum-literals (: -> →) [(_ x:id e) ≫ [⊢ [e ≫ e- ⇒ : τ]] @@ -16,14 +19,15 @@ #:with f- (generate-temporary #'f) -------- [_ ≻ (begin- - (define-syntax- f (make-rename-transformer (⊢ f- : (t/ro:C→ ty ... ty_out)))) - (ro:define/debug f- - (t/ro:λ ([x : ty] ...) - (t/ro:ann (t/ro:begin e ...) : ty_out))))]]) + (define-syntax- f + (make-rename-transformer (⊢ f- : (t/ro:C→ ty ... ty_out)))) + (ro:define/debug f- + (t/ro:λ ([x : ty] ...) + (t/ro:ann (t/ro:begin e ...) : ty_out))))]]) (define-typed-syntax debug [(_ (solvable-pred ...+) e) ≫ - [⊢ [solvable-pred ≫ solvable-pred- ⇐ : (t/ro:C→ t/ro:Nothing t/ro:Bool)]] ... + [⊢ solvable-pred ≫ solvable-pred- ⇐ (t/ro:C→ t/ro:Nothing t/ro:Bool)] ... [⊢ [e ≫ e- ⇒ : τ]] -------- [⊢ [_ ≫ (ro:debug (solvable-pred- ...) e-) ⇒ : t/ro:CSolution]]]) diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt index 751ae7f..cd26217 100644 --- a/turnstile/examples/rosette/rosette.rkt +++ b/turnstile/examples/rosette/rosette.rkt @@ -1,11 +1,23 @@ #lang turnstile -(extends "../stlc+union+case.rkt" #:except if #%app #%module-begin add1 sub1 +) +(extends "../stlc+union+case.rkt" + #:except define if #%app #%module-begin add1 sub1 +) (reuse List list #:from "../stlc+cons.rkt") -(require (only-in "../stlc+reco+var.rkt" [define stlc:define])) -;(require (only-in "../stlc+reco+var.rkt" define-type-alias)) (require (prefix-in ro: rosette)) (require (prefix-in ro: rosette/lib/synthax)) -(provide BVPred (rename-out [ro:#%module-begin #%module-begin])) +(provide (rename-out [ro:#%module-begin #%module-begin]) + Symbol Regexp Param Stx BV BVPred) + +;; providing version of define-typed-syntax +(define-syntax (define-typed-syntax stx) + (syntax-parse stx + [(_ name:id #:export-as out-name:id . rst) + #'(begin- + (provide- (rename-out [name out-name])) + (define-typerule name . rst))] ; define-typerule doesnt provide + [(_ name:id . rst) + #'(define-typed-syntax name #:export-as name . rst)] + [(_ (name:id . pat) . rst) + #'(define-typed-syntax name #:export-as name [(_ . pat) . rst])])) (define-for-syntax (mk-ro:-id id) (format-id id "ro:~a" id)) @@ -151,14 +163,16 @@ (define-typed-syntax define #:datum-literals (: -> →) [(_ x:id e) ≫ -------- - [_ ≻ (stlc:define x e)]] + [_ ≻ (stlc+union+case:define x e)]] [(_ (f [x : ty] ... (~or → ->) ty_out) e) ≫ ; [⊢ [e ≫ e- ⇒ : ty_e]] #:with f- (generate-temporary #'f) -------- [_ ≻ (begin- - (define-syntax- f (make-rename-transformer (⊢ f- : (→ ty ... ty_out)))) - (stlc:define f- (stlc+union+case:λ ([x : ty] ...) e)))]]) + (define-syntax- f + (make-rename-transformer (⊢ f- : (→ ty ... ty_out)))) + (stlc+union+case:define f- + (stlc+union+case:λ ([x : ty] ...) e)))]]) (define-base-type Stx) diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index 25cb23b..dfbed87 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -1,9 +1,8 @@ #lang turnstile (extends "../stlc.rkt" #:except #%module-begin #%app →) -(reuse #%datum #:from "../stlc+union.rkt") -(reuse define-type-alias #:from "../stlc+reco+var.rkt") -(reuse define-named-type-alias #:from "../stlc+union.rkt") +(reuse #%datum define-type-alias define-named-type-alias + #:from "../stlc+union.rkt") (reuse list #:from "../stlc+cons.rkt") (provide (rename-out [ro:#%module-begin #%module-begin]) @@ -11,7 +10,8 @@ CU U C→ → (for-syntax ~C→ C→?) Ccase-> ; TODO: symbolic case-> not supported yet - CListof CVectorof CParamof ; TODO: symbolic Param not supported yet + CListof CVectorof CMVectorof CIVectorof + CParamof ; TODO: symbolic Param not supported yet CUnit Unit CNegInt NegInt CZero Zero @@ -26,7 +26,7 @@ ;; BV types CBV BV CBVPred BVPred - ) + CSolution CPict) (require (prefix-in ro: rosette) @@ -34,7 +34,8 @@ (prefix-in C (combine-in (only-in "../stlc+union+case.rkt" - PosInt Zero NegInt Float True False String [U U*] U*? [case-> case->*] → →?) + PosInt Zero NegInt Float True False String [U U*] U*? + [case-> case->*] → →?) (only-in "../stlc+cons.rkt" Unit [List Listof]))) (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→]) (only-in "../stlc+cons.rkt" [~List ~CListof]) @@ -56,6 +57,18 @@ (pre-expand-export (syntax/loc stx (typed-out [[ro-x ty] out-x] ...)) modes)])))) +;; providing version of define-typed-syntax +(define-syntax (define-typed-syntax stx) + (syntax-parse stx + [(_ name:id #:export-as out-name:id . rst) + #'(begin- + (provide- (rename-out [name out-name])) + (define-typerule name . rst))] ; define-typerule doesnt provide + [(_ name:id . rst) + #'(define-typed-syntax name #:export-as name . rst)] + [(_ (name:id . pat) . rst) + #'(define-typed-syntax name #:export-as name [(_ . pat) . rst])])) + ;; --------------------------------- ;; Concrete and Symbolic union types @@ -109,7 +122,6 @@ ;; types? Should it transform (case-> (U (C→ τ ...)) ...) ;; into (U (Ccase-> (C→ τ ...) ...)) ? What makes sense here? - ;; --------------------------------- ;; Symbolic versions of types @@ -235,8 +247,10 @@ #:with f- (generate-temporary #'f) -------- [_ ≻ (begin- - (define-syntax- f (make-rename-transformer (⊢ f- : (C→ ty ... ty_out)))) - (ro:define f- (stlc:λ ([x : ty] ...) (ann (begin e ...) : ty_out))))]]) + (define-syntax- f + (make-rename-transformer (⊢ f- : (C→ ty ... ty_out)))) + (ro:define f- + (stlc:λ ([x : ty] ...) (ann (begin e ...) : ty_out))))]]) ;; --------------------------------- ;; quote diff --git a/turnstile/examples/stlc+box.rkt b/turnstile/examples/stlc+box.rkt index 5330372..fad688b 100644 --- a/turnstile/examples/stlc+box.rkt +++ b/turnstile/examples/stlc+box.rkt @@ -9,6 +9,8 @@ ;; - terms from stlc+cons.rkt ;; - ref deref := +(provide Ref ref deref :=) + (define-type-constructor Ref) (define-typed-syntax (ref e) ≫ diff --git a/turnstile/examples/stlc+cons.rkt b/turnstile/examples/stlc+cons.rkt index a60cd78..10ee58e 100644 --- a/turnstile/examples/stlc+cons.rkt +++ b/turnstile/examples/stlc+cons.rkt @@ -10,6 +10,10 @@ ;; TODO: enable HO use of list primitives +(provide (type-out List) + nil isnil cons list head tail + reverse length list-ref member) + (define-type-constructor List) (define-typed-syntax nil diff --git a/turnstile/examples/stlc+effect.rkt b/turnstile/examples/stlc+effect.rkt index 9b70c76..405ba84 100644 --- a/turnstile/examples/stlc+effect.rkt +++ b/turnstile/examples/stlc+effect.rkt @@ -1,5 +1,5 @@ #lang turnstile/lang -(extends "stlc+box.rkt" #:except ref Ref ~Ref ~Ref* Ref? deref := #%app λ) +(extends "stlc+box.rkt" #:except Ref ref deref := #%app λ) ;; Simply-Typed Lambda Calculus, plus mutable references ;; Types: @@ -9,6 +9,8 @@ ;; - terms from stlc+cons.rkt ;; - ref deref := +(provide Ref #%app λ ref deref :=) + (define-syntax-rule (locs loc ...) '(loc ...)) (begin-for-syntax @@ -28,7 +30,7 @@ [else b]))) -(define-typed-syntax effect:#%app #:export-as #%app +(define-typed-syntax #%app [(_ efn e ...) ≫ [⊢ efn ≫ e_fn- (⇒ : (~→ τ_in ... τ_out) @@ -76,7 +78,7 @@ (⇒ := (~locs as ...)) (⇒ ! (~locs ds ...))] -------- - [⊢ (box- e-) + [⊢ (#%app- box- e-) (⇒ : (Ref τ)) (⇒ ν (locs #,(syntax-position stx) ns ...)) (⇒ := (locs as ...)) @@ -89,7 +91,7 @@ (⇒ := (~locs as ...)) (⇒ ! (~locs ds ...))] -------- - [⊢ (unbox- e-) + [⊢ (#%app- unbox- e-) (⇒ : ty) (⇒ ν (locs ns ...)) (⇒ := (locs as ...)) @@ -107,7 +109,7 @@ (⇒ := (~locs as2 ...)) (⇒ ! (~locs ds2 ...))] -------- - [⊢ (set-box!- e_ref- e-) + [⊢ (#%app- set-box!- e_ref- e-) (⇒ : Unit) (⇒ ν (locs ns1 ... ns2 ...)) (⇒ := (locs #,(syntax-position stx) as1 ... as2 ...)) diff --git a/turnstile/examples/stlc+lit.rkt b/turnstile/examples/stlc+lit.rkt index e058eb2..257773f 100644 --- a/turnstile/examples/stlc+lit.rkt +++ b/turnstile/examples/stlc+lit.rkt @@ -1,6 +1,5 @@ #lang turnstile/lang (extends "stlc.rkt") -(provide (typed-out [+ : (→ Int Int Int)])) ;; Simply-Typed Lambda Calculus, plus numeric literals and primitives ;; Types: @@ -11,6 +10,10 @@ ;; - numeric literals ;; - prim + +(provide (type-out Int) + (typed-out [+ : (→ Int Int Int)]) + #%datum) + (define-base-type Int) (define-typed-syntax #%datum diff --git a/turnstile/examples/stlc+rec-iso.rkt b/turnstile/examples/stlc+rec-iso.rkt index 4d98be7..ef77543 100644 --- a/turnstile/examples/stlc+rec-iso.rkt +++ b/turnstile/examples/stlc+rec-iso.rkt @@ -1,6 +1,6 @@ #lang turnstile/lang (extends "stlc+tup.rkt") -(reuse ∨ var case define-type-alias define #:from "stlc+reco+var.rkt") +(reuse ∨ var case #:from "stlc+reco+var.rkt") ;; stlc + (iso) recursive types ;; Types: @@ -12,6 +12,8 @@ ;; - also var and case from stlc+reco+var ;; - fld, unfld +(provide μ unfld fld) + (define-type-constructor μ #:bvs = 1) (define-typed-syntax (unfld τ:type-ann e) ≫ diff --git a/turnstile/examples/stlc+reco+sub.rkt b/turnstile/examples/stlc+reco+sub.rkt index 70e1cce..2a64009 100644 --- a/turnstile/examples/stlc+reco+sub.rkt +++ b/turnstile/examples/stlc+reco+sub.rkt @@ -11,6 +11,8 @@ ;; - terms from stlc+sub.rkt ;; - records and variants from stlc+reco+var +(provide #%datum) + (define-typed-syntax #%datum [(_ . n:number) ≫ -------- diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt index 3ff715f..ca86aee 100644 --- a/turnstile/examples/stlc+reco+var.rkt +++ b/turnstile/examples/stlc+reco+var.rkt @@ -1,8 +1,6 @@ #lang turnstile/lang -(extends "stlc+tup.rkt" #:except × ×? tup proj ~× ~×*) +(extends "stlc+tup.rkt" #:except × ×? tup proj ~×) (require (only-in "stlc+tup.rkt" [~× ~stlc:×])) -(provide × ∨ (for-syntax ~× ~×* ~∨ ~∨*)) - ;; Simply-Typed Lambda Calculus, plus records and variants ;; Types: @@ -13,38 +11,8 @@ ;; - terms from stlc+tup.rkt ;; - redefine tup to records ;; - sums (var) -;; TopLevel: -;; - define (values only) -;; - define-type-alias - -(provide define-type-alias) -;; Using τ.norm leads to a "not valid type" error when file is compiled -(define-syntax define-type-alias - (syntax-parser - [(define-type-alias alias:id τ:type) - #'(define-syntax alias (make-variable-like-transformer #'τ))] - [(define-type-alias (f:id x:id ...) ty) - #'(define-syntax (f stx) - (syntax-parse stx - [(_ x ...) #'ty]))])) - -(define-typed-syntax define - [(_ x:id : τ:type e:expr) ≫ - ;This wouldn't work with mutually recursive definitions - ;[⊢ [e ≫ e- ⇐ τ.norm]] - ;So expand to an ann form instead. - -------- - [≻ (begin- - (define-syntax x (make-rename-transformer (⊢ y : τ.norm))) - (define- y (ann e : τ.norm)))]] - [(_ x:id e) ≫ - [⊢ e ≫ e- ⇒ τ] - #:with y (generate-temporary #'x) - -------- - [≻ (begin- - (define-syntax x (make-rename-transformer (⊢ y : τ))) - (define- y e-))]]) +(provide (type-out × ∨) tup proj var case) ; re-define tuples as records ; dont use define-type-constructor because I want the : literal syntax diff --git a/turnstile/examples/stlc+sub.rkt b/turnstile/examples/stlc+sub.rkt index 4d24c90..83a6222 100644 --- a/turnstile/examples/stlc+sub.rkt +++ b/turnstile/examples/stlc+sub.rkt @@ -3,7 +3,6 @@ (reuse Bool String add1 #:from "ext-stlc.rkt") (require (prefix-in ext: (only-in "ext-stlc.rkt" #%datum)) (only-in "ext-stlc.rkt" current-join)) -(provide (for-syntax subs? current-sub?)) ;; Simply-Typed Lambda Calculus, plus subtyping ;; Types: @@ -20,8 +19,11 @@ ;; - also * ;; Other: sub? current-sub? -(provide (typed-out [+ : (→ Num Num Num)] - [* : (→ Num Num Num)])) +(provide (for-syntax subs? current-sub?) + (type-out Top Num Nat) + (typed-out [+ : (→ Num Num Num)] + [* : (→ Num Num Num)]) + #%datum) (define-base-types Top Num Nat) diff --git a/turnstile/examples/stlc+tup.rkt b/turnstile/examples/stlc+tup.rkt index c5aa8a7..34adc56 100644 --- a/turnstile/examples/stlc+tup.rkt +++ b/turnstile/examples/stlc+tup.rkt @@ -9,6 +9,8 @@ ;; - terms from ext-stlc.rkt ;; - tup and proj +(provide (type-out ×) tup proj) + (define-type-constructor × #:arity >= 0 #:arg-variances (λ (stx) (make-list (stx-length (stx-cdr stx)) covariant))) diff --git a/turnstile/examples/stlc+union+case.rkt b/turnstile/examples/stlc+union+case.rkt index 297808e..658dbdb 100644 --- a/turnstile/examples/stlc+union+case.rkt +++ b/turnstile/examples/stlc+union+case.rkt @@ -1,7 +1,5 @@ #lang turnstile/lang -(extends "stlc+union.rkt" - #:except #%app add1 sub1) -(provide case→) +(extends "stlc+union.rkt" #:except #%app add1 sub1) ;; Simply-Typed Lambda Calculus, plus union types and case-> function types ;; Types: @@ -13,19 +11,20 @@ ;; - terms from stlc+union.rkt ;; Other: updated current-sub? -(provide (typed-out [add1 : (case→ (→ Nat Nat) +(provide (type-out case->) case→ + (typed-out [add1 : (case→ (→ Nat Nat) (→ Int Int))] [sub1 : (case→ (→ Zero NegInt) (→ PosInt Nat) (→ NegInt NegInt) (→ Nat Nat) - (→ Int Int))])) + (→ Int Int))]) + #%app) (define-type-constructor case-> #:arity > 0) (define-syntax case→ (make-rename-transformer #'case->)) - -(define-typed-syntax app #:export-as #%app +(define-typed-syntax #%app [(_ e_fn e_arg ...) ≫ [⊢ [e_fn ≫ e_fn- ⇒ : (~→ ~! τ_in ... τ_out)]] #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt index ddc6f68..5a65764 100644 --- a/turnstile/examples/stlc+union.rkt +++ b/turnstile/examples/stlc+union.rkt @@ -2,7 +2,6 @@ (extends "ext-stlc.rkt" #:except #%app #%datum + add1 sub1 * Int Int? ~Int Float Float? ~Float Bool ~Bool Bool?) -(reuse define-type-alias #:from "stlc+reco+var.rkt") ;; Simply-Typed Lambda Calculus, plus union types ;; Types: @@ -20,13 +19,15 @@ ;; - also * ;; Other: sub? current-sub? -(provide Int Num Nat U Bool +(provide (for-syntax current-sub? prune+sort) define-named-type-alias - (for-syntax current-sub? prune+sort) + Int Num Nat U (type-out U*) + Zero NegInt PosInt Float Bool False True (typed-out [+ : (→ Num Num Num)] [* : (→ Num Num Num)] [add1 : (→ Int Int)] - [sub1 : (→ Int Int)])) + [sub1 : (→ Int Int)]) + #%datum #%app) (define-syntax define-named-type-alias (syntax-parser @@ -38,7 +39,6 @@ (syntax-parse stx [(_ x ...) (add-orig #'ty stx)]))])) - (define-base-types Zero NegInt PosInt Float False True) (define-type-constructor U* #:arity >= 0) @@ -71,7 +71,7 @@ (define-syntax Num (make-variable-like-transformer (add-orig #'(U Float Int) #'Num))) -(define-typed-syntax datum #:export-as #%datum +(define-typed-syntax #%datum [(_ . b:boolean) ≫ #:with ty_out (if (syntax-e #'b) #'True #'False) -------- @@ -91,7 +91,7 @@ -------- [_ ≻ (ext-stlc:#%datum . x)]]) -(define-typed-syntax app #:export-as #%app +(define-typed-syntax #%app [(_ e_fn e_arg ...) ≫ [⊢ [e_fn ≫ e_fn- ⇒ : (~→ ~! τ_in ... τ_out)]] #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) @@ -130,4 +130,3 @@ (define (join t1 t2) #`(U #,t1 #,t2)) (current-join join)) - diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt index 76ebfe6..f530616 100644 --- a/turnstile/examples/stlc.rkt +++ b/turnstile/examples/stlc.rkt @@ -1,5 +1,7 @@ #lang turnstile/lang +(provide (type-out →) λ #%app ann) + (define-type-constructor → #:arity >= 1 #:arg-variances (λ (stx) (syntax-parse stx diff --git a/turnstile/examples/sysf.rkt b/turnstile/examples/sysf.rkt index b07cf38..ba9c8d4 100644 --- a/turnstile/examples/sysf.rkt +++ b/turnstile/examples/sysf.rkt @@ -9,6 +9,8 @@ ;; - terms from stlc+lit.rkt ;; - Λ and inst +(provide (type-out ∀) Λ inst) + (define-type-constructor ∀ #:bvs >= 0) (define-typed-syntax (Λ (tv:id ...) e) ≫ diff --git a/turnstile/examples/tests/run-all-tests.rkt b/turnstile/examples/tests/run-all-tests.rkt index a6ecf70..fe602d0 100644 --- a/turnstile/examples/tests/run-all-tests.rkt +++ b/turnstile/examples/tests/run-all-tests.rkt @@ -39,5 +39,9 @@ ;; type and effects (require "stlc+effect-tests.rkt") +;; union and case types +(require "stlc+union.rkt") +(require "stlc+union+case.rkt") + ; don't run this file for testing: (module test racket/base) diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl index 8de98dc..c12e45c 100644 --- a/turnstile/scribblings/reference.scrbl +++ b/turnstile/scribblings/reference.scrbl @@ -2,7 +2,7 @@ @(require scribble/example racket/sandbox (for-label racket/base - (except-in turnstile/turnstile ⊢ stx)) + (except-in turnstile/turnstile ⊢ stx mk-~ mk-?)) "doc-utils.rkt" "common.rkt") @title{The Turnstile Reference} @@ -40,8 +40,7 @@ and then press Control-@litchar{\}. conclusion) (define-typed-syntax name-id option ... rule ...+)) #:grammar - ([option (code:line #:export-as out-name-id) - (code:line @#,racket[syntax-parse] option)] + ([option (code:line @#,racket[syntax-parse] option)] [rule [expr-pattern ≫ premise ... -------- @@ -111,20 +110,20 @@ A programmer may use the generalized form @racket[[⊢ e ≫ e- (⇒ key τ) ... Dually, one may write @racket[[⊢ e ≫ e- ⇐ τ]] to check that @racket[e] has type @racket[τ]. Here, both @racket[e] and @racket[τ] are inputs (templates) and only - @racket[e-] is an output (pattern). + @racket[e-] is an output (pattern).} -A @racket[define-typed-syntax] definition is automatically provided, either using - the given name, or with a specified @racket[#:export-as] name. -} +@defform[(define-typerule ....)]{An alias for @racket[define-typed-syntax].} -@defform*[((define-primop op-id τ) - (define-primop op-id : τ) +@defform*[((define-primop typed-op-id τ) + (define-primop typed-op-id : τ) (define-primop typed-op-id op-id τ) (define-primop typed-op-id op-id : τ))]{ Defines @racket[typed-op-id] by attaching type @racket[τ] to (untyped) -identifier @racket[op-id], e.g. @racket[(define-primop typed+ + : (→ Int Int))]. +identifier @racket[op-id], e.g.: -When not specified, @racket[typed-op-id] is @racket[op-id] suffixed with +@racketblock[(define-primop typed+ + : (→ Int Int))] + +When not specified, @racket[op-id] is @racket[typed-op-id] suffixed with @litchar{-} (see @secref{racket-}).} @defform[(define-syntax-category name-id)]{ @@ -136,14 +135,11 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn use any forms other than @racket[define-base-type] and @racket[define-type-constructor] in conjunction with @racket[define-typed-syntax]. The other forms are considered "low-level" and are automatically used by @racket[define-typed-syntax]. @itemlist[ - @item{@defform[(define-base-type base-type-name-id option ...) - #:grammar - ([option (code:line #:no-provide)])]{ + @item{@defform[(define-base-type base-type-name-id)]{ Defines a base type. A @racket[(define-base-type τ)] additionally defines: @itemlist[@item{@racket[τ], an identifier macro representing type @racket[τ].} @item{@racket[τ?], a predicate recognizing type @racket[τ].} - @item{@racket[~τ], a @tech:pat-expander recognizing type @racket[τ].}] - Automatically provides the defined type unless @racket[#:no-provide] is specified.}} + @item{@racket[~τ], a @tech:pat-expander recognizing type @racket[τ].}]}} @item{@defform[(define-base-types base-type-name-id ...)]{Defines multiple base types.}} @item{ @defform[(define-type-constructor name-id option ...) @@ -152,8 +148,7 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn (code:line #:bvs op n) (code:line #:arr tycon) (code:line #:arg-variances expr) - (code:line #:extra-info stx) - (code:line #:no-provide)])]{ + (code:line #:extra-info stx)])]{ Defines a type constructor. Defining a type constructor @racket[τ] defines: @itemlist[@item{@racket[τ], a macro for constructing an instance of type @racket[τ], with the specified arity.} @@ -169,22 +164,23 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn shape @racket[(∀ (X) τ)], where @racket[τ] may reference @racket[X]. The @racket[#:extra-info] argument is useful for attaching additional metainformation - to types, for example to implement pattern matching. - - Automatically provides the defined type, unless @racket[#:no-provide] is specified. - }} + to types, for example to implement pattern matching.}} +@item{ +@defform[(type-out ty-id)]{ +A provide spec that, given @racket[ty-id], provides @racket[ty-id], +a predicate @racket[ty-id?], and a @tech:pat-expander @racket[~ty-id].}} @item{@defproc[(type=? [τ1 type?] [τ2 type?]) boolean?]{A phase 1 equality predicate for types that computes structural, @racket[free-identifier=?] equality, but includes alpha-equivalence. @examples[#:eval the-eval -(define-base-type Int #:no-provide) -(define-base-type String #:no-provide) +(define-base-type Int) +(define-base-type String) (begin-for-syntax (displayln (type=? #'Int #'Int))) (begin-for-syntax (displayln (type=? #'Int #'String))) -(define-type-constructor → #:arity > 0 #:no-provide) -(define-type-constructor ∀ #:arity = 1 #:bvs = 1 #:no-provide) +(define-type-constructor → #:arity > 0) +(define-type-constructor ∀ #:arity = 1 #:bvs = 1) (begin-for-syntax (displayln (type=? ((current-type-eval) #'(∀ (X) X)) @@ -265,7 +261,7 @@ Reuses @racket[name]s from @racket[base-lang].} To help avoid name conflicts, Turnstile re-provides all Racket bindings with a @litchar{-} suffix. These bindings are automatically used in some cases, e.g., -@racket[define-primop]. +@racket[define-primop], but in general are useful for avoiding name conflicts.. @section{Lower-level Functions} diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt index 52c0992..312d338 100644 --- a/turnstile/turnstile.rkt +++ b/turnstile/turnstile.rkt @@ -57,7 +57,8 @@ (module syntax-classes racket/base (provide (all-defined-out)) (require (for-meta 0 (submod ".." typecheck+)) - (for-meta -1 (submod ".." typecheck+) (except-in macrotypes/typecheck #%module-begin)) + (for-meta -1 (submod ".." typecheck+) + (except-in macrotypes/typecheck #%module-begin mk-~ mk-?)) (for-meta -2 (except-in macrotypes/typecheck #%module-begin))) (define-syntax-class --- [pattern dashes:id