suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

progress commit: stuck on fomega+define-syntax-category

Browse Source
This commit is contained in:
Stephen Chang 2015-08-21 19:28:36 -04:00
parent 336b6ea1f3
commit efaef8b60e
18 changed files with 668 additions and 761 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
tapl/exist.rkt
View File

@ -17,63 +17,21 @@
;; - terms from stlc+reco+var.rkt
;; - pack and open
#;(begin-for-syntax
(define (type=? t1 t2)
(or (stlc:type=? t1 t2)
(sysf:type=? t1 t2)))
(current-type=? type=?)
(current-typecheck-relation type=?))
#;(define-type-constructor (∃ [[X]] τ_body))
(define-basic-checked-stx ∃ #:arity = 1 #:bvs = 1)
; this is exactly the same as μ
;(define-syntax ∃
; (syntax-parser
; [(_ (tv:id) τ_body)
; #:with ((tv-) τ_body- k) (infer/ctx+erase #'([tv : #%type]) #'τ_body)
; #:when (#%type? #'k)
; (mk-type #'(λ (tv-) τ_body-))]))
;(begin-for-syntax
; #;(define (infer∃+erase e)
; (syntax-parse (infer+erase e) #:context e
; [(e- τ_e)
; #:with ((~literal #%plain-lambda) (tv) τ) #'τ_e
; #'(e- (tv τ))]))
; (define-syntax ~∃
; (pattern-expander
; (syntax-parser
; [(_ (tv:id) τ)
; #'((~literal #%plain-lambda) (tv) τ)])))
; (define-syntax ~∃*
; (pattern-expander
; (syntax-parser
; [(_ (tv:id) τ)
; #'(~or (~∃ (tv) τ)
; (~and any (~do
; (type-error
; #:src #'any
; #:msg "Expected ∃ type, got: ~a" #'any))))]))))
(define-type-constructor ∃ #:arity = 1 #:bvs = 1)
(define-syntax (pack stx)
(syntax-parse stx
[(_ (τ:type e) as ∃τ:type)
#:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
; #:with (#%plain-lambda (τ_abstract:id) τ_body) #'∃τ.norm
#:with [e- τ_e] (infer+erase #'e)
#:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body))
(⊢ e- : ∃τ)]))
(⊢ e- : ∃τ.norm)]))
(define-syntax (open stx)
(syntax-parse stx #:datum-literals (<=)
[(_ ([(tv:id x:id) <= e_packed]) e)
; #:with [e_packed- τ_packed] (infer+erase #'e_packed)
; #:when (displayln #'τ_packed)
; #:with (~∃ (τ_abstract) τ_body) #'τ_packed
#:with [e_packed- ((τ_abstract) (τ_body))] (⇑ e_packed as ∃)
; #:with [e_packed- (τ_abstract τ_body)] (infer∃+erase #'e_packed)
; #:with [e_packed- τ_packed] (infer+erase #'e_packed)
; #:with (#%plain-lambda (τ_abstract:id) τ_body) #'τ_packed ; existential
;; 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.

6
tapl/ext-stlc.rkt
View File

@ -129,10 +129,10 @@
(define-syntax (letrec/tc stx)
(syntax-parse stx
[(_ ([b:typed-binding e] ...) e_body)
[(_ ([b:type-bind e] ...) e_body)
#:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
(infers/type-ctxt+erase #'(b ...) #'(e ... e_body))
#:fail-unless (typechecks? #'(b.τ ...) #'(τ ...))
#:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
(string-append
"type check fail, args have wrong type:\n"
(string-join
@ -141,7 +141,7 @@
(format
"~a has type ~a, expected ~a"
(syntax->datum e) (type->str τ) (type->str τ-expect)))
#'(e ...) #'(τ ...) #'(b.τ ...))
#'(e ...) #'(τ ...) #'(b.type ...))
"\n"))
(⊢ (letrec ([x- e-] ...) e_body-) : τ_body)]))

135
tapl/fomega.rkt
View File

@ -1,17 +1,17 @@
#lang racket/base
(require "typecheck.rkt")
(require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀ + type-eval)
(prefix-in sysf: (only-in "sysf.rkt" type-eval))
(only-in "stlc+reco+var.rkt" same-types?))
(provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
(require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀ type-eval type=?)
(rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ type-eval ∀ ~∀ type=?))
[sysf:~∀ ~sysf:∀])
(only-in "stlc+reco+var.rkt" String #%datum same-types?))
(provide (rename-out [sysf:#%app #%app] [sysf:λ λ] #;[app/tc #%app] #;[λ/tc λ] #;[datum/tc #%datum]))
#;(provide (except-out (all-from-out "sysf.rkt")
sysf:Int sysf:→ sysf:∀
sysf:#%app sysf:λ
(for-syntax sysf:type-eval)))
(provide (except-out (all-from-out "sysf.rkt") (for-syntax sysf:type-eval))
sysf:∀ sysf:#%app sysf:λ
(for-syntax sysf:type-eval sysf:type=?)))
(provide (except-out (all-from-out "sysf.rkt") (for-syntax sysf:type-eval sysf:type=?))
(all-from-out "stlc+reco+var.rkt"))
(provide Int → ∀ inst Λ tyλ tyapp
(for-syntax type-eval))
(provide ∀ inst Λ tyλ tyapp
(for-syntax type-eval type=?))
;; System F_omega
;; Type relation:
@ -21,9 +21,11 @@
;; - terms from sysf.rkt
(define-syntax-category kind)
(begin-for-syntax
(current-type? (λ (t) (or (type? t) (kind? (typeof t))))))
(provide define-type-alias)
(define-syntax define-type-alias
#;(provide define-type-alias)
#;(define-syntax define-type-alias
(syntax-parser
[(_ alias:id τ)
#:with (τ- k_τ) (infer+erase #'τ)
@ -31,6 +33,18 @@
#'(define-syntax alias (syntax-parser [x:id #'τ-]))]))
(begin-for-syntax
(define (type=? t1 t2)
(printf "t1 = ~a\n" (syntax->datum t1))
(printf "t2 = ~a\n" (syntax->datum t2))
(and (syntax-parse (list t1 t2) #:datum-literals (:)
[((~∀ ([tv1 : k1] ...) tbody1)
(~∀ ([tv2 : k2] ...) tbody2))
#:when (displayln "here")
(types=? #'(k1 ...) #'(k2 ...))]
[_ #t])
(sysf:type=? t1 t2)))
(current-type=? type=?)
(current-typecheck-relation (current-type=?))
;; extend type-eval to handle tyapp
;; - requires manually handling all other forms
(define (type-eval τ)
@ -52,13 +66,12 @@
[((~literal #%plain-app) arg ...)
#:with (arg+ ...) (stx-map (current-type-eval) #'(arg ...))
(syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
[(~or x:id ((~literal tyλ) . _)) ; dont eval under tyλ
[_ #;(~or x:id ((~literal tyλ) . _)) ; dont eval under tyλ
(sysf:type-eval τ)]))
(current-type-eval type-eval))
(define-basic-checked-id-stx ★ : #%kind)
(define-basic-checked-stx ⇒ : #%kind #:arity >= 1)
;(define-type-constructor (⇒ k_in ... k_out))
(define-base-kind ★)
(define-kind-constructor ⇒ #:arity >= 1)
;; for now, handle kind checking in the types themselves
;; TODO: move kind checking to a common place (like #%app)?
@ -66,15 +79,15 @@
;; TODO: need some kind of "promote" abstraction,
;; so I dont have to manually add kinds to all types
(define-basic-checked-id-stx String : ★)
(define-basic-checked-id-stx Int : ★)
#;(define-basic-checked-id-stx String : ★)
#;(define-basic-checked-id-stx Int : ★)
;(define-base-type Str)
;(provide String)
;(define-syntax String (syntax-parser [x:id (⊢ Str : ★)]))
;(define-syntax Int (syntax-parser [x:id (⊢ sysf:Int : ★)]))
;; → in Fω is not first-class, can't pass it around
(define-basic-checked-stx → : ★ #:arity >= 1)
#;(define-basic-checked-stx → : ★ #:arity >= 1)
#;(define-syntax (→ stx)
(syntax-parse stx
[(_ τ ... τ_res)
@ -83,19 +96,57 @@
#:when (same-types? #'(k ... k_res))
(⊢ (sysf:→ (#%plain-type τ-) ... (#%plain-type τ_res-)) : ★)]))
(define-syntax (∀ stx)
#;(define-syntax (∀ stx)
(syntax-parse stx
[(_ (b:kinded-binding ...) τ_body)
#:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
#:when (★? #'k_body)
(⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
(define-syntax (∀ stx)
(syntax-parse stx
[(_ bvs:kind-ctx τ_body)
; #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body)
; #:when (★? #'k_body)
#:when (displayln ((current-type-eval) #'(sysf:∀ (bvs.x ...) τ_body)))
(⊢ #,((current-type-eval) #'(sysf:∀ (bvs.x ...) τ_body)) : (⇒ bvs.kind ...))]))
; (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
(begin-for-syntax
(define-syntax ~∀
(pattern-expander
(syntax-parser #:datum-literals (:)
[(_ ([tv:id : k] ...) τ)
#:when (displayln "pat expand")
#:with ∀τ (generate-temporary)
#'(~and ∀τ
(~parse (~sysf:∀ (tv ...) τ) #'∀τ)
(~parse (~⇒ k ...) (typeof #'∀τ)))]
[(_ . args)
#'(~and ∀τ
(~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ)
(~parse (~⇒ k (... ...)) (typeof #'∀τ))
(~parse args #'(([tv k] (... ...)) τ)))])))
(define-syntax ~∀*
(pattern-expander
(syntax-parser #:datum-literals (<:)
[(_ . args)
#'(~or
(~∀ . args)
(~and any (~do
(type-error
#:src #'any
#:msg "Expected ∀ type, got: ~a" #'any))))]))))
(define-syntax (Λ stx)
#;(define-syntax (Λ stx)
(syntax-parse stx
[(_ (b:kinded-binding ...) e)
#:with ((tv- ...) e- τ_e) (infer/ctx+erase #'(b ...) #'e)
(⊢ e- : (∀ ([tv- : b.tag] ...) τ_e))]))
(define-syntax (inst stx)
(define-syntax (Λ stx)
(syntax-parse stx
[(_ bvs:kind-ctx e)
#:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e)
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]))
#;(define-syntax (inst stx)
(syntax-parse stx
[(_ e τ ...)
#:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
@ -109,15 +160,47 @@
#:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
#:when (typechecks? #'(k_τ ...) #'(k_tv ...))
(⊢ e- : #,(substs #'(τ ...) #'(tv ...) #'τ_body))]))
(define-syntax (inst stx)
(syntax-parse stx
[(_ e τ:type ...)
#:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
#:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
#:when (typechecks? (stx-map typeof #'(k_τ ...)) #'(k ...))
(⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]))
;; TODO: merge with regular λ and app?
(define-syntax (tyλ stx)
(syntax-parse stx
[(_ bvs:kind-ctx τ_body)
#:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
(⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))]))
#;(define-syntax (tyλ stx)
(syntax-parse stx
[(_ (b:kinded-binding ...) τ_body)
#:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
(⊢ (λ tvs- τ_body-) : (⇒ b.tag ... k_body))]))
(define-syntax (tyapp stx)
(syntax-parse stx
[(_ τ_fn τ_arg ...)
#:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
#:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:expand (current-type-eval))
#: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))
"or wrong number of arguments:\nGiven:\n"
(string-join
(map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
(syntax->datum #'(τ_arg ...))
(stx-map type->str #'(k_arg ...)))
"\n" #:after-last "\n")
(format "Expected: ~a arguments with type(s): "
(stx-length #'(k_in ...)))
(string-join (stx-map type->str #'(k_in ...)) ", "))
(⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
#;(define-syntax (tyapp stx)
(syntax-parse stx
[(_ τ_fn τ_arg ...)
#:with [τ_fn- (~⇒* k_in ... k_out)] (infer+erase #'τ_fn)
@ -176,9 +259,9 @@
;; must override #%app and λ and primops to use new →
;; TODO: parameterize →?
(define-primop + : (→ Int Int Int) : ★)
#;(define-primop + : (→ Int Int Int) : ★)
(define-syntax (λ/tc stx)
#;(define-syntax (λ/tc stx)
(syntax-parse stx #:datum-literals (:)
[(_ ([x : τ] ...) e)
;#:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(τ ...)))
@ -187,7 +270,7 @@
#:with (xs- e- τ_res) (infer/type-ctxt+erase #'([x : τ] ...) #'e)
(⊢ (λ xs- e-) : (→ τ ... τ_res))]))
(define-syntax (app/tc stx)
#;(define-syntax (app/tc stx)
(syntax-parse stx
[(_ e_fn e_arg ...)
#:with [e_fn- (~→* τ_in ... τ_out)] (infer+erase #'e_fn)
@ -244,7 +327,7 @@
; (⊢ (#%app e_fn- e_arg- ...) : τ_res)]))
;; must override #%datum to use new kinded-Int, etc
(define-syntax (datum/tc stx)
#;(define-syntax (datum/tc stx)
(syntax-parse stx
[(_ . n:integer) (⊢ (#%datum . n) : Int)]
[(_ . s:str) (⊢ (#%datum . s) : String)]

93
tapl/fsub.rkt
View File

@ -1,17 +1,15 @@
#lang racket/base
(require "typecheck.rkt")
(require ;(except-in "sysf.rkt" #%app λ + #%datum ∀ Λ inst type=?)
;(prefix-in sysf: (only-in "sysf.rkt" #%app λ))
(except-in "stlc+reco+sub.rkt" #%app λ + type=? #;sub?)
(prefix-in stlc: (only-in "stlc+reco+sub.rkt" #%app λ #;type=? sub?))
(only-in "stlc+rec-iso.rkt" type=?)) ; type=? for binding forms
(require (except-in "stlc+reco+sub.rkt" #%app λ + type=?)
(prefix-in stlc: (only-in "stlc+reco+sub.rkt" #%app λ sub?))
(only-in "sysf.rkt" ∀? type=?)
(prefix-in sysf: (only-in "sysf.rkt" ∀ #;type=?))
(rename-in (only-in "sysf.rkt" ~∀) [~∀ ~sysf:∀]))
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]) (for-syntax sub?))
(provide (except-out (all-from-out "stlc+reco+sub.rkt")
stlc:#%app stlc:λ (for-syntax stlc:sub?))
(all-from-out "stlc+rec-iso.rkt")
#;(except-out (all-from-out "stlc+reco+sub.rkt")
(for-syntax #;stlc+reco+sub:type=? stlc+reco+sub:sub?)))
(provide ∀ Λ inst)
(except-out (all-from-out "sysf.rkt") sysf:∀ (for-syntax #;sysf:type=? ~sysf:∀)))
(provide ∀ Λ inst (for-syntax #;type=?))
;; System F<:
;; Types:
@ -33,67 +31,54 @@
(if sub (expose sub) t)]
[else t]))
(current-promote expose)
#;(define (type=? t1 t2)
(displayln (typeof t1))
(displayln (typeof t2))
(and (sysf:type=? t1 t2)
(sysf:type=? (typeof t1) (typeof t2))))
#;(current-type=? type=?)
; need this, to lift base-types; is there another way to do this?
(define (sub? t1 t2)
(stlc:sub? (expose t1) (expose t2)))
(stlc:sub? ((current-promote) t1) t2))
(current-sub? sub?)
;; extend to handle new ∀
#;(define (type=? τ1 τ2)
(syntax-parse (list τ1 τ2)
[(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
((~literal #%plain-lambda) (y:id ...) k2 ... t2))
#:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
#:when (= (stx-length #'(x ...)) (stx-length #'(k1 ...)))
((current-type=?) (substs #'(k1 ...) #'(x ...) #'t1)
(substs #'(k2 ...) #'(y ...) #'t2))]
[_ (or (sysf:type=? τ1 τ2) (stlc+reco+sub:type=? τ1 τ2))]))
#;(current-type=? type=?)
(current-typecheck-relation (current-sub?)))
(define-type-constructor <: #:arity >= 0) ; quasi-kind, but must be type constructor because its arguments are types
(begin-for-syntax
(current-type? (λ (t) (or (type? t) (<:? (typeof t))))))
;; Type annotations used in two places:
;; 1) typechecking the body of
;; 2) instantiation of ∀
;; Problem: need type annotations, even in expanded form
#;(define-syntax (∀ stx)
(syntax-parse stx #:datum-literals (<:)
[(_ ([X:id <: τ] ...) ~! body)
(syntax/loc stx (#%plain-lambda (X ...) τ ... body))]
#;[(_ x ...) #'(sysf:∀ x ...)]))
(define ∀-internal void)
;(define ∀-internal void)
(define-syntax ∀
(syntax-parser #:datum-literals (<:)
[(_ ([tv:id <: τ:type] ...) τ_body)
#:with ((tv- ...) τ_body- k) (infer/ctx+erase #'([tv : #%type] ...) #'τ_body)
#:when (#%type? #'k)
(mk-type #'(λ (tv- ...) (∀-internal τ.norm ... τ_body-)))]))
;#:with ((tv- ...) τ_body- k) (infer/ctx+erase #'([tv : #%type] ...) #'τ_body)
;#:when (#%type? #'k)
;(mk-type #'(λ (tv- ...) (∀-internal τ.norm ... τ_body-)))]))
; eval first to overwrite the old #%type
(⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) : (<: τ.norm ...))]))
(begin-for-syntax
#;(define (infer∀+erase e)
(syntax-parse (infer+erase e) #:context e
[(e- τ_e)
#:with ((~literal #%plain-lambda) (tv ...) τ_sub ... τ_body) #'τ_e
#'(e- (([tv τ_sub] ...) τ_body))]))
(define (∀? t)
(syntax-parse t
[((~literal #%plain-lambda) tvs ((~literal #%plain-app) (~literal ∀-internal) . args))
#t]
[_ #f]))
(define-syntax ~∀
(pattern-expander
(syntax-parser #:datum-literals (<:)
[(_ ([tv:id <: τ_sub] ...) τ)
#'((~literal #%plain-lambda) (tv ...)
((~literal #%plain-app) (~literal ∀-internal) τ_sub ... τ))]
#'(~and ∀τ
(~parse (~sysf:∀ (tv ...) τ) #'∀τ)
(~parse (~<: τ_sub ...) (typeof #'∀τ)))]
[(_ . args)
#'(~and ((~literal #%plain-lambda) (tv (... ...))
((~literal #%plain-app) (~literal ∀-internal) τ_sub (... ...) τ))
#'(~and ∀τ
(~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ)
(~parse (~<: τ_sub (... ...)) (typeof #'∀τ))
(~parse args #'(([tv τ_sub] (... ...)) τ)))])))
(define-syntax ~∀*
(pattern-expander
(syntax-parser #:datum-literals (<:)
[(_ . args) ; (_ ([tv:id <: τ_sub] ...) τ)
[(_ . args)
#'(~or
(~∀ . args)
;((~literal #%plain-lambda) (tv ...) τ_sub ... τ)
(~and any (~do
(type-error
#:src #'any
@ -106,21 +91,13 @@
;; "environment", ie, a syntax property with another tag: 'sub
;; The "expose" function looks for this tag to enforce the bound,
;; as in TaPL (fig 28-1)
#:with ((tv- ...) _ (e-) (τ)) (infer #'(e) #:tvctx #'([tv : #%type] ...)
#:octx #'([tv : τsub] ...) #:tag 'sub)
(⊢ e- : (∀ ([tv- <: τsub] ...) τ))]
#;[(_ x ...) #'(sysf:Λ x ...)]))
#:with ((tv- ...) _ (e-) (τ_e)) (infer #'(e) #:tvctx #'([tv : #%type] ...)
#:octx #'([tv : τsub] ...) #:tag 'sub)
(⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))]))
(define-syntax (inst stx)
(syntax-parse stx
[(_ e τ:type ...)
;#:with (e- (([tv τ_sub] ...) τ_body)) (infer∀+erase #'e)
#:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀)
; #:with (e- ∀τ) (infer+erase #'e)
; #:with ((~literal #%plain-lambda) (tv:id ...) τ_sub ... τ_body) #'∀τ
#:when (typechecks? #'(τ.norm ...) #'(τ_sub ...))
(⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]
#;[(_ e τ:type ...) ; need to ensure no types (ie bounds) in lam (ie expanded ∀) body
#:with (e- ∀τ) (infer+erase #'e)
#:with ((~literal #%plain-lambda) (tv:id ...) τ_body) #'∀τ
#'(sysf:inst e τ ...)]))
(⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))

7
tapl/stlc+box.rkt
View File

@ -13,8 +13,7 @@
;; Terms:
;; - terms from stlc+cons.rkt
;(define-type-constructor (Ref τ) #:declare τ type)
(define-basic-checked-stx Ref #:arity = 1)
(define-type-constructor Ref #:arity = 1)
(define-syntax (ref stx)
(syntax-parse stx
@ -24,16 +23,12 @@
(define-syntax (deref stx)
(syntax-parse stx
[(_ e)
; #:with (e- (~Ref* τ)) (infer+erase #'e) ; alternate pattern; worse err msg
; #:with (e- (τ)) (inferRef+erase #'e)
#:with (e- (τ)) (⇑ e as Ref)
(⊢ (unbox e-) : τ)]))
(define-syntax (:= stx)
(syntax-parse stx
[(_ e_ref e)
; #:with (e_ref- (τ1)) (inferRef+erase #'e_ref)
#:with (e_ref- (τ1)) (⇑ e_ref as Ref)
; #:with (e_ref- (~Ref* τ1)) (infer+erase #'e_ref) ; alt pattern; worse err msg
#:with (e- τ2) (infer+erase #'e)
#:when (typecheck? #'τ1 #'τ2)
(⊢ (set-box! e_ref- e-) : Unit)]))

16
tapl/stlc+cons.rkt
View File

@ -15,13 +15,12 @@
;; TODO: enable HO use of list primitives
;(define-type-constructor (List τ) #:declare τ type)
(define-basic-checked-stx List #:arity = 1)
(define-type-constructor List #:arity = 1)
(define-syntax (nil stx)
(syntax-parse stx
[(_ ~! τi:ann)
(⊢ null : (List τi.τ))]
[(_ ~! τi:type-ann)
(⊢ null : (List τi.norm))]
[null:id
#:fail-when #t (error 'nil "requires type annotation")
#'null]))
@ -29,27 +28,18 @@
(syntax-parse stx
[(_ e1 e2)
#:with (e1- τ1) (infer+erase #'e1)
; #:with (e2- (τ2)) (inferList+erase #'e2)
#:with (e2- (τ2)) (⇑ e2 as List)
; #:with (e2- τ-lst) (infer+erase #'e2)
; #:with τ2 (List-get τ from τ-lst)
#:when (typecheck? #'τ1 #'τ2)
(⊢ (cons e1- e2-) : (List τ1))]))
(define-syntax (isnil stx)
(syntax-parse stx
[(_ e)
; #:with (e- _) (inferList+erase #'e)
#:with (e- _) (⇑ e as List)
; #:with (e- τ-lst) (infer+erase #'e)
; #:fail-unless (List? #'τ-lst) "expected argument of List type"
(⊢ (null? e-) : Bool)]))
(define-syntax (head stx)
(syntax-parse stx
[(_ e)
; #:with (e- (τ)) (inferList+erase #'e)
#:with (e- (τ)) (⇑ e as List)
; #:with (e- τ-lst) (infer+erase #'e)
; #:with τ (List-get τ from τ-lst)
(⊢ (car e-) : τ)]))
(define-syntax (tail stx)
(syntax-parse stx

23
tapl/stlc+lit.rkt
View File

@ -1,9 +1,10 @@
#lang racket/base
(require "typecheck.rkt")
(extends "stlc.rkt" #:impl-uses (→))
;(require "stlc.rkt")
;(provide (all-from-out "stlc.rkt"))
(provide (rename-out [datum/tc #%datum]))
;(extends "stlc.rkt" #:impl-uses (→))
(require (except-in "stlc.rkt" #%app)
(prefix-in stlc: (only-in "stlc.rkt" #%app)))
(provide (except-out (all-from-out "stlc.rkt") stlc:#%app))
(provide (rename-out [stlc:#%app #%app] [datum/tc #%datum]) define-primop)
;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
;; Types:
@ -16,7 +17,19 @@
(define-base-type Int)
;(define-base-type Int)
(define-syntax define-primop
(syntax-parser #:datum-literals (:)
[(_ op:id : τ:type)
#:with op/tc (generate-temporary #'op)
#'(begin
(provide (rename-out [op/tc op]))
(define-syntax (op/tc stx)
(syntax-parse stx
[f:id (⊢ #,(syntax/loc stx op) : τ)] ; HO case
[(o . rst)
#:with app (datum->syntax #'o '#%app)
#:with opp (format-id #'o "~a" #'op)
(syntax/loc stx (app opp . rst))])))]))
(define-primop + : (→ Int Int Int))

31
tapl/stlc+rec-iso.rkt
View File

@ -17,29 +17,10 @@
;; - terms from stlc+reco+var.rkt
;; - fld/unfld
(define-basic-checked-stx μ #:arity = 1 #:bvs = 1)
#;(define-type-constructor
(μ [[tv]] τ_body))
#;(define-syntax μ
(syntax-parser
[(_ (tv:id) τ_body)
#:with ((tv-) τ_body- k) (infer/ctx+erase #'([tv : #%type]) #'τ_body)
#:when (#%type? #'k)
(mk-type #'(λ (tv-) τ_body-))]))
#;(begin-for-syntax
(define-syntax ~μ*
(pattern-expander
(syntax-parser
[(_ (tv:id) τ)
#'(~or
((~literal #%plain-lambda) (tv) τ)
(~and any (~do
(type-error
#:src #'any
#:msg "Expected μ type, got: ~a" #'any))))]))))
(define-type-constructor μ #:arity = 1 #:bvs = 1)
(begin-for-syntax
;; extend to handle μ
;; extend to handle μ, ie lambdas
(define (type=? τ1 τ2)
; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
@ -56,17 +37,15 @@
(define-syntax (unfld stx)
(syntax-parse stx
[(_ τ:ann e)
[(_ τ:type-ann e)
#:with (~μ* (tv) τ_body) #'τ.norm
; #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm
#:with [e- τ_e] (infer+erase #'e)
#:when (typecheck? #'τ_e #'τ.norm)
(⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))]))
(define-syntax (fld stx)
(syntax-parse stx
[(_ τ:ann e)
[(_ τ:type-ann e)
#:with (~μ* (tv) τ_body) #'τ.norm
; #:with ((~literal #%plain-type) ((~literal #%plain-lambda) (tv:id) τ_body)) #'τ.norm
#:with [e- τ_e] (infer+erase #'e)
#:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body))
(⊢ e- : τ.τ)]))
(⊢ e- : τ.norm)]))

99
tapl/stlc+reco+var.rkt
View File

@ -29,18 +29,6 @@
;; - define (values only)
(begin-for-syntax
; extend to:
; 1) accept strings (ie, record labels)
#;(define (type=? τ1 τ2)
; (printf "t1 = ~a\n" (syntax->datum τ1))
; (printf "t2 = ~a\n" (syntax->datum τ2))
(syntax-parse (list τ1 τ2)
[(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
[_ (stlc:type=? τ1 τ2)]))
;(current-type=? type=?)
;(current-typecheck-relation (current-type=?))
(define (same-types? τs)
(define τs-lst (syntax->list τs))
(or (null? τs-lst)
@ -51,23 +39,16 @@
(syntax-parser
[(_ alias:id τ:type)
; must eval, otherwise undefined types will be allowed
;#'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
#'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
;(define-type-constructor [: str τ] #:lits (:))
; re-define tuples as records
; dont use define-type-constructor because I want the : literal syntax
(define-syntax ×
(syntax-parser #:datum-literals (:)
[(_ [label:id : τ:type] ...)
#:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
#`(stlc:× valid-τ ...)]))
(begin-for-syntax
#;(define (infer×+erase e)
(syntax-parse (stlc:infer×+erase e) #:context e
[(e- τ_e)
#:with (((~literal #%plain-app) (quote l) τ) ...) #'τ_e
#'(e- ((l τ) ...))]))
(define-syntax ~×
(pattern-expander
(syntax-parser #:datum-literals (:)
@ -86,38 +67,20 @@
#:src #'any
#:msg "Expected × type, got: ~a" #'any))))]))))
#;(define-type-constructor
;(× [~× label τ_fld] ...) #:lits (~×)
(× [: label τ_fld] ...) #:lits (:)
#:declare label str
#:declare τ_fld type
)
; (× τ ...)
; #:declare τ type)
;; records
(define-syntax (tup stx)
(syntax-parse stx #:datum-literals (=)
[(_ [l:id = e] ...)
#:with ([e- τ] ...) (infers+erase #'(e ...))
;(⊢ (list (list l e-) ...) : (× [~× l τ] ...))]
(⊢ (list (list 'l e-) ...) : (× [l : τ] ...))]
#;[(_ e ...)
#'(stlc:tup e ...)]))
(⊢ (list (list 'l e-) ...) : (× [l : τ] ...))]))
(define-syntax (proj stx)
(syntax-parse stx #:literals (quote)
[(_ e_rec l:id)
; #:with (e_rec- (~×* [: 'l_τ τ] ...)) (infer+erase #'e_rec)
; #:with (e_rec- ([l_τ τ] ...)) (infer×+erase #'e_rec)
#:with (e_rec- ([l_τ τ] ...)) (⇑ e_rec as ×)
; #:with [rec- τ_rec] (infer+erase #'e_rec) ; match method #2: get
; #:with ('l_τ:str ...) (×-get label from τ_rec)
; #:with (τ ...) (×-get τ_fld from τ_rec)
#:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
(⊢ (cadr (assoc 'l e_rec-)) : τ_match)]
#;[(_ e ...) #'(stlc:proj e ...)]))
(⊢ (cadr (assoc 'l e_rec-)) : τ_match)]))
(define-basic-checked-stx ∨/internal)
(define-type-constructor ∨/internal)
; re-define tuples as records
(define-syntax ∨
@ -132,16 +95,6 @@
"Improper usage of type constructor ∨: ~a, expected (∨ [label:id : τ:type] ...+)")
#'any)]))
(begin-for-syntax
#;(define (infer∨+erase e)
(syntax-parse (infer+erase e) #:context e
[(e- τ_e)
#:fail-unless (∨/internal? #'τ_e)
(format
"~a (~a:~a): Expected expression ~a to have ∨ type, got: ~a"
(syntax-source e) (syntax-line e) (syntax-column e)
(syntax->datum e) (type->str #'τ_e))
#:with (~∨/internal ((~literal #%plain-app) (quote l) τ) ...) #'τ_e
#'(e- ((l τ) ...))]))
(define ∨? ∨/internal?)
(define-syntax ~∨
(pattern-expander
@ -161,22 +114,10 @@
#:msg "Expected ∨ type, got: ~a" #'any))))
~!)])))) ; dont backtrack here
#;(define-type-constructor
(∨ [<> label τ_var] ...) #:lits (<>)
#:declare label str
#:declare τ_var type)
(define-syntax (var stx)
(syntax-parse stx #:datum-literals (as =)
[(_ l:id = e as τ:type)
; #:when (∨? #'τ.norm)
; #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm))
; #:when (displayln #'τ)
; #:when (displayln #'τ.norm)
; #:when (displayln (type->str #'τ.norm))
#:with (~∨* [l_τ : τ_l] ...) #'τ.norm
; #:with ('l_τ:str ...) (∨-get label from τ)
; #:with (τ_l ...) (∨-get τ_var from τ)
#:with match_res (stx-assoc #'l #'((l_τ τ_l) ...))
#:fail-unless (syntax-e #'match_res)
(format "~a field does not exist" (syntax->datum #'l))
@ -188,11 +129,7 @@
(syntax-parse stx #:datum-literals (of =>)
[(_ e [l:id x:id => e_l] ...)
#:fail-when (null? (syntax->list #'(l ...))) "no clauses"
; #:with (e- (~∨* [<> 'l_x τ_x] ...)) (infer+erase #'e)
;#:with (e- ([l_x τ_x] ...)) (infer∨+erase #'e)
#:with (e- ([l_x τ_x] ...)) (⇑ e as ∨)
; #:with ('l_x:str ...) (∨-get label from τ_e)
; #:with (τ_x ...) (∨-get τ_var from τ_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"
#:with (((x-) e_l- τ_el) ...)
@ -202,34 +139,6 @@
(cond [(symbol=? l_e 'l) (let ([x- (cadr e-)]) e_l-)] ...))
: #,(stx-car #'(τ_el ...)))]))
#;(define-syntax (var stx)
(syntax-parse stx #:datum-literals (as =) #:literals (quote)
[(_ l:str = e as τ:type)
; #:when (∨? #'τ.norm)
; #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm))
#:with (~∨* [<> 'l_τ τ_l] ...) #'τ.norm
; #:with ('l_τ:str ...) (∨-get label from τ)
; #:with (τ_l ...) (∨-get τ_var from τ)
#:with (l_match:str τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...))
#:with (e- τ_e) (infer+erase #'e)
#:when (typecheck? #'τ_e #'τ_match)
(⊢ (list l e) : τ)]))
#;(define-syntax (case stx)
(syntax-parse stx #:datum-literals (of =>) #:literals (quote)
[(_ e [l:str x => e_l] ...)
#:fail-when (null? (syntax->list #'(l ...))) "no clauses"
#:with (e- (~∨* [<> 'l_x τ_x] ...)) (infer+erase #'e)
; #:with ('l_x:str ...) (∨-get label from τ_e)
; #:with (τ_x ...) (∨-get τ_var from τ_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"
#:with (((x-) e_l- τ_el) ...)
(stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
#:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
(⊢ (let ([l_e (car e-)])
(cond [(string=? l_e l) (let ([x- (cadr e-)]) e_l-)] ...))
: #,(stx-car #'(τ_el ...)))]))
(define-syntax (define/tc stx)
(syntax-parse stx
[(_ x:id e)

3
tapl/stlc+tup.rkt
View File

@ -14,7 +14,8 @@
;; - terms from ext-stlc.rkt
;; - tup and proj
(define-basic-checked-stx ×)
(define-type-constructor ×)
;(define-basic-checked-stx ×)
;(define-type-constructor (× τ ...) #:declare τ type)
(define-syntax (tup stx)

28
tapl/stlc.rkt
View File

@ -1,11 +1,11 @@
#lang racket/base
(require "typecheck.rkt")
(provide (rename-out [λ/tc λ] [app/tc #%app]))
(provide (for-syntax type=? current-type=? type-eval))
(provide (for-syntax type=? types=? current-type=? type-eval))
(provide #%module-begin #%top-interaction #%top require) ; from racket
;; Simply-Typed Lambda Calculus
;; - no base type so cannot write any terms
;; - no base type, so cannot write any terms
;; Types: multi-arg → (1+)
;; Terms:
;; - var
@ -14,12 +14,11 @@
(begin-for-syntax
;; type eval
;; - for now, type-eval = full expansion = canonical type representation
;; - type-eval = =full expansion == canonical type representation
;; - must expand because:
;; - checks for unbound identifiers (ie, undefined types)
;; - later, expanding enables reuse of same mechanisms for kind checking
;; - may require some caution when mixing expanded and unexpanded types to
;; create other types
;; and type application
(define (type-eval τ)
(or #;(expanded-type? τ) ; don't expand if already expanded
(add-orig (expand/df τ) τ)))
@ -29,9 +28,7 @@
;; type=? : Type Type -> Boolean
;; Indicates whether two types are equal
;; type equality == structurally free-identifier=?
;; does not assume any sort of representation (eg expanded/unexpanded)
;; - caller (see typechecks? in typecheck.rkt) is responsible to
;; convert if necessary
;; assumes canonical (ie expanded) representation
(define (type=? τ1 τ2)
; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
@ -47,19 +44,16 @@
(define current-type=? (make-parameter type=?))
(current-typecheck-relation type=?))
;(define-syntax-category type)
(define-syntax-category type)
(define-basic-checked-stx → #:arity >= 1)
#;(define-type-constructor (→ τ_in ... τ_out)
#:declare τ_in type
#:declare τ_out type)
;(define-basic-checked-stx → : #%type #:arity >= 1)
(define-type-constructor → #:arity >= 1)
(define-syntax (λ/tc stx)
(syntax-parse stx
[(_ (b:typed-binding ...) e)
#:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
(⊢ (λ xs- e-) : (→ b.τ ... τ_res))]))
[(_ bvs:type-ctx e)
#:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
(⊢ (λ xs- e-) : (→ bvs.type ... τ_res))]))
(define-syntax (app/tc stx)
(syntax-parse stx

1
tapl/stx-utils.rkt
View File

@ -3,6 +3,7 @@
(provide (all-defined-out))
(define (stx-cadr stx) (stx-car (stx-cdr stx)))
(define (stx-caddr stx) (stx-cadr (stx-cdr stx)))
(define (stx-andmap f . stx-lsts)
(apply andmap f (map syntax->list stx-lsts)))

54
tapl/sysf.rkt
View File

@ -19,53 +19,7 @@
;; - terms from stlc+lit.rkt
;; - Λ and inst
;; dont use define-type-constructor, instead define explicit macro
;(provide ∀)
#;(define-syntax (∀ stx)
(syntax-parse stx
[(_ (x:id ...) body) ; cannot use :type annotation on body bc of unbound vars
;; use #%plain-lambda to avoid insertion of #%expression
(syntax/loc stx (#%plain-lambda (x ...) body))]))
#;(define-type-constructor (∀ [[x ...]] body))
(define-basic-checked-stx ∀ #:arity = 1 #:bvs >= 0)
;(define-syntax ∀
; (syntax-parser
; [(_ (tv:id ...) τ_body)
; #:with ((tv- ...) τ_body- k) (infer/ctx+erase #'([tv : #%type] ...) #'τ_body)
; #:when (#%type? #'k)
; (mk-type #'(λ (tv- ...) τ_body-))]))
;(begin-for-syntax
; (define (infer∀+erase e)
; (syntax-parse (infer+erase e) #:context e
; [(e- τ_e)
; #:with ((~literal #%plain-lambda) (tv ...) τ) #'τ_e
; #'(e- ((tv ...) τ))]))
; (define-syntax ~∀*
; (pattern-expander
; (syntax-parser
; [(_ (tv:id ...) τ)
; #'(~or
; ((~literal #%plain-lambda) (tv ...) τ)
; (~and any (~do
; (type-error
; #:src #'any
; #:msg "Expected ∀ type, got: ~a" #'any))))]))))
#;(begin-for-syntax
;; extend to handle ∀
#;(define (type=? τ1 τ2)
(syntax-parse (list τ1 τ2)
[(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
((~literal #%plain-lambda) (y:id ...) k2 ... t2))
#:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
#:with (z ...) (generate-temporaries #'(x ...))
((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
(substs #'(z ...) #'(y ...) #'t2))]
[_ (stlc:type=? τ1 τ2)]))
(current-type=? type=?)
(current-typecheck-relation type=?))
(define-type-constructor ∀ #:arity = 1 #:bvs >= 0)
(define-syntax (Λ stx)
(syntax-parse stx
@ -75,7 +29,5 @@
(define-syntax (inst stx)
(syntax-parse stx
[(_ e τ:type ...)
#:with (e- (~∀* (tv ...) τ_body)) (infer+erase #'e)
; #:with (e- ∀τ) (infer+erase #'e)
; #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'∀τ
(⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
#:with (e- (tvs (τ_body))) (⇑ e as ∀)
(⊢ e- : #,(substs #'(τ.norm ...) #'tvs #;#'(tv ...) #'τ_body))]))

372
tapl/tests/fomega-tests.rkt
View File

@ -1,198 +1,204 @@
#lang s-exp "../fomega.rkt"
(require "rackunit-typechecking.rkt")
(check-type Int : ★)
(check-type String : ★)
;(check-type Int : ★)
(check-type Int : #%type)
;(check-type String : ★)
(check-type String : #%type)
(typecheck-fail →)
(check-type (→ Int Int) : ★)
;(check-type (→ Int Int) : ★)
(check-type (→ Int Int) : #%type)
(typecheck-fail (→ →))
(typecheck-fail (→ 1))
(check-type 1 : Int)
(check-type (∀ ([t : ★]) (→ t t)) : ★)
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
(check-type (∀ ([t : ★]) (→ t t)) : (⇒ ★))
;(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : #%type)
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
: (∀ ([X : ★]) (→ X X)))
((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x)))
(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
;; partial-apply →
(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
: (⇒ ★ ★))
; f's type must have kind ★
(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
(∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
(check-type (inst
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
: (→ (→ Int String) (→ Int String)))
(typecheck-fail
(inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
#:with-msg "not a valid type: 1")
;; applied f too early
(typecheck-fail (inst
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)))
(check-type ((inst
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
(λ ([x : Int]) "int")) : (→ Int String))
(check-type (((inst
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
(λ ([x : Int]) "int")) 1) : String ⇒ "int")
;; tapl examples, p441
(typecheck-fail
(define-type-alias tmp 1)
#:with-msg "not a valid type: 1")
(define-type-alias Id (tyλ ([X : ★]) X))
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
;; tapl examples, p451
(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
(check-type Pair : (⇒ ★ ★ ★))
(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
; parametric pair constructor
(check-type
(Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
: (∀ ([X : ★][Y : ★]) (→ X Y (tyapp Pair X Y))))
; concrete Pair Int String constructor
(check-type
(inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
Int String)
: (→ Int String (tyapp Pair Int String)))
; Pair Int String value
(check-type
((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
Int String) 1 "1")
: (tyapp Pair Int String))
; fst: parametric
(check-type
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
: (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) X)))
; fst: concrete Pair Int String accessor
(check-type
(inst
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
Int String)
: (→ (tyapp Pair Int String) Int))
; apply fst
(check-type
((inst
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
Int String)
((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
Int String) 1 "1"))
: Int ⇒ 1)
; snd
(check-type
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
: (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) Y)))
(check-type
(inst
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
Int String)
: (→ (tyapp Pair Int String) String))
(check-type
((inst
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
Int String)
((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
Int String) 1 "1"))
: String ⇒ "1")
;;; sysf tests wont work, unless augmented with kinds
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
: (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
: (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
: (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
; first inst should be discarded
(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
; second inst is discarded
(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
;; polymorphic arguments
(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
(check-type
(inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
(check-type
((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
: Int ⇒ 10)
(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
(Λ ([s : ★]) (λ ([y : s]) y)))
: Int ⇒ 10)
;; previous tests -------------------------------------------------------------
(check-type 1 : Int)
(check-not-type 1 : (→ Int Int))
(typecheck-fail #f) ; unsupported literal
(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
(check-not-type (λ ([x : Int]) x) : Int)
(check-type (λ ([x : Int]) x) : (→ Int Int))
(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
: (→ (→ Int Int Int) Int Int Int))
(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
;(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
;(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
;(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
;(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
;(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
;(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
;
;(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
;(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
;(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
;
;;; partial-apply →
;(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
; : (⇒ ★ ★))
;; f's type must have kind ★
;(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
;(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
; (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
;(check-type (inst
; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
; : (→ (→ Int String) (→ Int String)))
;(typecheck-fail
; (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
; #:with-msg "not a valid type: 1")
;
;;; applied f too early
;(typecheck-fail (inst
; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)))
;(check-type ((inst
; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
; (λ ([x : Int]) "int")) : (→ Int String))
;(check-type (((inst
; (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
; (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
; (λ ([x : Int]) "int")) 1) : String ⇒ "int")
;
;;; tapl examples, p441
;(typecheck-fail
; (define-type-alias tmp 1)
; #:with-msg "not a valid type: 1")
;(define-type-alias Id (tyλ ([X : ★]) X))
;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
;(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
;(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
;(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
;
;;; tapl examples, p451
;(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
;
;(check-type Pair : (⇒ ★ ★ ★))
;
;(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
;; parametric pair constructor
;(check-type
; (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
; : (∀ ([X : ★][Y : ★]) (→ X Y (tyapp Pair X Y))))
;; concrete Pair Int String constructor
;(check-type
; (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
; Int String)
; : (→ Int String (tyapp Pair Int String)))
;; Pair Int String value
;(check-type
; ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
; Int String) 1 "1")
; : (tyapp Pair Int String))
;; fst: parametric
;(check-type
; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
; : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) X)))
;; fst: concrete Pair Int String accessor
;(check-type
; (inst
; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
; Int String)
; : (→ (tyapp Pair Int String) Int))
;; apply fst
;(check-type
; ((inst
; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
; Int String)
; ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
; Int String) 1 "1"))
; : Int ⇒ 1)
;; snd
;(check-type
; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
; : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) Y)))
;(check-type
; (inst
; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
; Int String)
; : (→ (tyapp Pair Int String) String))
;(check-type
; ((inst
; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
; Int String)
; ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
; Int String) 1 "1"))
; : String ⇒ "1")
;
;;;; sysf tests wont work, unless augmented with kinds
;(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
;
;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
;
;(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
; : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
;
;(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
; : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
;
;(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
; : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
;
;(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
;(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
;; first inst should be discarded
;(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
;; second inst is discarded
;(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
;
;;; polymorphic arguments
;(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
;(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
;(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
;(check-type
; (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
;(check-type
; ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
; : Int ⇒ 10)
;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
;(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
; (Λ ([s : ★]) (λ ([y : s]) y)))
; : Int ⇒ 10)
;
;
;;; previous tests -------------------------------------------------------------
;(check-type 1 : Int)
;(check-not-type 1 : (→ Int Int))
;(typecheck-fail #f) ; unsupported literal
;(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
;(check-not-type (λ ([x : Int]) x) : Int)
;(check-type (λ ([x : Int]) x) : (→ Int Int))
;(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
;(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
;(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
;(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
; : (→ (→ Int Int Int) Int Int Int))
;(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
;(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
;(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
;(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
;(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)

6
tapl/tests/fsub-tests.rkt
View File

@ -15,6 +15,10 @@
(check-type (proj ((λ ([x : (× [a : Int])]) x) rab) a)
: Int ⇒ 0)
(check-type (Λ ([X <: Top]) (λ ([x : X]) x)) : (∀ ([X <: Top]) (→ X X)))
(check-type (inst (Λ ([X <: Top]) (λ ([x : X]) x)) (× [a : Int][b : Bool]))
: (→ (× [a : Int][b : Bool]) (× [a : Int][b : Bool])))
(check-type (proj ((inst (Λ ([X <: Top]) (λ ([x : X]) x))
(× [a : Int][b : Bool]))
rab) b)
@ -29,7 +33,7 @@
(define fNat (Λ ([X <: Nat]) (λ ([x : X]) (+ x 1))))
(check-type fNat : (∀ ([X <: Nat]) (→ X Nat)))
; check type constructors properly call expose
;; check type constructors properly call expose
(define f2poly
(Λ ([X <: (× [a : Nat])])
(λ ([x : X])

6
tapl/tests/run-all-tests.rkt
View File

@ -22,6 +22,6 @@
(require "fsub-tests.rkt") ; sysf + reco-sub
;;; F_omega
(require "fomega-tests.rkt")
(require "fomega2-tests.rkt")
;; F_omega
;(require "fomega-tests.rkt")
;(require "fomega2-tests.rkt")

10
tapl/tests/stlc+cons-tests.rkt
View File

@ -7,8 +7,14 @@
#:with-msg "nil: requires type annotation")
(check-type (cons 1 (nil {Int})) : (List Int))
(typecheck-fail nil #:with-msg "nil: requires type annotation")
(typecheck-fail (nil Int) #:with-msg "expected ann")
(typecheck-fail (nil (Int)) #:with-msg "expected ann")
(typecheck-fail
(nil Int)
#:with-msg
"Improperly formatted type annotation: Int; should have shape {τ}, where τ is a valid type.")
(typecheck-fail
(nil (Int))
#:with-msg
"Improperly formatted type annotation: \\(Int); should have shape {τ}, where τ is a valid type.")
(typecheck-fail
(λ ([lst : (List Int Int)]) lst)
#:with-msg

493
tapl/typecheck.rkt
View File

@ -62,7 +62,7 @@
;; macro for nicer syntax
(define-syntax (⊢ stx)
(syntax-parse stx #:datum-literals (:)
[(_ e : τ) #'(assign-type #'e #`τ)]
[(_ e : τ) #'(assign-type #`e #`τ)]
[(_ e τ) #'(⊢ e : τ)]))
;; assign-type Type -> Syntax
@ -135,7 +135,9 @@
;; expanded before wrapping in lambda
;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
;; the types before typechecking, which is acceptable
(define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:octx [octx tvctx] #:tag [tag 'unused])
(define (infer es #:ctx [ctx null] #:tvctx [tvctx null]
#:octx [octx tvctx] #:tag [tag 'unused]
#:expand [expand expand/df])
(syntax-parse ctx #:datum-literals (:)
[([x : τ] ...) ; dont expand yet bc τ may have references to tvs
#:with ([tv : k] ...) tvctx
@ -156,7 +158,7 @@
((~literal #%plain-lambda) xs+
((~literal let-values) () ((~literal let-values) ()
((~literal #%expression) e+) ... (~literal void))))))))
(expand/df
(expand
#`(λ (tv ...)
(let-syntax ([tv (make-rename-transformer (assign-type (assign-type #'tv #'k) #'ok #:tag '#,tag))] ...)
(λ (x ...)
@ -177,8 +179,8 @@
(define (infer/ctx+erase ctx e)
(syntax-parse (infer (list e) #:ctx ctx)
[(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
(define (infers/ctx+erase ctx es)
(stx-cdr (infer es #:ctx ctx)))
(define (infers/ctx+erase ctx es #:expand [expand expand/df])
(stx-cdr (infer es #:ctx ctx #:expand expand)))
; tyctx = kind env for bound type vars in term e
(define (infer/tyctx+erase ctx e)
(syntax-parse (infer (list e) #:tvctx ctx)
@ -239,7 +241,7 @@
(begin-for-syntax
;; type validation
;; only check outer wrapper; tycons are responsible for verifying their own args
(define (#%type? t) (typecheck? t #'#%type))
#;(define (#%type? t) (typecheck? t #'#%type))
#;(define (is-type? τ)
(or (plain-type? τ)
; partial expand to reveal #%type wrapper
@ -308,8 +310,8 @@
(define (mk-? id) (format-id id "~a?" id))
(define-for-syntax (mk-? id) (format-id id "~a?" id)))
(define #%type void)
(define-for-syntax (mk-type t) (assign-type t #'#%type))
#;(define #%type void)
#;(define-for-syntax (mk-type t) (assign-type t #'#%type))
#;(define-syntax (define-base-type stx)
(syntax-parse stx
@ -361,12 +363,12 @@
#'e-]))))]))
(define-syntax define-basic-checked-id-stx
(syntax-parser
[(_ τ:id (~optional (~seq : kind) #:defaults ([kind #'#%type])))
#:with τ? (format-id #'τ "~a?" #'τ)
(syntax-parser #:datum-literals (:)
[(_ τ:id : kind)
#:with τ? (mk-? #'τ)
#:with τ-internal (generate-temporary #'τ)
#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
#:with τ-cls (generate-temporary #'τ)
;#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
;#:with τ-cls (generate-temporary #'τ)
#:with τ-expander (format-id #'τ "~~~a" #'τ)
#'(begin
(provide τ (for-syntax τ? τ-expander))
@ -395,26 +397,27 @@
(syntax-parser
[(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))]))
(define-syntax define-base-type (syntax-parser [(_ τ:id) #'(define-basic-checked-id-stx τ)]))
#;(define-syntax define-base-type (syntax-parser [(_ τ:id) #'(define-basic-checked-id-stx τ)]))
; I use identifiers "τ" and "kind" but this form is not restricted to them.
; E.g., τ can be #'★ and kind can be #'#%kind (★'s type)
(define-syntax (define-basic-checked-stx stx)
(syntax-parse stx #:datum-literals (:)
[(_ τ:id (~optional (~seq : kind) #:defaults ([kind #'#%type]))
[(_ τ:id : kind
(~optional
(~seq #:arity op n:exact-nonnegative-integer)
#:defaults ([op #'>=] [n #'0]))
(~optional
(~seq #:bvs (~and has-bvs? bvs-op) bvs-n:exact-nonnegative-integer)
#:defaults ([bvs-op #'>=][bvs-n #'0])))
#:with kind+ ((current-type-eval) #'kind)
#:with #%kind (format-id #'kind "#%~a" #'kind)
;#:with kind+ ((current-type-eval) #'kind)
#:with τ-internal (generate-temporary #'τ)
#:with τ? (mk-? #'τ)
#:with τ-expander (format-id #'τ "~~~a" #'τ)
#:with τ-expander* (format-id #'τ-expander "~a*" #'τ-expander)
#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
#:with τ-get (format-id #'τ "~a-get" #'τ)
;#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
;#:with τ-get (format-id #'τ "~a-get" #'τ)
#`(begin
(provide τ (for-syntax τ-expander τ-expander* τ? #;inferτ+erase))
(begin-for-syntax
@ -450,25 +453,25 @@
(and (stx-pair? t)
(syntax-parse t
[((~literal #%plain-lambda) bvs ((~literal #%plain-app) tycon . _))
(typecheck? #'tycon #'τ-internal)])))
#;(define (τ-get t)
(syntax-parse t
[(τ-expander . pat) #'pat]))
#;(define (inferτ+erase e)
(syntax-parse (infer+erase e) #:context e
[(e- τ_e)
#:fail-unless (stx-pair? #'τ_e)
(format
"~a (~a:~a): Expected expression ~a to have ~a type, got: ~a"
(syntax-source e) (syntax-line e) (syntax-column e)
(syntax->datum e) 'τ (type->str #'τ_e))
#:with ((~literal #%plain-app) tycon . args) #'τ_e
#:fail-unless (typecheck? #'tycon #'τ-internal)
(format
"~a (~a:~a): Expected expression ~a to have ~a type, got: ~a"
(syntax-source e) (syntax-line e) (syntax-column e)
(syntax->datum e) 'τ (type->str #'τ_e))
#`(e- args)])))
(typecheck? #'tycon #'τ-internal)]))))
; #;(define (τ-get t)
; (syntax-parse t
; [(τ-expander . pat) #'pat]))
; #;(define (inferτ+erase e)
; (syntax-parse (infer+erase e) #:context e
; [(e- τ_e)
; #:fail-unless (stx-pair? #'τ_e)
; (format
; "~a (~a:~a): Expected expression ~a to have ~a type, got: ~a"
; (syntax-source e) (syntax-line e) (syntax-column e)
; (syntax->datum e) 'τ (type->str #'τ_e))
; #:with ((~literal #%plain-app) tycon . args) #'τ_e
; #:fail-unless (typecheck? #'tycon #'τ-internal)
; (format
; "~a (~a:~a): Expected expression ~a to have ~a type, got: ~a"
; (syntax-source e) (syntax-line e) (syntax-column e)
; (syntax->datum e) 'τ (type->str #'τ_e))
; #`(e- args)])))
(define τ-internal
(λ _ (raise (exn:fail:type:runtime
(format "~a: Cannot use type at run time" 'τ)
@ -485,186 +488,188 @@
(format "wrong number of type vars, expected ~a ~a" 'bvs-op 'bvs-n)
#:fail-unless (op (stx-length #'args) n)
(format "wrong number of arguments, expected ~a ~a" 'op 'n)
#:with (bvs- τs- ks) (infers/ctx+erase #'([bv : kind] (... ...)) #'args)
#:when (stx-andmap
(λ (t k)
(or (typecheck? k #'kind+)
(type-error #:src t
#:msg "not a valid type: ~a" t)))
#'args #'ks)
;#:with (~! (~var _ type) (... ...)) #'τs-
#:with (bvs- τs- _)
(infers/ctx+erase #'([bv : #%kind] (... ...)) #'args
#:expand (current-type-eval))
; #:when (stx-andmap
; (λ (t k)
; (or (typecheck? k #'kind+)
; (type-error #:src t
; #:msg "not a valid type: ~a" t)))
; #'args #'ks)
#:with (~! (~var _ kind) (... ...)) #'τs-
; #:with (~! [arg- τ_arg] (... ...)) (infers+erase #'args)
; #:when (stx-andmap (λ (t) (typecheck? t #'#%type)) #'(τ_arg (... ...)))
(assign-type #'(λ bvs- (τ-internal . τs-)) #'kind)]
(assign-type #'(λ bvs- (τ-internal . τs-)) #'#%kind)]
;; else fail with err msg
[_
(type-error #:src stx
#:msg (string-append
"Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
#'τ stx #'op #'n)])))]
#;[(_ #:cat cat
(τ:id (~optional (~and bvs-pat:bound-vars bvs-test) ; bvs-test checks for existence of bound vars
#:defaults ([bvs-pat.stx #'[[]]][(bvs-pat.x 1) null]))
. pat)
; lits must have ~ prefix (for syntax-parse compat) for now
(~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null]))
decls ...
#;(~optional (~seq (~seq #:decl tvar (~datum as) cls) ...)
#:defaults ([(tvar 1) null][(cls 1) null])))
#:with τ-match (format-id #'τ "~a-match" #'τ)
#:with τ? (format-id #'τ "~a?" #'τ)
#:with τ-get (format-id #'τ "~a-get" #'τ)
#:with τ-match+erase (format-id #'τ "infer~a+erase" #'τ)
#:with τ-expander (format-id #'τ "~~~a" #'τ)
#:with τ-expander* (format-id #'τ "~~~a*" #'τ)
#:with pat-class (generate-temporary #'τ) ; syntax-class name
#:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
#:with (lit-tmp ...) (generate-temporaries #'(lit ...))
#`(begin
;; list can't be function, ow it will use typed #%app
;; define lit as macro that expands into #%app,
;; so it will use the #%app here (racket's #%app)
(define lit-tmp void) ...
(define-syntax lit (syntax-parser [(_ . xs) #'(lit-tmp . xs)])) ...
(provide lit ...)
(provide τ (for-syntax τ-expander τ-expander*))
(begin-for-syntax
#;(define-syntax lit
(pattern-expander
(syntax-parser
[(_ . xs)
#'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ;...
; the ~τ pattern backtracks normally;
; the ~τ* version errors immediately for a non-match
(define-syntax τ-expander
(pattern-expander
(syntax-parser
[(_ (~optional
(~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
. match-pat)
;; manually replace literals with expanded form, to get around ~ restriction
#:with new-match-pat
#`#,(subst-datum-lits
#`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
#'(lit ...)
#'match-pat)
#'((~literal #%plain-type)
((~literal #%plain-lambda) (bvs.x (... ...))
((~literal let-values) () ((~literal let-values) ()
((~literal #%plain-app) (~literal tycon) . new-match-pat)))))])))
(define-syntax τ-expander*
(pattern-expander
(syntax-parser
[(_ (~optional
(~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
. match-pat)
#:with pat-from-constructor
#,(if (attribute bvs-test)
#'(quote-syntax (τ bvs-pat.stx . pat))
#'(quote-syntax (τ . pat)))
;; manually replace literals with expanded form, to get around ~ restriction
#:with new-match-pat
#`#,(subst-datum-lits
#`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
#'(lit ...)
#'match-pat)
#'(~and
(~or
((~literal #%plain-type)
((~literal #%plain-lambda) (bvs.x (... ...))
((~literal let-values) () ((~literal let-values) ()
((~literal #%plain-app) (~literal tycon) . new-match-pat)))))
(~and any
(~do
(type-error #:src #'any
#:msg
"Expected type of expression to match pattern ~a, got: ~a"
(quote-syntax pat-from-constructor) #'any))))
~!)])))
(define-syntax-class pat-class
;; dont check is-type? here; should already be types
;; only check is-type? for user-entered types, eg tycon call
;; thus, dont include decls here, only want shape
; uses "lit" pattern expander
(pattern pat))
(define (τ-match ty)
(or (match-type ty tycon pat-class)
;; error msg should go in specific macro def?
(type-error #:src ty
#:msg "Expected type with pattern: ~a, got: ~a"
(quote-syntax (τ . pat)) ty)))
; predicate version of τ-match
(define (τ? ty) (match-type ty tycon pat-class))
;; expression version of τ-match
(define (τ-match+erase e)
(syntax-parse (infer+erase e)
[(e- ty)
#:with τ_matched/#f (match-type #'ty tycon pat-class)
#:fail-unless (syntax-e #'τ_matched/#f)
(format
"~a (~a:~a): Expected type of expression ~a to match pattern ~a, got: ~a"
(syntax-source e) (syntax-line e) (syntax-column e)
(syntax->datum e) (type->str (quote-syntax (τ . pat))) (type->str #'ty))
#'(e- τ_matched/#f)]))
;; get syntax bound to specific pat var (as declared in def-tycon)
(define-syntax (τ-get stx)
(syntax-parse stx #:datum-literals (from)
[(_ attr from ty)
#:with args (generate-temporary)
#:with args.attr (format-id #'args "~a.~a" #'args #'attr)
#:with the-pat (quote-syntax (τ . pat))
#'(syntax-parse #'ty ;((current-type-eval) #'ty)
[typ ;((~literal #%plain-type) ((~literal #%plain-app) f . args))
#:fail-unless (τ? #'typ)
(format "~a (~a:~a) Expected type with pattern: ~a, got: ~a"
(syntax-source #'typ) (syntax-line #'typ) (syntax-column #'typ)
(type->str (quote-syntax the-pat)) (type->str #'typ))
#:with ((~literal #%plain-type)
((~literal #%plain-lambda) tvs
((~literal let-values) () ((~literal let-values) ()
((~literal #%plain-app) f . args)))))
((current-type-eval) #'typ)
#:declare args pat-class ; check shape of arguments
; #:fail-unless (typecheck? #'f #'tycon) ; check tycons match
; (format "Type error: expected ~a type, got ~a"
; (type->str #'τ) (type->str #'ty))
(attribute args.attr)])])))
(define tycon (λ _ (raise (exn:fail:type:runtime
(format "~a: Cannot use type at run time" 'τ)
(current-continuation-marks)))))
(define-syntax (τ stx)
(syntax-parse stx #:literals (lit ...)
[(_ (~optional (~or (~and bvs:bound-vars bvs-pat.stx)
(~seq #:bind (~and bvs (bvs-pat.x ...)))))
. (~and pat ~! args)) ; first check shape
#:with (tv (... ...)) (cond [(attribute bvs.x) #'(bvs.x (... ...))]
[(attribute bvs) #'bvs]
[else null])
; this inner syntax-parse gets the ~! to register
; otherwise, apparently #:declare's get subst into pat (before ~!)
(syntax-parse #'args #:literals (lit ...)
[pat #,@#'(decls ...) ; then check declarations (eg, valid type)
#'(#%type
(λ (tv (... ...)) ;(bvs.x (... ...))
; (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
(let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] (... ...))
(tycon . args))))])]
[_
#:with expected-pat
#,(if (attribute bvs-test)
#'(quote-syntax (τ bvs-pat.stx . pat))
#'(quote-syntax (τ . pat)))
(type-error #:src stx
#:msg (string-append
"Improper usage of type constructor ~a: ~a, expected pattern ~a, "
#;(format
"where: ~a"
(string-join
(stx-map
(λ (typ clss) (format "~a is a ~a" typ clss))
#'(ty (... ...)) #'(cls (... ...)))
", ")))
#'τ stx #'expected-pat)])))]))
#'τ stx #'op #'n)])))]))
; #;[(_ #:cat cat
; (τ:id (~optional (~and bvs-pat:bound-vars bvs-test) ; bvs-test checks for existence of bound vars
; #:defaults ([bvs-pat.stx #'[[]]][(bvs-pat.x 1) null]))
; . pat)
; ; lits must have ~ prefix (for syntax-parse compat) for now
; (~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null]))
; decls ...
; #;(~optional (~seq (~seq #:decl tvar (~datum as) cls) ...)
; #:defaults ([(tvar 1) null][(cls 1) null])))
; #:with τ-match (format-id #'τ "~a-match" #'τ)
; #:with τ? (format-id #'τ "~a?" #'τ)
; #:with τ-get (format-id #'τ "~a-get" #'τ)
; #:with τ-match+erase (format-id #'τ "infer~a+erase" #'τ)
; #:with τ-expander (format-id #'τ "~~~a" #'τ)
; #:with τ-expander* (format-id #'τ "~~~a*" #'τ)
; #:with pat-class (generate-temporary #'τ) ; syntax-class name
; #:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
; #:with (lit-tmp ...) (generate-temporaries #'(lit ...))
; #`(begin
; ;; list can't be function, ow it will use typed #%app
; ;; define lit as macro that expands into #%app,
; ;; so it will use the #%app here (racket's #%app)
; (define lit-tmp void) ...
; (define-syntax lit (syntax-parser [(_ . xs) #'(lit-tmp . xs)])) ...
; (provide lit ...)
; (provide τ (for-syntax τ-expander τ-expander*))
; (begin-for-syntax
; #;(define-syntax lit
; (pattern-expander
; (syntax-parser
; [(_ . xs)
; #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ;...
; ; the ~τ pattern backtracks normally;
; ; the ~τ* version errors immediately for a non-match
; (define-syntax τ-expander
; (pattern-expander
; (syntax-parser
; [(_ (~optional
; (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
; . match-pat)
; ;; manually replace literals with expanded form, to get around ~ restriction
; #:with new-match-pat
; #`#,(subst-datum-lits
; #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
; #'(lit ...)
; #'match-pat)
; #'((~literal #%plain-type)
; ((~literal #%plain-lambda) (bvs.x (... ...))
; ((~literal let-values) () ((~literal let-values) ()
; ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))])))
; (define-syntax τ-expander*
; (pattern-expander
; (syntax-parser
; [(_ (~optional
; (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
; . match-pat)
; #:with pat-from-constructor
; #,(if (attribute bvs-test)
; #'(quote-syntax (τ bvs-pat.stx . pat))
; #'(quote-syntax (τ . pat)))
; ;; manually replace literals with expanded form, to get around ~ restriction
; #:with new-match-pat
; #`#,(subst-datum-lits
; #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
; #'(lit ...)
; #'match-pat)
; #'(~and
; (~or
; ((~literal #%plain-type)
; ((~literal #%plain-lambda) (bvs.x (... ...))
; ((~literal let-values) () ((~literal let-values) ()
; ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))
; (~and any
; (~do
; (type-error #:src #'any
; #:msg
; "Expected type of expression to match pattern ~a, got: ~a"
; (quote-syntax pat-from-constructor) #'any))))
; ~!)])))
; (define-syntax-class pat-class
; ;; dont check is-type? here; should already be types
; ;; only check is-type? for user-entered types, eg tycon call
; ;; thus, dont include decls here, only want shape
; ; uses "lit" pattern expander
; (pattern pat))
; (define (τ-match ty)
; (or (match-type ty tycon pat-class)
; ;; error msg should go in specific macro def?
; (type-error #:src ty
; #:msg "Expected type with pattern: ~a, got: ~a"
; (quote-syntax (τ . pat)) ty)))
; ; predicate version of τ-match
; (define (τ? ty) (match-type ty tycon pat-class))
; ;; expression version of τ-match
; (define (τ-match+erase e)
; (syntax-parse (infer+erase e)
; [(e- ty)
; #:with τ_matched/#f (match-type #'ty tycon pat-class)
; #:fail-unless (syntax-e #'τ_matched/#f)
; (format
; "~a (~a:~a): Expected type of expression ~a to match pattern ~a, got: ~a"
; (syntax-source e) (syntax-line e) (syntax-column e)
; (syntax->datum e) (type->str (quote-syntax (τ . pat))) (type->str #'ty))
; #'(e- τ_matched/#f)]))
; ;; get syntax bound to specific pat var (as declared in def-tycon)
; (define-syntax (τ-get stx)
; (syntax-parse stx #:datum-literals (from)
; [(_ attr from ty)
; #:with args (generate-temporary)
; #:with args.attr (format-id #'args "~a.~a" #'args #'attr)
; #:with the-pat (quote-syntax (τ . pat))
; #'(syntax-parse #'ty ;((current-type-eval) #'ty)
; [typ ;((~literal #%plain-type) ((~literal #%plain-app) f . args))
; #:fail-unless (τ? #'typ)
; (format "~a (~a:~a) Expected type with pattern: ~a, got: ~a"
; (syntax-source #'typ) (syntax-line #'typ) (syntax-column #'typ)
; (type->str (quote-syntax the-pat)) (type->str #'typ))
; #:with ((~literal #%plain-type)
; ((~literal #%plain-lambda) tvs
; ((~literal let-values) () ((~literal let-values) ()
; ((~literal #%plain-app) f . args)))))
; ((current-type-eval) #'typ)
; #:declare args pat-class ; check shape of arguments
;; #:fail-unless (typecheck? #'f #'tycon) ; check tycons match
;; (format "Type error: expected ~a type, got ~a"
;; (type->str #'τ) (type->str #'ty))
; (attribute args.attr)])])))
; (define tycon (λ _ (raise (exn:fail:type:runtime
; (format "~a: Cannot use type at run time" 'τ)
; (current-continuation-marks)))))
; (define-syntax (τ stx)
; (syntax-parse stx #:literals (lit ...)
; [(_ (~optional (~or (~and bvs:bound-vars bvs-pat.stx)
; (~seq #:bind (~and bvs (bvs-pat.x ...)))))
; . (~and pat ~! args)) ; first check shape
; #:with (tv (... ...)) (cond [(attribute bvs.x) #'(bvs.x (... ...))]
; [(attribute bvs) #'bvs]
; [else null])
; ; this inner syntax-parse gets the ~! to register
; ; otherwise, apparently #:declare's get subst into pat (before ~!)
; (syntax-parse #'args #:literals (lit ...)
; [pat #,@#'(decls ...) ; then check declarations (eg, valid type)
; #'(#%type
; (λ (tv (... ...)) ;(bvs.x (... ...))
;; (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
; (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] (... ...))
; (tycon . args))))])]
; [_
; #:with expected-pat
; #,(if (attribute bvs-test)
; #'(quote-syntax (τ bvs-pat.stx . pat))
; #'(quote-syntax (τ . pat)))
; (type-error #:src stx
; #:msg (string-append
; "Improper usage of type constructor ~a: ~a, expected pattern ~a, "
; #;(format
; "where: ~a"
; (string-join
; (stx-map
; (λ (typ clss) (format "~a is a ~a" typ clss))
; #'(ty (... ...)) #'(cls (... ...)))
; ", ")))
; #'τ stx #'expected-pat)])))]))
; define-type-constructor, archied 2015-08-12
;(define-syntax define-type-constructor
@ -897,31 +902,40 @@
(define-syntax (define-syntax-category stx)
(syntax-parse stx
[(_ name:id)
#:with names (format-id #'name "~as" #'name)
#:with #%tag (format-id #'name "#%~a" #'name)
#:with #%tag? (mk-? #'#%tag)
#:with name? (mk-? #'name)
#:with named-binding (format-id #'name "~aed-binding" #'name)
#:with current-name? (format-id #'name? "current-~a" #'name?)
#:with is-name? (mk-? #'name)
#:with name-ctx (format-id #'name "~a-ctx" #'name)
#:with name-bind (format-id #'name "~a-bind" #'name)
#:with current-is-name? (format-id #'is-name? "current-~a" #'is-name?)
#:with mk-name (format-id #'name "mk-~a" #'name)
#:with define-base-name (format-id #'name "define-base-~a" #'name)
#:with define-name-cons (format-id #'name "define-~a-constructor" #'name)
#:with name-ann (format-id #'name "~a-ann" #'name)
#'(begin
(provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann)
#%tag define-base-name define-name-cons)
(define #%tag void)
(begin-for-syntax
(define (#%tag? t) (typecheck? t #'#%tag))
(define (name? t) (#%tag? (typeof t)))
(define current-name? (make-parameter name?))
(define (is-name? t) (#%tag? (typeof t)))
(define current-is-name? (make-parameter is-name?))
(define (mk-name t) (assign-type t #'#%tag))
(define-syntax-class name
#:attributes (norm)
(pattern τ
#:with norm ((current-type-eval) #'τ)
#:with k (typeof #'norm)
#:fail-unless (#%tag? #'k)
;#:fail-unless ((current-name?) #'norm)
;#:fail-unless ((current-name?) #'norm)
;#:fail-unless (#%tag? #'k)
#:fail-unless ((current-is-name?) #'norm)
(format "~a (~a:~a) not a valid ~a: ~a"
(syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
'name (type->str #'τ))))
(define-syntax-class named-binding #:datum-literals (:)
#:attributes (x tag)
(pattern [x:id : ~! (~var ty name)] #:attr tag #'ty.norm)
(define-syntax-class name-bind #:datum-literals (:)
#:attributes (x name)
(pattern [x:id : ~! (~var ty name)]
#:attr name #'ty.norm)
(pattern any
#:fail-when #t
(format
@ -929,10 +943,35 @@
"Improperly formatted ~a annotation: ~a; should have shape [x : τ], "
"where τ is a valid ~a.")
'name (type->str #'any) 'name)
#:attr x #f #:attr tag #f))))]))
#:attr x #f #:attr name #f))
(define-syntax-class name-ctx
#:attributes ((x 1) (name 1))
(pattern ((~var || name-bind) (... ...))))
(define-syntax-class name-ann ; type instantiation
#:attributes (norm)
(pattern stx
#:when (stx-pair? #'stx)
#:when (brace? #'stx)
#:with ((~var t name)) #'stx
#:attr norm (delay #'t.norm))
(pattern any
#:fail-when #t
(type-error #:src #'any #:msg
(format
(string-append
"Improperly formatted ~a annotation: ~a; should have shape {τ}, "
"where τ is a valid ~a.")
'name (type->str #'any) 'name))
#:attr norm #f)))
(define-syntax define-base-name
(syntax-parser
[(_ (~var x id)) #'(define-basic-checked-id-stx x : #%tag)]))
(define-syntax define-name-cons
(syntax-parser
[(_ (~var x id) . rst) #'(define-basic-checked-stx x : name . rst)])))]))
;; syntax classes
(begin-for-syntax
(define-syntax-class type
#;(define-syntax-class type
;; τ = surface syntax, as written
;; norm = canonical form for the type, ie expanded
;; -dont bother to check if type is already expanded, because this class
@ -946,7 +985,7 @@
(syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
(type->str #'τ))))
(define-syntax-class typed-binding #:datum-literals (:)
#;(define-syntax-class typed-binding #:datum-literals (:)
#:attributes (x τ)
(pattern [x:id : ~! ty:type] #:attr τ #'ty.norm)
(pattern any
@ -961,7 +1000,7 @@
(define (brace? stx)
(define paren-shape/#f (syntax-property stx 'paren-shape))
(and paren-shape/#f (char=? paren-shape/#f #\{)))
(define-syntax-class ann ; type instantiation
#;(define-syntax-class ann ; type instantiation
#:attributes (τ norm)
(pattern stx
#:when (stx-pair? #'stx)
@ -979,7 +1018,7 @@
(define-syntax (define-primop stx)
#;(define-syntax (define-primop stx)
(syntax-parse stx #:datum-literals (:)
[(_ op:id : τ (~optional (~seq : k) #:defaults ([k #'#%type])))
#:with kind ((current-type-eval) #'k)
@ -997,7 +1036,7 @@
#:with op (format-id stx "~a" #'op)
(syntax/loc stx (app op x (... ...)))])))]))
(define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
;(define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
(begin-for-syntax
; subst τ for y in e, if (bound-id=? x y)