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

Add Typed Scheme as a collection.

Browse Source 
svn: r8864

original commit: 0d54ed5e7427f5e75e6274cc3c9625e676fc34bc
This commit is contained in:
Sam Tobin-Hochstadt 2008-03-03 22:57:55 +00:00
commit 7f2824d11c
21 changed files with 2960 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/typed-scheme/info.ss Normal file
View File

@ -0,0 +1,4 @@
#lang setup/infotab
(define name "Typed Scheme")
(define scribblings '(("typed-scheme.scrbl")))

9
collects/typed-scheme/lang/main.ss Normal file
View File

@ -0,0 +1,9 @@
#lang s-exp "minimal.ss"
(providing (libs (except scheme/base require #%module-begin #%top-interaction with-handlers lambda #%app))
(basics #%module-begin
#%top-interaction
with-handlers
lambda
#%app)
(from scheme require))

29
collects/typed-scheme/lang/minimal.ss Normal file
View File

@ -0,0 +1,29 @@
#lang scheme/base
(provide #%module-begin provide require rename-in rename-out prefix-in only-in all-from-out except-out except-in
providing begin)
(require (for-syntax scheme/base))
(define-for-syntax ts-mod "../typed-scheme.ss")
(define-syntax (providing stx)
(syntax-case stx (libs from basics except)
[(form (libs (except lb ex ...) ...) (basics b ...) (from spec id ...) ...)
(datum->syntax
stx
(syntax->datum
(with-syntax ([(b* ...) (generate-temporaries #'(b ...))]
[ts ts-mod])
(syntax/loc
stx
(begin
(require (except-in ts b ...))
(require (only-in ts [b b*] ...))
(require (except-in lb ex ...) ...)
(require (only-in spec id ...) ...)
(provide id ...) ...
(provide (rename-out [b* b] ...))
(provide (all-from-out ts))
(provide (all-from-out lb) ...))))))]))

15
collects/typed-scheme/lang/reader.ss Normal file
View File

@ -0,0 +1,15 @@
(module reader scheme/base
(require (prefix-in r: "../typed-reader.ss")
(only-in syntax/module-reader wrap-read-all))
(define (*read in)
(wrap-read-all 'typed-scheme/lang/main in r:read))
(define (*read-syntax src in)
(wrap-read-all 'typed-scheme/lang/main
in
(lambda (in)
(r:read-syntax src in))))
(provide (rename-out [*read read] [*read-syntax read-syntax])))

570
collects/typed-scheme/private/base-env.ss Normal file
View File

@ -0,0 +1,570 @@
#lang scheme/base
(require (for-template (only-in (lib "list.ss") foldl)
scheme/base
'#%paramz
scheme/promise
string-constants/string-constant
#;'#%more-scheme
#;'#%qq-and-or
(lib "match-error.ss" "mzlib" "private" "match"))
)
(require
"extra-procs.ss"
scheme/promise
(except-in "type-rep.ss" make-arr)
(only-in scheme/list cons?)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"union.ss"
string-constants/string-constant
(lib "match-error.ss" "mzlib" "private" "match")
"tc-structs.ss")
(require (for-syntax
scheme/base
"init-envs.ss"
(except-in "type-rep.ss" make-arr)
(only-in (lib "list.ss") foldl)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"union.ss"
string-constants/string-constant
(lib "match-error.ss" "mzlib" "private" "match")
"tc-structs.ss"))
(define-for-syntax (initialize-others)
(d-s date
([second : N] [minute : N] [hour : N] [day : N] [month : N]
[year : N] [weekday : N] [year-day : N] [dst? : B] [time-zone-offset : N])
())
(d-s exn ([message : -String] [continuation-marks : Univ]) ())
(d-s (exn:fail exn) () (-String Univ))
(d-s (exn:fail:read exn:fail) ([srclocs : (-lst Univ)]) (-String Univ))
)
(provide (for-syntax initial-env initialize-others))
(define-for-syntax initial-env
(let ([make-lst make-Listof]
[make-lst/elements -pair])
(make-env
[string->sexpr (-> -String (-mu x (Un Sym -String N B (-lst x))))]
(car (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v a)]
[((make-lst (-v a))) (-v a)])))
[first (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v a)]
[((make-lst (-v a))) (-v a)]))]
[second (-poly (a b c)
(cl->
[((-pair a (-pair b c))) b]
[((-lst a)) a]))]
[third (-poly (a b c d)
(cl->
[((-pair a (-pair b (-pair c d)))) c]
[((-lst a)) a]))]
[fourth (-poly (a) ((-lst a) . -> . a))]
[fifth (-poly (a) ((-lst a) . -> . a))]
[sixth (-poly (a) ((-lst a) . -> . a))]
[rest (-poly (a) ((-lst a) . -> . (-lst a)))]
(cadr
(-poly (a b c)
(cl->
[((-pair a (-pair b c))) b]
[((-lst a)) a])))
(caddr (-poly (a) (-> (-lst a) a)))
(cadddr (-poly (a) (-> (-lst a) a)))
(cdr (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v b)]
[((make-lst (-v a))) (make-lst (-v a))])))
(cddr (make-Poly (list 'a) (-> (make-lst (-v a)) (make-lst (-v a)))))
(cdddr (make-Poly (list 'a) (-> (make-lst (-v a)) (make-lst (-v a)))))
(cons (-poly (a b)
(cl-> [(a (-lst a)) (-lst a)]
[(a b) (-pair a b)])))
[*cons (-poly (a b) (cl->
[(a b) (-pair a b)]
[(a (-lst a)) (-lst a)]))]
[*list? (make-pred-ty (-lst Univ))]
(null? (make-pred-ty (-val null)))
(eof-object? (make-pred-ty (-val eof)))
[null (-val null)]
(number? (make-pred-ty N))
(integer? (make-pred-ty -Integer))
(boolean? (make-pred-ty B))
(add1 (-> N N))
(sub1 (-> N N))
(eq? (-> Univ Univ B))
(eqv? (-> Univ Univ B))
(equal? (-> Univ Univ B))
(even? (-> N B))
[assert (-poly (a) (-> (*Un a (-val #f)) a))]
[gensym (cl-> [(Sym) Sym]
[() Sym])]
[string-append (->* null -String -String)]
[open-input-string (-> -String -Input-Port)]
[open-output-file
(cl->
[(-Pathlike) -Port]
[(-Pathlike Sym) -Port])]
[read (cl->
[(-Port) -Sexp]
[() -Sexp])]
[ormap (-poly (a b) ((-> a b) (-lst a) . -> . b))]
[andmap (-poly (a b) ((-> a b) (-lst a) . -> . b))]
[newline (cl-> [() -Void]
[(-Port) -Void])]
[not (-> Univ B)]
[floor (-> N N)]
[box (-poly (a) (a . -> . (make-Box a)))]
[unbox (-poly (a) ((make-Box a) . -> . a))]
[set-box! (-poly (a) ((make-Box a) a . -> . -Void))]
[box? (make-pred-ty (make-Box Univ))]
[cons? (make-pred-ty (-pair Univ Univ))]
[pair? (make-pred-ty (-pair Univ Univ)) #;(-poly (a b) (make-pred-ty (-pair a b)))]
[empty? (make-pred-ty (-val null))]
[empty (-val null)]
[string? (make-pred-ty -String)]
[string (->* '() -Char -String)]
[symbol? (make-pred-ty Sym)]
[list? (make-pred-ty (-lst Univ))]
[list (-poly (a) (->* '() a (-lst a)))]
[procedure? (make-pred-ty (make-Function (list (make-top-arr))))]
[map
(-poly (a b c d)
(cl-> [((-> a b) (-lst a)) (-lst b)]
[((-> a b c) (-lst a) (-lst b)) (-lst c)]
[((-> a b c d) (-lst a) (-lst b) (-lst c)) (-lst d)]))]
[for-each
(-poly (a b c)
(cl-> [((-> a b) (-lst a)) -Void]
[((-> a b c) (-lst a) (-lst b)) -Void]))]
[foldl (-poly (a b)
((a b . -> . b) b (make-lst a) . -> . b))]
[call-with-values (-poly (a b) (-> (-> a) (-> a b) b))]
(error
(make-Function (list
(make-arr null (Un))
(make-arr (list Sym -String) (Un) Univ)
(make-arr (list -String) (Un) Univ)
(make-arr (list Sym) (Un)))))
[namespace-variable-value
(cl->
[(Sym) Univ]
[(Sym B -Namespace (-> Univ)) Univ])]
(match:error (Univ . -> . (Un)))
(display
(cl->
[(Univ) -Void]
[(Univ -Port) -Void]))
[void (->* '() Univ -Void)]
[void? (make-pred-ty -Void)]
[printf (->* (list -String) Univ -Void)]
[fprintf (->* (list -Output-Port -String) Univ -Void)]
[format (->* (list -String) Univ -String)]
(fst (make-Poly (list 'a 'b) (-> (make-lst/elements (-v a) (-v b)) (-v a))))
(snd (make-Poly (list 'a 'b) (-> (make-lst/elements (-v a) (-v b)) (-v b))))
(= (->* (list N N) N B))
(>= (->* (list N N) N B))
(< (->* (list N N) N B))
(<= (->* (list N N) N B))
[> (->* (list N) N B)]
(zero? (N . -> . B))
(* (->* '() N N))
(/ (->* (list N) N N))
(+ (->* '() N N))
(- (->* (list N) N N))
(max (->* (list N) N N))
(min (->* (list N) N N))
[values (make-Poly '(a) (-> (-v a) (-v a)))]
[vector-ref
(make-Poly (list 'a) ((make-Vector (-v a)) N . -> . (-v a)))]
[build-vector (-poly (a) (N (N . -> . a) . -> . (make-Vector a)))]
[reverse (make-Poly '(a) (-> (make-lst (-v a)) (make-lst (-v a))))]
[append (-poly (a) (->* (list) (-lst a) (-lst a)))]
[length (make-Poly '(a) (-> (make-lst (-v a)) N))]
[memq (make-Poly (list 'a) (-> (-v a) (make-lst (-v a)) (-opt (make-lst (-v a)))))]
[memv (make-Poly (list 'a) (-> (-v a) (make-lst (-v a)) (-opt (make-lst (-v a)))))]
[member
(-poly (a) (a (-lst a) . -> . (-opt (-lst a))))]
[string<? (->* (list -String -String) -String B)]
[string>? (->* (list -String -String) -String B)]
[string=? (->* (list -String -String) -String B)]
[char=? (->* (list -Char -Char) -Char B)]
[string<=? (->* (list -String -String) -String B)]
[string>=? (->* (list -String -String) -String B)]
[string-ci<? (->* (list -String -String) -String B)]
[string-ci>? (->* (list -String -String) -String B)]
[string-ci=? (->* (list -String -String) -String B)]
[string-ci<=? (->* (list -String -String) -String B)]
[string-ci>=? (->* (list -String -String) -String B)]
[string-upcase (-> -String -String)]
[string-downcase (-> -String -String)]
[string-titlecase (-> -String -String)]
[string-foldcase (-> -String -String)]
[string-normalize-nfd (-> -String -String)]
[string-normalize-nfkd (-> -String -String)]
[string-normalize-nfc (-> -String -String)]
[string-normalize-nfkc (-> -String -String)]
[string-ref (-> -String N -Char)]
[substring (cl->*
(-> -String N -String)
(-> -String N N -String))]
[string->path (-> -String -Path)]
[file-exists? (-> -Pathlike B)]
[assq (-poly (a) (-> Univ (-lst (-pair Univ a)) a))]
[build-path ((list -Pathlike*) -Pathlike* . ->* . -Path)]
[string->number (-> -String (-opt N))]
[with-input-from-file
(-poly (a)
(cl->
[(-Pathlike (-> a)) a]
[(-Pathlike (-> a) Sym) a]))]
[with-output-to-file
(-poly (a)
(cl->
[(-Pathlike (-> a)) a]
[(-Pathlike (-> a) Sym) a]))]
[random (cl->
[(N) N]
[() N])]
[assoc (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
[list-ref (-poly (a) ((-lst a) N . -> . a))]
[positive? (-> N B)]
[negative? (-> N B)]
[odd? (-> N B)]
[even? (-> N B)]
[apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))]
[call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))]
[quotient (N N . -> . N)]
[remainder (N N . -> . N)]
[quotient/remainder (N N . -> . (-values (list N N)))]
;; parameter stuff
[parameterization-key Sym]
[extend-parameterization (-poly (a b) (-> Univ (-Param a b) a Univ))]
[continuation-mark-set-first (-> (-opt -Cont-Mark-Set) Univ Univ)]
[make-parameter (-poly (a b) (cl-> [(a) (-Param a a)]
[(b (a . -> . b)) (-Param a b)]))]
[current-directory (-Param -Pathlike -Path)]
[current-namespace (-Param -Namespace -Namespace)]
[print-struct (-Param B B)]
[read-decimal-as-inexact (-Param B B)]
[current-command-line-arguments (-Param (make-Vector -String) (make-Vector -String))]
;; regexp stuff
[regexp-match
(cl->
[((*Un -String -Regexp) -String) (-opt (-lst (-opt -String)))]
[(-Pattern -String) (-opt (-lst (-opt (*Un -Bytes -String))))]
[(-Pattern -String N) (-opt (-lst (-opt (*Un -Bytes -String))))]
[(-Pattern -String N (-opt N)) (-opt (-lst (-opt (*Un -Bytes -String))))]
[(-Pattern -String N (-opt N) (-opt -Output-Port)) (-lst (-opt (*Un -Bytes -String)))]
[(-Pattern -String (-opt N) (-opt -Output-Port)) (-lst (-opt (*Un -Bytes -String)))]
[(-Pattern -String (-opt -Output-Port)) (-lst (-opt (*Un -Bytes -String)))]
[(-Pattern (*Un -Input-Port -Bytes)) (-opt (-lst (-opt -Bytes)))]
[(-Pattern (*Un -Input-Port -Bytes) N) (-opt (-lst (-opt -Bytes)))]
[(-Pattern (*Un -Input-Port -Bytes) N (-opt N)) (-opt (-lst (-opt -Bytes)))]
[(-Pattern (*Un -Input-Port -Bytes) (-opt N)) (-opt (-lst (-opt -Bytes)))]
[(-Pattern (*Un -Input-Port -Bytes) N (-opt N) (-opt -Output-Port)) (-lst (-opt -Bytes))])]
[number->string (N . -> . -String)]
[current-milliseconds (-> N)]
[modulo (N N . -> . N)]
;; errors
[raise-type-error
(cl->
[(Sym -String Univ) (Un)]
[(Sym -String N (-lst Univ)) (Un)])]
;; this is a hack
[match:error ((list) Univ . ->* . (Un))]
[vector-set! (-poly (a) (-> (make-Vector a) N a -Void))]
[vector->list (-poly (a) (-> (make-Vector a) (-lst a)))]
[list->vector (-poly (a) (-> (-lst a) (make-Vector a)))]
[exact? (N . -> . B)]
[inexact? (N . -> . B)]
[expt (N N . -> . N)]
[vector (-poly (a) (->* (list) a (make-Vector a)))]
[real? (Univ . -> . B)]
[real-part (N . -> . N)]
[imag-part (N . -> . N)]
[magnitude (N . -> . N)]
[angle (N . -> . N)]
[numerator (N . -> . N)]
[denominator (N . -> . N)]
[exact->inexact (N . -> . N)]
[inexact->exact (N . -> . N)]
[make-string
(cl->
[(N) -String]
[(N -Char) -String])]
[arithmetic-shift (N N . -> . N)]
[abs (N . -> . N)]
[substring (cl-> [(-String N) -String]
[(-String N N) -String])]
[string-length (-String . -> . N)]
[string-set! (-String N -Char . -> . -Void)]
[make-vector
(-poly (a)
(cl->
[(N) (make-Vector N)]
[(N a) (make-Vector a)]))]
[file-exists? (-Pathlike . -> . B)]
[string->symbol (-String . -> . Sym)]
[symbol->string (Sym . -> . -String)]
[vector-length (-poly (a) ((make-Vector a) . -> . N))]
[call-with-input-file (-poly (a)
(cl->
[(-String (-Port . -> . a)) a]
[(-String (-Port . -> . a) Sym) a]))]
[call-with-output-file (-poly (a)
(cl->
[(-String (-Port . -> . a)) a]
[(-String (-Port . -> . a) Sym) a]))]
[current-output-port (-Param -Output-Port -Output-Port)]
[current-error-port (-Param -Output-Port -Output-Port)]
[current-input-port (-Param -Input-Port -Input-Port)]
[round (N . -> . N)]
[seconds->date (N . -> . (make-Struct 'date #f (list N N N N N N N N B N) #f))]
[current-seconds (-> N)]
[sqrt (-> N N)]
[path->string (-> -Path -String)]
[link-exists? (-> -Pathlike B)]
[directory-exists? (-> -Pathlike B)]
[file-exists? (-> -Pathlike B)]
[directory-list (cl-> [() (-lst -Path)]
[(-Path) (-lst -Path)])]
[make-hash-table (let ([ht-opt (*Un (-val 'weak) (-val 'equal))])
(-poly (a b)
(cl-> [() (-HT a b)]
[(ht-opt) (-HT a b)]
[(ht-opt ht-opt) (-HT a b)])))]
[hash-table-put! (-poly (a b) ((-HT a b) a b . -> . -Void))]
[hash-table-map (-poly (a b c) ((-HT a b) (a b . -> . c) . -> . (-lst c)))]
[hash-table-get (-poly (a b c)
(cl->
(((-HT a b) a) b)
(((-HT a b) a (-> c)) (*Un b c))
(((-HT a b) a c) (*Un b c))))]
#;[hash-table-index (-poly (a b) ((-HT a b) a b . -> . -Void))]
[bytes (->* (list) N -Bytes)]
[bytes-ref (-> -Bytes N N)]
[bytes-append (->* (list -Bytes) -Bytes -Bytes)]
[subbytes (cl->
[(-Bytes N) -Bytes]
[(-Bytes N N) -Bytes])]
[bytes-length (-> -Bytes N)]
[open-input-file (-> -Pathlike -Input-Port)]
[close-input-port (-> -Input-Port -Void)]
[close-output-port (-> -Output-Port -Void)]
[read-line (cl->
[() -String]
[(-Input-Port) -String]
[(-Input-Port Sym) -String])]
[copy-file (-> -Pathlike -Pathlike -Void)]
[bytes->string/utf-8 (-> -Bytes -String)]
;; language
[(expand #'(this-language))
Sym
string-constants/string-constant]
;; make-promise
[(cadr (syntax->list (expand #'(delay 3))))
(-poly (a) (-> (-> a) (-Promise a)))
scheme/promise]
;; qq-append
[(cadr (syntax->list (expand #'`(,@'() 1))))
(-poly (a b)
(cl->*
(-> (-lst a) (-val '()) (-lst a))
(-> (-lst a) (-lst b) (-lst (*Un a b)))))]
[force (-poly (a) (-> (-Promise a) a))]
[bytes<? (->* (list -Bytes) -Bytes B)]
[regexp-replace*
(cl->*
(-Pattern (*Un -Bytes -String) (*Un -Bytes -String) . -> . -Bytes)
(-Pattern -String -String . -> . -String))]
[peek-char
(cl->*
[-> -Char]
[-Input-Port . -> . -Char]
[-Input-Port N . -> . -Char]
[N . -> . -Char])]
[peek-byte
(cl->*
[-> -Byte]
[-Input-Port . -> . -Byte]
[-Input-Port N . -> . -Byte]
[N . -> . -Byte])]
[make-pipe
(cl->*
[-> (-values (list -Input-Port -Output-Port))]
[N . -> . (-values (list -Input-Port -Output-Port))])]
[open-output-bytes
(cl->*
[-> -Output-Port]
[Univ . -> . -Output-Port])]
[get-output-bytes
(cl->*
[-Output-Port . -> . -Bytes]
[-Output-Port Univ . -> . -Bytes]
[-Output-Port Univ N . -> . -Bytes]
[-Output-Port Univ N N . -> . -Bytes]
[-Output-Port N . -> . -Bytes]
[-Output-Port N N . -> . -Bytes])]
#;[exn:fail? (-> Univ B)]
#;[exn:fail:read? (-> Univ B)]
[write (-> -Sexp -Void)]
[open-output-string (-> -Output-Port)]
;; FIXME - wrong
[get-output-string (-> -Output-Port -String)]
[make-directory (-> -Path -Void)]
[hash-table-for-each (-poly (a b c)
(-> (-HT a b) (-> a b c) -Void))]
[delete-file (-> -Pathlike -Void)]
[make-namespace (cl->* (-> -Namespace)
(-> (*Un (-val 'empty) (-val 'initial)) -Namespace))]
[eval (-> -Sexp Univ)]
[exit (-> (Un))]
;; syntax operations
[syntax-source (-poly (a) (-> (-Syntax a) Univ))]
[syntax-position (-poly (a) (-> (-Syntax a) (-opt N)))]
[datum->syntax (cl->*
(-> (-opt (-Syntax Univ)) Sym (-Syntax Sym))
(-> (-opt (-Syntax Univ)) Univ (-Syntax Univ)))]
[syntax->datum (-poly (a) (-> (-Syntax a) Univ))]
[syntax-e (-poly (a) (-> (-Syntax a) a))]
[syntax-original? (-poly (a) (-> (-Syntax a) B))]
[identifier? (make-pred-ty (-Syntax Sym))]
[syntax? (make-pred-ty (-Syntax Univ))]
[syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a))
(-> (-Syntax Univ) Univ Univ)))]
)))
(begin-for-syntax (initialize-type-env initial-env)
(initialize-others))
;; the initial type name environment - just the base types
(define-syntax (define-tname-env stx)
(syntax-case stx ()
[(_ var provider [nm ty] ...)
#`(begin
(define-syntax nm (lambda (stx) (raise-syntax-error 'type-check "type name used out of context" stx))) ...
(provide nm) ...
(define-syntax provider (lambda (stx) #'(begin (provide nm) ...)))
(provide provider)
(begin-for-syntax
(initialize-type-name-env
(list (list #'nm ty) ...))))]))
(define-syntax (define-other-types stx)
(syntax-case stx ()
[(_ provider requirer nm ...)
(with-syntax ([(nms ...) (generate-temporaries #'(nm ...))])
(let ([body-maker (lambda (stx)
(map (lambda (nm nms) (datum->syntax stx `(rename ,#'mod ,nm ,nms)))
(syntax->list #'(nm ...))
(syntax->list #'(nms ...))))])
#'(begin (define-syntax nms (lambda (stx) (raise-syntax-error 'type-check "type name used out of context" stx))) ...
(provide nms) ...
(define-syntax (requirer stx)
(syntax-case stx ()
[(_ mod)
(datum->syntax
stx
`(require . ,(map (lambda (nm* nms*) (datum->syntax stx `(rename ,#'mod ,nm* ,nms*)))
(list 'nm ...)
(list #'nms ...))))]))
(define-syntax provider (lambda (stx) #'(begin (provide (rename-out [nms nm])) ...)))
(provide provider requirer))))]))
;; the initial set of available type names
(define-tname-env initial-type-names provide-tnames
[Number N]
[Integer -Integer]
[Void -Void]
[Boolean B]
[Symbol Sym]
[String -String]
[Any Univ]
[Port -Port]
[Path -Path]
[Regexp -Regexp]
[PRegexp -PRegexp]
[Char -Char]
[Option (-poly (a) (-opt a))]
[List (-lst Univ)]
[Listof -Listof]
[Namespace -Namespace]
[Input-Port -Input-Port]
[Output-Port -Output-Port]
[Bytes -Bytes]
[EOF (-val eof)]
[Keyword -Keyword]
[HashTable (-poly (a b) (-HT a b))]
[Promise (-poly (a) (-Promise a))]
[Pair (-poly (a b) (-pair a b))]
[Box (-poly (a) (make-Box a))]
[Syntax Any-Syntax]
[Identifier Ident]
)
(define-other-types
provide-extra-tnames
require-extra-tnames
-> U mu Un All Opaque Vectorof
Parameter Tuple Class
)
(provide-extra-tnames)

9
collects/typed-scheme/private/extra-procs.ss Normal file
View File

@ -0,0 +1,9 @@
(module extra-procs mzscheme
(provide assert)
(define (assert v)
(unless v
(error "Assertion failed - value was #f"))
v)
)

52
collects/typed-scheme/private/mutated-vars.ss Normal file
View File

@ -0,0 +1,52 @@
(module mutated-vars mzscheme
(require-for-template mzscheme)
(require (lib "boundmap.ss" "syntax")
(lib "kerncase.ss" "syntax")
(lib "trace.ss"))
;; mapping telling whether an identifer is mutated
;; maps id -> boolean
(define table (make-module-identifier-mapping))
;; find and add to mapping all the set!'ed variables in form
;; syntax -> void
(define (find-mutated-vars form)
;; syntax -> void
(define (fmv/list lstx)
(for-each find-mutated-vars (syntax->list lstx)))
;(printf "called with ~a~n" (syntax-object->datum form))
(kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal require/typed-internal #%app lambda)
;; what we care about: set!
[(set! v e)
(begin
;(printf "mutated var found: ~a~n" (syntax-e #'v))
(module-identifier-mapping-put! table #'v #t))]
[(define-values (var ...) expr)
(find-mutated-vars #'expr)]
[(#%app . rest) (fmv/list #'rest)]
[(begin . rest) (fmv/list #'rest)]
[(begin0 . rest) (fmv/list #'rest)]
[(lambda _ . rest) (fmv/list #'rest)]
[(case-lambda (_ . rest) ...) (for-each fmv/list (syntax->list #'(rest ...)))]
[(if e1 e2) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e2))]
[(if e1 e2 e3) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e1) (find-mutated-vars #'e3))]
[(with-continuation-mark e1 e2 e3) (begin (find-mutated-vars #'e1)
(find-mutated-vars #'e1)
(find-mutated-vars #'e3))]
[(let-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
(fmv/list #'b))]
[(letrec-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
(fmv/list #'b))]
;; all the other forms don't have any expression subforms (like #%top)
[_ (void)]))
;(trace find-mutated-vars)
;; checks to see if a particular variable is ever set!'d
;; is-var-mutated? : identifier -> boolean
(define (is-var-mutated? id) (module-identifier-mapping-get table id (lambda _ #f)))
(provide find-mutated-vars is-var-mutated?)
)

210
collects/typed-scheme/private/parse-type.ss Normal file
View File

@ -0,0 +1,210 @@
#lang scheme/base
(provide parse-type parse-type/id)
(require (except-in "type-rep.ss" make-arr)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"tc-utils.ss"
"union.ss"
(lib "stx.ss" "syntax")
(except-in "type-environments.ss")
"type-name-env.ss"
"type-alias-env.ss"
"type-utils.ss"
(only-in (lib "list.ss") foldl foldr)
#;(except-in (lib "list.ss" "srfi" "1") unfold remove)
(lib "plt-match.ss"))
(define enable-mu-parsing (make-parameter #t))
(define (parse-type/id loc datum)
#;(printf "parse-type/id id : ~a~n ty: ~a~n" (syntax-object->datum loc) (syntax-object->datum stx))
(let* ([stx* (datum->syntax loc datum loc loc)])
(parse-type stx*)))
(define (stx-cadr stx) (stx-car (stx-cdr stx)))
(define (parse-type stx)
(parameterize ([current-orig-stx stx])
(syntax-case* stx ()
symbolic-identifier=?
[(fst . rst)
(not (syntax->list #'rst))
(-pair (parse-type #'fst) (parse-type #'rst))]
[(Class (pos-args ...) ([fname fty . rest] ...) ([mname mty] ...))
(eq? (syntax-e #'Class) 'Class)
(make-Class
(map parse-type (syntax->list #'(pos-args ...)))
(map list
(map syntax-e (syntax->list #'(fname ...)))
(map parse-type (syntax->list #'(fty ...)))
(map (lambda (e) (syntax-case e ()
[(#t) #t]
[_ #f]))
(syntax->list #'(rest ...))))
(map list
(map syntax-e (syntax->list #'(mname ...)))
(map parse-type (syntax->list #'(mty ...)))))]
[(Instance t)
(eq? (syntax-e #'Instance) 'Instance)
(let ([v (parse-type #'t)])
(unless (or (Mu? v) (Class? v) (Union? v))
(tc-error "Argument to Instance must be a class type, got ~a" v))
(make-Instance v))]
[(Tuple ts ...)
(or (eq? (syntax-e #'Tuple) 'Tuple)
(eq? (syntax-e #'Tuple) 'List))
(begin
(add-type-name-reference (stx-car stx))
(-Tuple (map parse-type (syntax->list #'(ts ...)))))]
[(cons fst rst)
(eq? (syntax-e #'cons) 'cons)
(-pair (parse-type #'fst) (parse-type #'rst))]
[(pred t)
(eq? (syntax-e #'pred) 'pred)
(make-pred-ty (parse-type #'t))]
[(dom -> rng : pred-ty)
(and
(eq? (syntax-e #'->) '->)
(eq? (syntax-e #':) ':))
(begin
(add-type-name-reference (stx-cadr stx))
(make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (parse-type #'pred-ty)))]
[(dom ... rest ::: -> rng)
(and (eq? (syntax-e #'->) '->)
(or (symbolic-identifier=? #'::: (quote-syntax ..))
(symbolic-identifier=? #'::: (quote-syntax ...))))
(begin
(add-type-name-reference #'->)
(->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-type #'rng)))]
;; has to be below the previous one
[(dom ... -> rng)
(eq? (syntax-e #'->) '->)
(begin
(add-type-name-reference #'->)
(->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rng)))]
[(values tys ...)
(eq? (syntax-e #'values) 'values)
(-values (map parse-type (syntax->list #'(tys ...))))]
[(case-lambda tys ...)
(eq? (syntax-e #'case-lambda) 'case-lambda)
(make-Function (map (lambda (ty)
(syntax-case* ty (->) symbolic-identifier=?
[(dom ... -> rng)
(make-arr
(map parse-type (syntax->list #'(dom ...)))
(parse-type #'rng))]))
(syntax->list #'(tys ...))))]
;; I wish I could write this
#;[(case-lambda ([dom ... -> rng] ...)) (make-funty (list (make-arr (list (parse-type #'dom) ...) (parse-type #'rng)) ...))]
#;[(list-of t) (make-lst (parse-type #'t))]
#;[(Listof t) (make-lst (parse-type #'t))]
[(Vectorof t)
(eq? (syntax-e #'Vectorof) 'Vectorof)
(begin
(add-type-name-reference #'Vectorof)
(make-Vector (parse-type #'t)))]
[(mu x t)
(and (identifier? #'x)
(memq (syntax-e #'mu) '(mu Rec))
(enable-mu-parsing))
(let* ([var (syntax-e #'x)]
[tvar (make-F var)])
(add-type-name-reference #'mu)
(parameterize ([current-tvars (extend-env (list var) (list tvar) (current-tvars))])
(make-Mu var (parse-type #'t))))]
[(U ts ...)
(eq? (syntax-e #'U) 'U)
(begin
(add-type-name-reference #'U)
(apply Un (map parse-type (syntax->list #'(ts ...)))))]
[(Un-pat ts ...)
(eq? (syntax-e #'Un-pat) 'Un)
(apply Un (map parse-type (syntax->list #'(ts ...))))]
[(quot t)
(eq? (syntax-e #'quot) 'quote)
(-val (syntax-e #'t))]
[(All (vars ...) t)
(and (eq? (syntax-e #'All) 'All)
(andmap identifier? (syntax->list #'(vars ...))))
(let* ([vars (map syntax-e (syntax->list #'(vars ...)))]
[tvars (map make-F vars)])
(add-type-name-reference #'All)
(parameterize ([current-tvars (extend-env vars tvars (current-tvars))])
(make-Poly vars (parse-type #'t))))]
[(Opaque p?)
(eq? (syntax-e #'Opaque) 'Opaque)
(begin
(add-type-name-reference #'Opaque)
(make-Opaque #'p? (syntax-local-certifier)))]
[(Parameter t)
(eq? (syntax-e #'Parameter) 'Parameter)
(let ([ty (parse-type #'t)])
(add-type-name-reference #'Parameter)
(-Param ty ty))]
[(Parameter t1 t2)
(eq? (syntax-e #'Parameter) 'Parameter)
(begin
(add-type-name-reference #'Parameter)
(-Param (parse-type #'t1) (parse-type #'t2)))]
[id
(identifier? #'id)
(cond
;; if it's a type variable, we just produce the corresponding reference (which is in the HT)
[(lookup (current-tvars) (syntax-e #'id) (lambda (_) #f))]
;; if it's a type alias, we expand it (the expanded type is stored in the HT)
[(lookup-type-alias #'id parse-type (lambda () #f))
=>
(lambda (t)
(add-type-name-reference #'id)
t)]
;; if it's a type name, we just use the name
[(lookup-type-name #'id (lambda () #f))
(add-type-name-reference #'id)
(make-Name #'id)]
[else
(tc-error "unbound type ~a" (syntax-e #'id))])]
[(All . rest) (eq? (syntax-e #'All) 'All) (tc-error "All: bad syntax")]
[(Opaque . rest) (eq? (syntax-e #'Opaque) 'Opqaue) (tc-error "Opaque: bad syntax")]
[(U . rest) (eq? (syntax-e #'U) 'U) (tc-error "Union: bad syntax")]
[(Vectorof . rest) (eq? (syntax-e #'Vectorof) 'Vectorof) (tc-error "Vectorof: bad syntax")]
[(mu . rest) (eq? (syntax-e #'mu) 'mu) (tc-error "mu: bad syntax")]
[(Un . rest) (eq? (syntax-e #'Un) 'Un) (tc-error "Union: bad syntax")]
[(t ... -> . rest) (eq? (syntax-e #'->) '->) (tc-error "->: bad syntax")]
[(id arg args ...)
(let loop
([rator (parse-type #'id)]
[args (map parse-type (syntax->list #'(arg args ...)))])
(match rator
[(Name: _)
(make-App rator args stx)]
[(Poly: ns _)
(unless (= (length args) (length ns))
(tc-error "Wrong number of arguments to type ~a, expected ~a but got ~a" rator (length ns) (length args)))
(instantiate-poly rator args)]
[(Mu: _ _) (loop (unfold rator) args)]
[_ (tc-error "Type ~a cannot be applied, arguments were: ~a" rator args)]))
#;
(let ([ty (parse-type #'id)])
#;(printf "ty is ~a" ty)
(unless (Poly? ty)
(tc-error "not a polymorphic type: ~a" (syntax-e #'id)))
(unless (= (length (syntax->list #'(arg args ...))) (Poly-n ty))
(tc-error "wrong number of arguments to type constructor ~a: expected ~a, got ~a"
(syntax-e #'id)
(Poly-n ty)
(length (syntax->list #'(arg args ...)))))
(instantiate-poly ty (map parse-type (syntax->list #'(arg args ...)))))]
[t
(or (boolean? (syntax-e #'t)) (number? (syntax-e #'t))
(string? (syntax-e #'t)))
(-val (syntax-e #'t))]
[_ (tc-error "not a valid type: ~a" (syntax->datum stx))])))

335
collects/typed-scheme/private/prims.ss Normal file
View File

@ -0,0 +1,335 @@
#lang scheme/base
#|
This file defines two sorts of primitives. All of them are provided into any module using the typed scheme language.
1. macros for defining type annotated code.
this includes: lambda:, define:, etc
potentially, these macros should be replacements for the mzscheme ones in the user program
however, it's nice to be able to use both when the sugar is more limited
for example: (define ((f x) y) (+ x y))
2. macros for defining 'magic' code
examples: define-typed-struct, require/typed
these expand into (ignored) mzscheme code, and declarations that a typechecker understands
in order to protect the declarations, they are wrapped in `#%app void' so that local-expand of the module body
will not expand them on the first pass of the macro expander (when the stop list is ignored)
|#
(provide (all-defined-out))
(require (for-syntax
scheme/base
"type-rep.ss"
(lib "match.ss")
"parse-type.ss"
(lib "struct.ss" "syntax")
(lib "stx.ss" "syntax")
"utils.ss"
"tc-utils.ss"
"type-name-env.ss"
"type-contract.ss"))
(require "require-contract.ss"
"internal-forms.ss"
"planet-requires.ss"
(lib "etc.ss")
(except-in (lib "contract.ss") ->)
(only-in (lib "contract.ss") [-> c->])
(lib "struct.ss")
"base-env.ss")
(define-for-syntax (ignore stx) (syntax-property stx 'typechecker:ignore #t))
(define-for-syntax (internal stx)
(quasisyntax/loc stx
(define-values ()
(begin
(quote-syntax #,stx)
(#%plain-app values)))))
(define-syntax (require/typed stx)
(syntax-case* stx (rename) (lambda (x y) (eq? (syntax-e x) (syntax-e y)))
[(_ lib [nm ty] ...)
#'(begin (require/typed nm ty lib) ...)]
[(_ nm ty lib)
(identifier? #'nm)
(quasisyntax/loc stx (begin
#,(syntax-property (syntax-property #'(define cnt* #f)
'typechecker:contract-def #'ty)
'typechecker:ignore #t)
#,(internal #'(require/typed-internal nm ty))
#,(syntax-property #'(require/contract nm cnt* lib)
'typechecker:ignore #t)))]
[(_ (rename internal-nm nm) ty lib)
(raise-syntax-error "rename not currently supported" stx)
#; #;
(identifier? #'nm)
(quasisyntax/loc stx (begin
#,(syntax-property (syntax-property #'(define cnt* #f)
'typechecker:contract-def #'ty)
'typechecker:ignore #t)
#,(internal #'(require/typed-internal internal-nm ty))
#,(syntax-property #'(require/contract nm cnt* lib)
'typechecker:ignore #t)))]))
(define-syntax (require/opaque-type stx)
(syntax-case stx ()
[(_ ty pred lib)
(and (identifier? #'ty) (identifier? #'pred))
(begin
(register-type-name #'ty (make-Opaque #'pred (syntax-local-certifier)))
(quasisyntax/loc stx
(begin
#,(syntax-property #'(define pred-cnt (any/c . c-> . boolean?))
'typechecker:ignore #t)
#,(internal #'(require/typed-internal pred (Any -> Boolean : (Opaque pred))))
(define-type-alias ty (Opaque pred))
#,(syntax-property #'(require/contract pred pred-cnt lib)
'typechecker:ignore #t))))]))
(define-for-syntax (types-of-formals stx src)
(syntax-case stx (:)
[([var : ty] ...) (quasisyntax/loc stx (ty ...))]
[([var : ty] ... . [rest : rest-ty]) (syntax/loc stx (ty ... rest-ty ..))]
[_
(let loop ([stx stx])
(syntax-case stx ()
;; should never happen
[() (raise-syntax-error #f "bad annotation syntax" src stx)]
[([var : ty] . rest)
(identifier? #'var)
(loop #'rest)]
[([var : ty] . rest)
(raise-syntax-error #f "not a variable" src #'var)]
[(e . rest)
(raise-syntax-error #f "expected annotated variable of the form [x : T], got something else" src #'e)]))]))
(define-syntax (plambda: stx)
(syntax-case stx ()
[(plambda: (tvars ...) formals . body)
(syntax-property #'(lambda: formals . body)
'typechecker:plambda
#'(tvars ...))]))
(define-syntax (pcase-lambda: stx)
(syntax-case stx ()
[(pcase-lambda: (tvars ...) cl ...)
(syntax-property #'(case-lambda: cl ...)
'typechecker:plambda
#'(tvars ...))]))
(define-syntax (pdefine: stx)
(syntax-case stx (:)
[(pdefine: tvars (nm . formals) : ret-ty . body)
(with-syntax* ([(tys ...) (types-of-formals #'formals stx)]
[type (syntax/loc #'ret-ty (All tvars (tys ... -> ret-ty)))])
(syntax/loc stx
(define: nm : type
(plambda: tvars formals . body))))]))
(define-syntax (ann stx)
(syntax-case stx (:)
[(_ arg : ty)
#;#'(let: ([id : ty arg]) id)
(syntax-property #'arg 'type-ascription #'ty)]))
(define-syntax (: stx)
(let ([stx*
;; make it possible to add another colon after the id for clarity
(syntax-case stx (:)
[(: id : . more) (syntax/loc stx (: id . more))]
[_ stx])])
(syntax-case stx* ()
[(_ id ty)
(identifier? #'id)
(syntax-property
(internal (syntax/loc stx (:-internal id ty)))
'disappeared-use #'id)]
[(_ id ty)
(raise-syntax-error '|type declaration| "can only annotate identifiers with types"
stx #'id)]
[(_ _ _ _ . _)
(raise-syntax-error '|type declaration| "too many arguments" stx)]
[(_ _)
(raise-syntax-error '|type declaration| "too few arguments" stx)])))
(define-syntax (inst stx)
(syntax-case stx (:)
[(_ arg : tys ...)
(syntax-property #'arg 'type-inst #'(tys ...))]))
(define-syntax (define: stx)
(syntax-case stx (:)
[(define: (nm . formals) : ret-ty body ...)
(identifier? #'nm)
(with-syntax* ([(tys ...) (types-of-formals #'formals stx)]
[arrty (syntax/loc stx (tys ... -> ret-ty))])
(syntax/loc stx
(define: nm : arrty
(lambda: formals body ...))))]
[(define: nm : ty body)
(identifier? #'nm)
(with-syntax ([new-nm (syntax-property #'nm 'type-label #'ty)])
(syntax/loc stx (define new-nm body)))]
[(define: (vars ...) (f args ...) : ret body ...)
(andmap identifier? (syntax->list #'(vars ...)))
#'(pdefine: (vars ...) (f args ...) : ret body ...)]
[(define: (nm . formals) body ...)
(raise-syntax-error #f "missing return type annotation" stx)]
[(define: nm body)
(raise-syntax-error #f "missing type annotation" stx)]))
;; helper function for annoating the bound names
(define-for-syntax (annotate-names stx)
(define (label-one var ty)
(syntax-property var 'type-label ty))
(define (label vars tys)
(map label-one
(syntax->list vars)
(syntax->list tys)))
(syntax-case stx (:)
[[var : ty] (label-one #'var #'ty)]
[([var : ty] ...)
(label #'(var ...) #'(ty ...))]
[([var : ty] ... . [rest : rest-ty])
(append (label #'(var ...) #'(ty ...)) (label-one #'rest #'rest-ty))]))
(define-syntax-rule (λ: . args) (lambda: . args))
(define-syntax (lambda: stx)
(syntax-case stx (:)
[(lambda: formals . body)
(with-syntax ([labeled-formals (annotate-names #'formals)])
(syntax/loc stx (lambda labeled-formals . body)))]))
(define-syntax (case-lambda: stx)
(syntax-case stx (:)
[(case-lambda: [formals . body] ...)
(with-syntax ([(lab-formals ...) (map annotate-names (syntax->list #'(formals ...)))])
(syntax/loc stx (case-lambda [lab-formals . body] ...)))]))
(define-syntaxes (let-internal: let*: letrec:)
(let ([mk (lambda (form)
(lambda (stx)
(syntax-case stx (:)
[(_ ([nm : ty . exprs] ...) . body)
(with-syntax* ([(vars ...) (annotate-names #'([nm : ty] ...))]
[bindings (map (lambda (v e loc)
(quasisyntax/loc loc [#,v . #,e]))
(syntax->list #'(vars ...))
(syntax->list #'(exprs ...))
(syntax->list (syntax-case stx () [(_ bs . body) #'bs])))])
(quasisyntax/loc stx (#,form bindings . body)))])))])
(values (mk #'let) (mk #'let*) (mk #'letrec))))
(define-syntax (let: stx)
(syntax-case stx (:)
[(let: nm : ret-ty ([arg : ty val] ...) . body)
(identifier? #'nm)
(syntax/loc stx ((letrec: ([nm : (ty ... -> ret-ty) (lambda: ([arg : ty] ...) . body)]) nm) val ...))]
[(let: . rest)
(syntax/loc stx (let-internal: . rest))]))
(define-syntax (define-type-alias stx)
(syntax-case stx ()
[(_ tname rest)
(identifier? #'tname)
(begin
#`(begin
#,(ignore #'(define-syntax tname (lambda (stx) (raise-syntax-error 'type-check "type name used out of context" stx))))
#,(internal (syntax/loc stx (define-type-alias-internal tname rest)))))]
[(_ (tname . args) rest)
(andmap identifier? (syntax->list #'args))
#'(define-type-alias tname (All args rest))]))
(define-syntax (define-typed-struct/exec stx)
(syntax-case stx (:)
[(_ nm ([fld : ty] ...) [proc : proc-ty])
(with-syntax*
([proc* (syntax-property #'(ann proc : proc-ty) 'typechecker:with-type #t)]
[d-s (syntax-property (syntax/loc stx (define-struct/properties nm (fld ...)
([prop:procedure proc*])))
'typechecker:ignore-some #t)]
[dtsi (internal (syntax/loc stx (define-typed-struct/exec-internal nm ([fld : ty] ...) proc-ty)))])
#'(begin d-s dtsi))]))
(define-syntax (with-handlers: stx)
(syntax-case stx ()
[(_ ([pred? action] ...) . body)
(with-syntax ([(pred?* ...) (map (lambda (s) (syntax-property #`(ann #,s : (Any -> Any)) 'typechecker:with-type #t))
(syntax->list #'(pred? ...)))]
[(action* ...)
(map (lambda (s) (syntax-property s 'typechecker:exn-handler #t)) (syntax->list #'(action ...)))]
[body* (syntax-property #'(begin . body) 'typechecker:exn-body #t)])
(syntax-property #'(with-handlers ([pred?* action*] ...) body*)
'typechecker:with-handlers
#t))]))
(define-syntax (define-typed-struct stx)
(syntax-case stx (:)
[(_ nm ([fld : ty] ...) . opts)
(with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts))
'typechecker:ignore #t)]
[dtsi (internal (syntax/loc stx (define-typed-struct-internal nm ([fld : ty] ...))))])
#'(begin d-s dtsi))]
[(_ (vars ...) nm ([fld : ty] ...) . opts)
(with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts))
'typechecker:ignore #t)]
[dtsi (internal (syntax/loc stx (define-typed-struct-internal (vars ...) nm ([fld : ty] ...))))])
#'(begin d-s dtsi))]))
(define-syntax (require-typed-struct stx)
(syntax-case stx (:)
[(_ nm ([fld : ty] ...) lib)
(with-syntax* ([(struct-info maker pred sel ...) (build-struct-names #'nm (syntax->list #'(fld ...)) #f #t)]
[oty #'(Opaque pred)])
#'(begin
(require/opaque-type nm pred lib)
(require/typed maker (ty ... -> oty) lib)
(require/typed sel (oty -> ty) lib) ...))]))
(define-syntax (do: stx)
(syntax-case stx (:)
[(_ : ty ((var : tys init . step) ...) (e0 e1 ...) c ...)
(with-syntax ([(step ...)
(map (lambda (v s)
(syntax-case s ()
[() v]
[(e) #'e]
[_ (raise-syntax-error
#f
"bad variable syntax"
stx)]))
(syntax->list #'(var ...))
(syntax->list #'(step ...)))])
(syntax-case #'(e1 ...) ()
[() (syntax/loc
stx
(let: doloop : ty ([var : tys init] ...)
(if (not e0)
(begin c ... (doloop step ...)))))]
[(e1 e2 ...)
(syntax/loc
stx
(let: doloop : ty ([var : tys init] ...)
(if e0
(begin e1 e2 ...)
(begin c ... (doloop step ...)))))]))]))

96
collects/typed-scheme/private/remove-intersect.ss Normal file
View File

@ -0,0 +1,96 @@
#lang scheme/base
(require "type-rep.ss" "unify.ss" "union.ss" "infer.ss" "subtype.ss"
"type-utils.ss" "resolve-type.ss" "type-effect-convenience.ss"
mzlib/plt-match mzlib/trace)
(provide restrict (rename-out [*remove remove]) overlap)
(define (overlap t1 t2)
(match (list t1 t2)
[(list (Univ:) _) #t]
[(list _ (Univ:)) #t]
[(list (F: _) _) #t]
[(list _ (F: _)) #t]
[(list (Name: n) (Name: n*)) (free-identifier=? n n*)]
[(list (? Mu?) _) (overlap (unfold t1) t2)]
[(list _ (? Mu?)) (overlap t1 (unfold t2))]
[(list (Union: e) t)
(ormap (lambda (t*) (overlap t* t)) e)]
[(list t (Union: e))
(ormap (lambda (t*) (overlap t t*)) e)]
[(or (list _ (? Poly?)) (list (? Poly?) _))
#t] ;; these can have overlap, conservatively
[(list (Base: s1) (Base: s2)) (eq? s1 s2)]
[(list (Base: _) (Value: _)) (subtype t2 t1)] ;; conservative
[(list (Value: _) (Base: _)) (subtype t1 t2)] ;; conservative
[(list (Syntax: t) (Syntax: t*))
(overlap t t*)]
[(or (list (Syntax: _) _)
(list _ (Syntax: _)))
#f]
[(list (Base: _) _) #f]
[(list _ (Base: _)) #f]
[(list (Value: (? pair? v)) (Pair: _ _)) #t]
[(list (Pair: _ _) (Value: (? pair? v))) #t]
[(list (Pair: a b) (Pair: a* b*))
(and (overlap a a*)
(overlap b b*))]
[(or (list (Pair: _ _) _)
(list _ (Pair: _ _)))
#f]
[else #t]))
;; this is *definitely* not yet correct
;; NEW IMPL
;; restrict t1 to be a subtype of t2
(define (restrict t1 t2)
;; we don't use union map directly, since that might produce too many elements
(define (union-map f l)
(match l
[(Union: es)
(let ([l (map f es)])
;(printf "l is ~a~n" l)
(apply Un l))]))
(cond
[(subtype t1 t2) t1] ;; already a subtype
[(match t2
[(Poly: vars t)
(let ([subst (infer t t1 vars)])
(and subst (restrict t1 (subst-all subst t1))))]
[_ #f])]
[(Union? t1) (union-map (lambda (e) (restrict e t2)) t1)]
[(Mu? t1)
(restrict (unfold t1) t2)]
[(Mu? t2) (restrict t1 (unfold t2))]
[(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1
[(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
[else t2] ;; t2 and t1 have a complex relationship, so we punt
))
;(trace restrict)
;; also not yet correct
;; produces old without the contents of rem
(define (*remove old rem)
(define initial
(if (subtype old rem)
(Un) ;; the empty type
(match (list old rem)
[(list (or (App: _ _ _) (Name: _)) t)
;; must be different, since they're not subtypes
;; and n must refer to a distinct struct type
old]
[(list (Union: l) rem)
(apply Un (map (lambda (e) (*remove e rem)) l))]
[(list (? Mu? old) t) (*remove (unfold old) t)]
[(list (Poly: vs b) t) (make-Poly vs (*remove b rem))]
[_ old])))
(if (subtype old initial) old initial))
;(trace *remove)
;(trace restrict)

40
collects/typed-scheme/private/require-contract.ss Normal file
View File

@ -0,0 +1,40 @@
#lang scheme/base
(require scheme/contract (for-syntax scheme/base syntax/kerncase))
(provide require/contract define-ignored)
(define-syntax (define-ignored stx)
(syntax-case stx ()
[(_ name expr)
(syntax-case (local-expand/capture-lifts #'expr 'expression
(list #'define-values))
(begin define-values)
[(begin (define-values (n) e) e*)
#'(begin (define-values (n) e)
(define name e*))]
[e #'(define name e)])]))
(define-syntax (require/contract stx)
(syntax-case stx ()
[(require/contract nm cnt lib)
#`(begin (require (only-in lib [nm tmp]))
(define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen #'#,stx)))]))
#|
(module a mzscheme
(provide x)
(define (x a) 'hi))
(module z mzscheme
(require require-contract)
(require (lib "contract.ss"))
(define-struct b (X Y))
(require/contract x (b? . -> . b?) a )
(x 'no)
)
(require z)
|#

79
collects/typed-scheme/private/resolve-type.ss Normal file
View File

@ -0,0 +1,79 @@
#lang scheme/base
(require "type-rep.ss" "type-name-env.ss" "tc-utils.ss"
"type-utils.ss"
mzlib/plt-match
mzlib/trace)
(provide resolve-name resolve-app needs-resolving? resolve-once)
(define (resolve-name t)
(match t
[(Name: n) (lookup-type-name n)]
[_ (int-err "resolve-name: not a name ~a" t)]))
(define (resolve-app rator rands stx)
(parameterize ([current-orig-stx stx])
(match rator
[(Poly: _ _)
(instantiate-poly rator rands)]
[(Name: _) (resolve-app (resolve-name rator) rands stx)]
[(Mu: _ _) (resolve-app (unfold rator) rands)]
[(App: r r* s) (resolve-app (resolve-app r r* s) rands)]
[_ (tc-error "resolve-app: not a proper operator ~a" rator)])))
(define (needs-resolving? t)
(or (Mu? t) (App? t) (Name? t)))
(define (resolve-once t)
(match t
[(Mu: _ _) (unfold t)]
[(App: r r* s) (resolve-app r r* s)]
[(Name: _) (resolve-name t)]))
#|
(define (resolve-tc-result tcr)
(match tcr
[(tc-result: t e1s e2s)
(ret (resolve-type t) (map resolve-effect e1s) (map resolve-effect e2s))]))
(define (resolve-effect* e)
(effect-case resolve-type resolve-effect e))
(define (resolve-type* t)
(define (int t)
(type-case resolve-type t
[#:Name stx (lookup-type-name stx)]
[#:Poly #:matcher Poly: names body (make-Poly names (resolve-type body))]
[#:Mu #:matcher Mu: name body (make-Mu name (resolve-type body))]
[#:App rator rands stx
(let ([rator (resolve-type rator)]
[rands (map resolve-type rands)])
(unless (Poly? rator)
(tc-error/stx stx "Cannot apply non-polymorphic type: ~a, arguments were: ~a" rator rands))
(instantiate-poly rator rands))]))
(let loop ([t (int t)])
(if (or (Name? t) (App? t))
(loop (resolve-type t))
t)))
(define table (make-hash-table))
(define (resolve-type t)
(hash-table-get table t
(lambda () (let ([v (resolve-type* t)])
(hash-table-put! table t v)
v))))
(define (resolve-effect t)
(hash-table-get table t
(lambda () (let ([v (resolve-effect* t)])
(hash-table-put! table t v)
v))))
;(trace resolve-type)
|#

272
collects/typed-scheme/private/subtype.ss Normal file
View File

@ -0,0 +1,272 @@
#lang scheme/base
(require "type-rep.ss" "unify.ss" "type-utils.ss"
"tc-utils.ss"
"effect-rep.ss"
"type-comparison.ss"
"resolve-type.ss"
"type-name-env.ss"
mzlib/plt-match
mzlib/trace)
;; exn representing failure of subtyping
;; s,t both types
(define-struct (exn:subtype exn:fail) (s t))
#;
(define-values (fail-sym exn:subtype?)
(let ([sym (gensym)])
(values sym (lambda (s) (eq? s sym)))))
;; inference failure - masked before it gets to the user program
(define-syntax fail!
(syntax-rules ()
[(_ s t) #;(raise fail-sym)
(raise (make-exn:subtype "subtyping failed" (current-continuation-marks) s t))
#;(error "inference failed" s t)]))
;; data structures for remembering things on recursive calls
(define (empty-set) '())
(define current-seen (make-parameter (empty-set)))
(define (seen-before s t) (cons (Type-seq s) (Type-seq t)))
(define (remember s t A) (cons (seen-before s t) A))
(define (seen? s t) (member (seen-before s t) (current-seen)))
;; is s a subtype of t?
;; type type -> boolean
(define (subtype s t)
(with-handlers
([exn:subtype? (lambda _ #f)])
(subtype* (current-seen) s t)))
;; are all the s's subtypes of all the t's?
;; [type] [type] -> boolean
(define (subtypes s t)
(with-handlers
([exn:subtype? (lambda _ #f)])
(subtypes* (current-seen) s t)))
;; subtyping under constraint set, but produces boolean result instead of raising exn
;; List[(cons Number Number)] type type -> maybe[List[(cons Number Number)]]
(define (subtype*/no-fail A s t)
(with-handlers
([exn:subtype? (lambda _ #f)])
(subtype* A s t)))
;; type type -> (does not return)
;; subtying fails
#;
(define (fail! s t) (raise (make-exn:subtype "subtyping failed" (current-continuation-marks) s t)))
;; check subtyping for two lists of types
;; List[(cons Number Number)] listof[type] listof[type] -> List[(cons Number Number)]
(define (subtypes* A ss ts)
(cond [(and (null? ss) (null? ts) A)]
[(or (null? ss) (null? ts)) (fail! ss ts)]
[(subtype* A (car ss) (car ts))
=>
(lambda (A*) (subtypes* A* (cdr ss) (cdr ts)))]
[else (fail! (car ss) (car ts))]))
;; check if s is a supertype of any element of ts
(define (supertype-of-one/arr A s ts)
(ormap (lambda (e) (arr-subtype*/no-fail A e s)) ts))
(define (sub-eff e1 e2)
(match (list e1 e2)
[(list e e) #t]
[(list (Latent-Restrict-Effect: t) (Latent-Restrict-Effect: t*))
(and (subtype t t*)
(subtype t* t))]
[(list (Latent-Remove-Effect: t) (Latent-Remove-Effect: t*))
(and (subtype t t*)
(subtype t* t))]
[else #f]))
;(trace sub-eff)
;; simple co/contra-variance for ->
(define (arr-subtype*/no-fail A0 s t)
(with-handlers
([exn:subtype? (lambda _ #f)])
(match (list s t)
;; top for functions is above everything
[(list _ (top-arr:)) A0]
[(list (arr: s1 s2 #f thn-eff els-eff) (arr: t1 t2 #f (or '() thn-eff) (or '() els-eff)))
(let ([A1 (subtypes* A0 t1 s1)])
(subtype* A1 s2 t2))]
[(list (arr: s1 s2 s3 thn-eff els-eff) (arr: t1 t2 t3 thn-eff* els-eff*))
(unless
(or (and (null? thn-eff*) (null? els-eff*))
(and (effects-equal? thn-eff thn-eff*)
(effects-equal? els-eff els-eff*))
(and (andmap sub-eff thn-eff thn-eff*)
(andmap sub-eff els-eff els-eff*)))
(fail! s t))
;; either the effects have to be the same, or the supertype can't have effects
(let ([A (subtypes*/varargs A0 t1 s1 s3)])
(if (not t3)
(subtype* A s2 t2)
(let ([A1 (subtype* A t3 s3)])
(subtype* A1 s2 t2))))]
[else
(fail! s t)])))
(define (subtypes/varargs args dom rst)
(with-handlers
([exn:subtype? (lambda _ #f)])
(subtypes*/varargs (empty-set) args dom rst)))
(define (subtypes*/varargs A0 argtys dom rst)
(let loop-varargs ([dom dom] [argtys argtys] [A A0])
(cond
[(and (null? dom) (null? argtys)) A]
[(null? argtys) (fail! argtys dom)]
[(and (null? dom) rst)
(cond [(subtype* A (car argtys) rst) => (lambda (A) (loop-varargs dom (cdr argtys) A))]
[else (fail! (car argtys) rst)])]
[(null? dom) (fail! argtys dom)]
[(subtype* A (car argtys) (car dom)) => (lambda (A) (loop-varargs (cdr dom) (cdr argtys) A))]
[else (fail! (car argtys) (car dom))])))
;(trace subtypes*/varargs)
;; the algorithm for recursive types transcribed directly from TAPL, pg 305
;; List[(cons Number Number)] type type -> List[(cons Number Number)]
;; potentially raises exn:subtype, when the algorithm fails
;; is s a subtype of t, taking into account constraints A
(define (subtype* A s t)
(parameterize ([match-equality-test type-equal?]
[current-seen A])
(if (seen? s t)
A
(let* ([A0 (remember s t A)])
(parameterize ([current-seen A0])
#;(match t
[(Name: n) (when (eq? 'heap (syntax-e n))
(trace subtype*))]
[_ #f])
(match (list s t)
;; subtyping is reflexive
[(list t t) A0]
;; univ is top
[(list _ (Univ:)) A0]
;; (Un) is bot
[(list _ (Union: (list))) (fail! s t)]
[(list (Union: (list)) _) A0]
;; value types
[(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
;; integers are numbers too
[(list (Base: 'Integer) (Base: 'Number)) A0]
;; values are subtypes of their "type"
[(list (Value: (? integer? n)) (Base: 'Integer)) A0]
[(list (Value: (? number? n)) (Base: 'Number)) A0]
[(list (Value: (? boolean? n)) (Base: 'Boolean)) A0]
[(list (Value: (? symbol? n)) (Base: 'Symbol)) A0]
[(list (Value: (? string? n)) (Base: 'String)) A0]
;; tvars are equal if they are the same variable
[(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
;; case-lambda
[(list (Function: arr1) (Function: arr2))
(when (null? arr1) (fail! s t))
(let loop-arities ([A* A0]
[arr2 arr2])
(cond
[(null? arr2) A*]
[(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
[else (fail! s t)]))]
;; recur structurally on pairs
[(list (Pair: a d) (Pair: a* d*))
(let ([A1 (subtype* A0 a a*)])
(and A1 (subtype* A1 d d*)))]
;; quantification over two types preserves subtyping
[(list (Poly: ns b1) (Poly: ms b2))
(=> unmatch)
(unless (= (length ns) (length ms))
(unmatch))
;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
(subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
;; use unification to see if we can use the polytype here
[(list (Poly: vs b) s)
(=> unmatch)
(if (unify1 s b) A0 (unmatch))]
[(list s (Poly: vs b))
(=> unmatch)
(if (null? (fv b)) (subtype* A0 s b) (unmatch))]
;; names are compared for equality:
[(list (Name: n) (Name: n*))
(=> unmatch)
(if (free-identifier=? n n*)
A0
(unmatch))]
;; just unfold the recursive types
[(list _ (? Mu?)) (subtype* A0 s (unfold t))]
[(list (? Mu?) _) (subtype* A0 (unfold s) t)]
;; for unions, we check the cross-product
[(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
[(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
;; subtyping on immutable structs is covariant
[(list (Struct: nm _ flds #f) (Struct: nm _ flds* #f))
(subtypes* A0 flds flds*)]
[(list (Struct: nm _ flds proc) (Struct: nm _ flds* proc*))
(subtypes* A0 (cons proc flds) (cons proc* flds*))]
;; subtyping on structs follows the declared hierarchy
[(list (Struct: nm (? Type? parent) flds proc) other)
;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
(subtype* A0 parent other)]
;; applications and names are structs too
[(list (App: (Name: n) args _) other)
(let ([t (lookup-type-name n)])
(unless (Type? t)
(fail! s t))
#;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other
(instantiate-poly t args))
(let ([v (subtype* A0 (instantiate-poly t args) other)])
#;(printf "val: ~a~n" v)
v))]
[(list (Name: n) other)
(let ([t (lookup-type-name n)])
;(printf "subtype: name: ~a ~a ~a~n" (syntax-e n) t other)
(if (Type? t)
(subtype* A0 t other)
(fail! s t)))]
;; Promises are covariant
[(list (Struct: 'Promise _ (list t) _) (Struct: 'Promise _ (list t*) _)) (subtype* A0 t t*)]
;; subtyping on values is pointwise
[(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
;; single values shouldn't actually happen, but they're just like the type
[(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
[(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
;; subtyping on other stuff
[(list (Syntax: t) (Syntax: t*))
(subtype* A0 t t*)]
[(list (Instance: t) (Instance: t*))
(subtype* A0 t t*)]
;; otherwise, not a subtype
[_ (fail! s t) (printf "failed")]))))))
(define (type-compare? a b)
(and (subtype a b) (subtype b a)))
(provide subtype type-compare? subtypes/varargs subtypes)
;(trace subtype*)
;(trace supertype-of-one/arr)
;(trace arr-subtype*/no-fail)
;(trace subtype-of-one)
;(trace subtype*/no-fail)
;(trace subtypes*)
;(trace subtype)
;(subtype (-> Univ B) (-> Univ Univ))
;(subtype (make-poly '(a) (make-tvar 'a)) (make-lst N))

92
collects/typed-scheme/private/type-annotation.ss Normal file
View File

@ -0,0 +1,92 @@
#lang scheme/base
(require "type-rep.ss" "parse-type.ss" "tc-utils.ss" "subtype.ss" "utils.ss" "union.ss" "resolve-type.ss"
"type-env.ss")
(require (lib "plt-match.ss"))
(provide type-annotation
get-type
get-type/infer
type-label-symbol
type-ascrip-symbol
check-type)
(define type-label-symbol 'type-label)
(define type-ascrip-symbol 'type-ascription)
(define (print-size stx)
(syntax-case stx ()
[(a . b) (begin
(printf/log "Annotation Sexp Pair ~n")
(print-size #'a)
(print-size #'b))]
[_ (printf/log "Annotation Sexp ~n" )]))
;; get the type annotation of this syntax
;; syntax -> Maybe[Type]
(define (type-annotation stx)
(define (pt prop)
(print-size prop)
(if (syntax? prop)
(parse-type prop)
(parse-type/id stx prop)))
(cond
[(syntax-property stx type-label-symbol) => pt]
[(syntax-property stx type-ascrip-symbol) => pt]
[(and (identifier? stx) (lookup-type stx (lambda () #f)))
=>
(lambda (t)
(maybe-finish-register-type stx)
t)]
[else #f]))
(define (log/ann stx ty)
(printf/log "Required Annotated Variable: ~a ~a~n" (syntax-e stx) ty))
(define (log/extra stx ty ty2)
(printf/log "Extra Annotated Variable: ~a ~a ~a~n" (syntax-e stx) ty ty2))
(define (log/noann stx ty)
(printf/log "Unannotated Variable: ~a ~a~n" (syntax-e stx) ty))
;; get the type annotation of this identifier, otherwise error
;; identifier -> Type
(define (get-type stx)
(parameterize
([current-orig-stx stx])
(cond
[(type-annotation stx) => (lambda (x)
(log/ann stx x)
x)]
[(not (syntax-original? stx))
(tc-error "untyped var: ~a" (syntax-e stx))]
[else
(tc-error "no type information on variable ~a" (syntax-e stx))])))
;; get the type annotations on this list of identifiers
;; if not all identifiers have annotations, return the supplied inferred type
;; list[identifier] type -> list[type]
(define (get-type/infer stxs e-type)
(match (list stxs e-type)
[(list '() (Values: '())) (list)]
[(list (list stx ...) (Values: (list ty ...)))
(map (lambda (stx ty)
(cond [(type-annotation stx) => (lambda (ann) (check-type stx ty ann) (log/extra stx ty ann) ann)]
[else (log/noann stx ty) ty]))
stx ty)]
[(list (list stx) ty)
(cond [(type-annotation stx) => (lambda (ann)
(check-type stx ty ann)
(log/extra stx ty ann)
(list ann))]
[else (log/noann stx ty) (list ty)])]
[else (int-err "wrong type arity - get-type/infer ~a ~a" stxs e-type)]))
;; check that e-type is compatible with ty in context of stx
;; otherwise, error
;; syntax type type -> void
(define (check-type stx e-type ty)
(let ([stx* (current-orig-stx)])
(parameterize ([current-orig-stx stx])
(unless (subtype e-type ty)
;(printf "orig-stx: ~a" (syntax->datum stx*))
(tc-error "Body had type:~n~a~nVariable had type:~n~a~n" e-type ty)))))

231
collects/typed-scheme/private/type-effect-convenience.ss Normal file
View File

@ -0,0 +1,231 @@
(module type-effect-convenience scheme/base
(require "type-rep.ss"
"effect-rep.ss"
mzlib/plt-match
"type-comparison.ss"
"type-effect-printer.ss"
"union.ss"
"subtype.ss"
"type-utils.ss"
(lib "list.ss")
scheme/promise
(prefix-in 1: srfi/1)
(for-syntax scheme/base))
(provide (all-defined-out))
(define (-vet id) (make-Var-True-Effect id))
(define (-vef id) (make-Var-False-Effect id))
(define -rem make-Remove-Effect)
(define -rest make-Restrict-Effect)
(define (var->type-eff eff)
(match eff
[(Var-True-Effect: v) (make-Remove-Effect (make-Value #f) v)]
[(Var-False-Effect: v) (make-Restrict-Effect (make-Value #f) v)]
[_ eff]))
(define ((add-var v) eff)
(match eff
[(Latent-Var-True-Effect:) (-vet v)]
[(Latent-Var-False-Effect:) (-vef v)]
[(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
[(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
[(True-Effect:) eff]
[(False-Effect:) eff]
[_ (error 'internal-tc-error "can't add var to effect ~a" eff)]))
(define-syntax ->
(syntax-rules (:)
[(_ dom ... rng)
(->* (list dom ...) rng)]
[(_ dom ... rng : eff1 eff2)
(->* (list dom ...) : eff1 eff2)]))
(define-syntax ->*
(syntax-rules (:)
[(_ dom rng)
(make-Function (list (make-arr* dom rng)))]
[(_ dom rst rng)
(make-Function (list (make-arr* dom rng rst)))]
[(_ dom rng : eff1 eff2)
(make-Function (list (make-arr* dom rng #f eff1 eff2)))]
[(_ dom rst rng : eff1 eff2)
(make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
(define-syntax cl->
(syntax-rules (:)
[(_ [(dom ...) rng] ...)
(make-Function (list (make-arr* (list dom ...) rng) ...))]
[(_ [(dom ...) rng : eff1 eff2] ...)
(make-Function (list (make-arr* (list dom ...) rng #f eff1 eff2) ...))]
[(_ [(dom ...) rng rst : eff1 eff2] ...)
(make-Function (list (make-arr* (list dom ...) rng rst eff1 eff2) ...))]))
(define (cl->* . args)
(define (funty-arities f)
(match f
[(Function: as) as]))
(make-Function (map car (map funty-arities args))))
(define make-arr*
(case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
[(dom rng rest) (make-arr dom rng rest (list) (list))]
[(dom rng rest eff1 eff2) (make-arr dom rng rest eff1 eff2)]))
(define (make-promise-ty t)
(make-Struct (string->uninterned-symbol "Promise") #f (list t) #f))
(define N (make-Base 'Number))
(define -Integer (make-Base 'Integer))
(define B (make-Base 'Boolean))
(define Sym (make-Base 'Symbol))
(define -Void (make-Base 'Void))
(define -Bytes (make-Base 'Bytes))
(define -Regexp (make-Base 'Regexp))
(define -PRegexp (make-Base 'PRegexp))
(define -Byte-Regexp (make-Base 'Byte-Regexp))
(define -Byte-PRegexp (make-Base 'Byte-PRegexp))
(define -String (make-Base 'String))
(define -Keyword (make-Base 'Keyword))
(define -Char (make-Base 'Char))
(define -Syntax make-Syntax)
(define -Prompt-Tag (make-Base 'Prompt-Tag))
(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set))
(define -Path (make-Base 'Path))
(define -Namespace (make-Base 'Namespace))
(define -Output-Port (make-Base 'Output-Port))
(define -Input-Port (make-Base 'Input-Port))
(define -HT make-Hashtable)
(define -Promise make-promise-ty)
(define Univ (make-Univ))
(define-syntax -v
(syntax-rules ()
[(_ x) (make-F 'x)]))
(define-syntax -poly
(syntax-rules ()
[(_ (vars ...) ty)
(let ([vars (-v vars)] ...)
(make-Poly (list 'vars ...) ty))]))
(define-syntax -mu
(syntax-rules ()
[(_ var ty)
(let ([var (-v var)])
(make-Mu 'var ty))]))
(define -values make-Values)
;; produce the appropriate type of a list of types
;; that is - if there is exactly one type, just produce it, otherwise produce a values-ty
;; list[type] -> type
(define (list->values-ty l)
(if (= 1 (length l)) (car l) (-values l)))
(define-syntax *Un
(syntax-rules ()
[(_ . args) (make-Union (list . args))]))
(define -pair make-Pair)
(define -base make-Base)
(define -struct make-Struct)
(define -val make-Value)
(define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
(define -lst make-Listof)
(define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
(define -Port (*Un -Input-Port -Output-Port))
(define (-lst* . args) (if (null? args)
(-val null)
(-pair (car args) (apply -lst* (cdr args)))))
#;(define NE (-mu x (Un N (make-Listof x))))
(define -NE (-mu x (*Un N (-pair x (-pair Sym (-pair x (-val null)))))))
(define (Un/eff . args)
(apply Un (map tc-result-t args)))
(define -Param make-Param)
(define make-pred-ty
(case-lambda
[(in out t)
(->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
[(t) (make-pred-ty (list Univ) B t)]))
(define -Pathlike (*Un -Path -String))
(define -Pathlike* (*Un (-val 'up) (-val 'same) -Path -String))
(define -Pattern (*Un -String -Bytes -Regexp -Byte-Regexp -PRegexp -Byte-PRegexp))
(define -Byte N)
(define (-Tuple l)
(foldr -pair (-val '()) l))
(define Any-Syntax
(-mu x
(-Syntax (*Un
(-lst x)
(-mu y (*Un x (-pair x y)))
(make-Vector x)
(make-Box x)
N
B
-String
Sym))))
(define Ident (-Syntax Sym))
;; DO NOT USE if t contains #f
(define (-opt t) (*Un (-val #f) t))
(define-syntax (make-env stx)
(syntax-case stx ()
[(_ e ...)
#`(list
#,@(map (lambda (e)
(syntax-case e ()
[(nm ty)
(identifier? #'nm)
#`(list #'nm ty)]
[(e ty extra-mods ...)
#'(list (let ([new-ns
(let* ([ns (make-empty-namespace)])
(namespace-attach-module (current-namespace)
'scheme/base
ns)
ns)])
(parameterize ([current-namespace new-ns])
(namespace-require 'extra-mods) ...
e))
ty)]))
(syntax->list #'(e ...))))]))
;; if t is of the form (Pair t* (Pair t* ... (Listof t*)))
;; return t*
;; otherwise, return t
;; generalize : Type -> Type
(define (generalize t)
(let/ec exit
(let loop ([t* t])
(match t*
[(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
[(Pair: t1 t2)
(let ([t-new (loop t2)])
(if (type-equal? (-lst t1) t-new)
t-new
(exit t)))]
[_ (exit t)]))))
)

145
collects/typed-scheme/private/type-effect-printer.ss Normal file
View File

@ -0,0 +1,145 @@
(module type-effect-printer mzscheme
(require "type-rep.ss" "effect-rep.ss" "rep-utils.ss" "tc-utils.ss")
(require (lib "plt-match.ss"))
(require "planet-requires.ss")
;; do we attempt to find instantiations of polymorphic types to print?
;; FIXME - currently broken
(define print-poly-types? #f)
;; do we use simple type aliases in printing
(define print-aliases #t)
;; does t have a type name associated with it currently?
;; has-name : Type -> Maybe[Symbol]
(define (has-name? t)
(define ns ((current-type-names)))
(let/cc return
(unless print-aliases
(return #f))
(for-each
(lambda (pair)
(cond [(eq? t (cdr pair))
(return (car pair))]))
ns)
#f))
;; print out an effect
;; print-effect : Effect Port Boolean -> Void
(define (print-effect c port write?)
(define (fp . args) (apply fprintf port args))
(match c
[(Restrict-Effect: t v) (fp "(restrict ~a ~a)" t (syntax-e v))]
[(Remove-Effect: t v) (fp "(remove ~a ~a)" t (syntax-e v))]
[(Latent-Restrict-Effect: t) (fp "(restrict ~a)" t)]
[(Latent-Remove-Effect: t) (fp "(remove ~a)" t)]
[(Latent-Var-True-Effect:) (fp "(var #t)")]
[(Latent-Var-False-Effect:) (fp "(var #f)")]
[(True-Effect:) (fp "T")]
[(False-Effect:) (fp "F")]
[(Var-True-Effect: v) (fp "(var #t ~a)" (syntax-e v))]
[(Var-False-Effect: v) (fp "(var #f ~a)" (syntax-e v))]))
;; print out a type
;; print-type : Type Port Boolean -> Void
(define (print-type c port write?)
(define (fp . args) (apply fprintf port args))
(define (print-arr a)
(match a
[(top-arr:)
(fp "Procedure")]
[(arr: dom rng rest thn-eff els-eff)
(fp "(")
(for-each (lambda (t) (fp "~a " t)) dom)
(when rest
(fp "~a .. " rest))
(fp "-> ~a" rng)
(unless (and (null? thn-eff) (null? els-eff))
(fp " : ~a ~a" thn-eff els-eff))
(fp ")")]))
(define (tuple? t)
(match t
[(Pair: a (? tuple?)) #t]
[(Value: '()) #t]
[_ #f]))
(define (tuple-elems t)
(match t
[(Pair: a e) (cons a (tuple-elems e))]
[(Value: '()) null]))
;(fp "~a~n" (Type-seq c))
(match c
[(Univ:) (fp "Any")]
[(? has-name?) (fp "~a" (has-name? c))]
;; names are just the printed as the original syntax
[(Name: stx) (fp "[~a]" (syntax-e stx))]
[(App: rator rands stx)
(fp "~a" (cons rator rands))]
;; special cases for lists
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
(fp "(Listof ~a)" elem-ty)]
[(Mu: var (Union: (list (Pair: elem-ty (F: var)) (Value: '()))))
(fp "(Listof ~a)" elem-ty)]
[(Value: v) (cond [(or (symbol? v) (null? v))
(fp "'~a" v)]
[else (fp "~a" v)])]
[(? tuple? t)
(fp "~a" (cons 'List (tuple-elems t)))]
[(Base: n) (fp "~a" n)]
[(Opaque: pred _) (fp "(Opaque ~a)" (syntax-object->datum pred))]
[(Struct: 'Promise par (list fld) proc) (fp "(Promise ~a)" fld)]
[(Struct: nm par flds proc)
(fp "#(struct:~a ~a" nm flds)
(when proc
(fp " ~a" proc))
(fp ")")]
[(Function: arities)
(let ()
(match arities
[(list) (fp "(case-lambda)")]
[(list a) (print-arr a)]
[(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))]
[(arr: _ _ _ _ _) (print-arr c)]
[(Vector: e) (fp "(Vectorof ~a)" e)]
[(Box: e) (fp "(Box ~a)" e)]
[(Union: elems) (fp "~a" (cons 'U elems))]
[(Pair: l r) (fp "(Pair ~a ~a)" l r)]
[(F: nm) (fp "<~a>" nm)]
[(Values: (list v ...)) (fp "~a" (cons 'values v))]
[(Param: in out)
(if (equal? in out)
(fp "(Paramter ~a)" in)
(fp "(Parameter ~a ~a)" in out))]
[(Hashtable: k v) (fp "(HashTable ~a ~a)" k v)]
#;
[(Poly-unsafe: n b) (fp "(unsafe-poly ~a ~a ~a)" (Type-seq c) n b)]
[(Poly-names: names body)
#;(fprintf (current-error-port) "POLY SEQ: ~a~n" (Type-seq body))
(fp "(All ~a ~a)" names body)]
#;
[(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)]
[(Mu: x (Syntax: (Union: (list
(Base: 'Number)
(Base: 'Boolean)
(Base: 'Symbol)
(Base: 'String)
(Mu: var (Union: (list (Value: '()) (Pair: (F: x) (F: var)))))
(Mu: y (Union: (list (F: x) (Pair: (F: x) (F: y)))))
(Vector: (F: x))
(Box: (F: x))))))
(fp "SyntaxObject")]
[(Mu-name: name body) (fp "(mu ~a ~a ~a)" (Type-seq c) name body)]
;; FIXME - this should not be used
#;
[(Scope: sc) (fp "(Scope ~a)" sc)]
#;
[(B: idx) (fp "(B ~a)" idx)]
[(Syntax: t) (fp "(Syntax ~a)" t)]
[(Instance: t) (fp "(Instance ~a)" t)]
[(Class: pf nf ms) (fp "(Class)")]
[else (fp "Unknown Type: ~a" (struct->vector c))]
))
(set-box! print-type* print-type)
(set-box! print-effect* print-effect)
)

78
collects/typed-scheme/private/type-utils.ss Normal file
View File

@ -0,0 +1,78 @@
#lang scheme/base
(require "type-rep.ss"
"effect-rep.ss"
"tc-utils.ss"
"rep-utils.ss"
"free-variance.ss"
mzlib/plt-match
(for-syntax scheme/base))
(provide fv fv/list
substitute
subst-all
subst
ret
instantiate-poly
tc-result:
tc-result-equal?
effects-equal?
tc-result-t)
;; substitute : Type Name Type -> Type
(define (substitute image name target)
(define (sb t) (substitute image name t))
(if (hash-table-get (free-vars* target) name #f)
(type-case sb target
[#:F name* (if (eq? name* name) image target)])
target))
;; substitute many variables
;; substitution = Listof[List[Name,Type]]
;; subst-all : substition Type -> Type
(define (subst-all s t)
(foldr (lambda (e acc) (substitute (cadr e) (car e) acc)) t s))
(define (instantiate-poly t types)
(match t
[(Poly: ns body)
(unless (= (length types) (length ns))
(int-err "instantiate-poly: wrong number of types: expected ~a, got ~a" (length ns) (length types)))
(subst-all (map list ns types) body)]
[_ (int-err "instantiate-many: requires Poly type, got ~a" t)]))
;; this structure represents the result of typechecking an expression
(define-struct tc-result (t thn els) #:inspector #f)
(define-match-expander tc-result:
(lambda (stx)
(syntax-case stx ()
[(form pt) #'(struct tc-result (pt _ _))]
[(form pt pe1 pe2) #'(struct tc-result (pt pe1 pe2))])))
;; convenience function for returning the result of typechecking an expression
(define ret
(case-lambda [(t) (make-tc-result t (list) (list))]
[(t thn els) (make-tc-result t thn els)]))
(define (subst v t e) (substitute t v e))
;; type comparison
;; equality - good
(define tc-result-equal? equal?)
(define (effects-equal? fs1 fs2) (andmap eq? fs1 fs2))
;; fv : Type -> Listof[Name]
(define (fv t) (hash-table-map (free-vars* t) (lambda (k v) k)))
;; fv/list : Listof[Type] -> Listof[Name]
(define (fv/list ts) (hash-table-map (combine-frees (map free-vars* ts)) (lambda (k v) k)))

62
collects/typed-scheme/private/union.ss Normal file
View File

@ -0,0 +1,62 @@
(module union mzscheme
(require "type-rep.ss" "subtype.ss" "tc-utils.ss"
"type-effect-printer.ss" "rep-utils.ss"
"type-comparison.ss")
(require (lib "plt-match.ss") (lib "list.ss") (lib "trace.ss"))
(provide Un #;(rename *Un Un))
(define (make-union* set)
(match set
[(list t) t]
[_ (make-Union set)]))
(define empty-union (make-Union null))
(define (flat t)
(match t
[(Union: es) es]
[_ (list t)]))
#;(define (Values-types t) (match t [(Values: ts) ts]))
(define (remove-subtypes ts)
(let loop ([ts* ts] [result '()])
(cond [(null? ts*) (reverse result)]
[(ormap (lambda (t) (subtype (car ts*) t)) result) (loop (cdr ts*) result)]
[else (loop (cdr ts*) (cons (car ts*) result))])))
(define Un
(case-lambda
[() empty-union]
[args
;; a is a Type (not a union type)
;; b is a List[Type]
(define (union2 a b)
(define b* (make-union* b))
(cond
[(subtype a b*) (list b*)]
[(subtype b* a) (list a)]
[else (cons a b)]))
#;(union-count!)
(let ([types (remove-dups (sort (apply append (map flat args)) type<?))])
(cond
[(null? types) (make-union* null)]
[(null? (cdr types)) (car types)]
[(ormap Values? types)
(if (andmap Values? types)
(make-Values (apply map Un (map Values-types types)))
(int-err "Un: should not take the union of multiple values with some other type: ~a" types))]
[else (make-union* #;(remove-subtypes types) (foldr union2 null types))]))]))
#;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args)
#;(define (*Un . args) (Un-intern args))
;(trace Un)
(define (u-maker args) (apply Un args))
;(trace u-maker)
(set-union-maker! u-maker)
)

90
collects/typed-scheme/typed-reader.ss Normal file
View File

@ -0,0 +1,90 @@
(module typed-reader mzscheme
(require (lib "etc.ss"))
(require-for-template "private/prims.ss")
;; Provides raise-read-error and raise-read-eof-error
(require (lib "readerr.ss" "syntax"))
(define (skip-whitespace port)
;; Skips whitespace characters, sensitive to the current
;; readtable's definition of whitespace
(let ([ch (peek-char port)])
(unless (eof-object? ch)
;; Consult current readtable:
(let-values ([(like-ch/sym proc dispatch-proc)
(readtable-mapping (current-readtable) ch)])
;; If like-ch/sym is whitespace, then ch is whitespace
(when (and (char? like-ch/sym)
(char-whitespace? like-ch/sym))
(read-char port)
(skip-whitespace port))))))
(define (skip-comments read-one port src)
;; Recursive read, but skip comments and detect EOF
(let loop ()
(let ([v (read-one)])
(cond
[(special-comment? v) (loop)]
[(eof-object? v)
(let-values ([(l c p) (port-next-location port)])
(raise-read-eof-error "unexpected EOF in type annotation" src l c p 1))]
[else v]))))
(define (parse port read-one src)
(skip-whitespace port)
(let ([name (read-one)])
(begin0
(begin (skip-whitespace port)
(let ([next (read-one)])
(case (syntax-e next)
;; type annotation
[(:) (skip-whitespace port)
(syntax-property name 'type-label (syntax-object->datum (read-one)))]
[(::) (skip-whitespace port)
(datum->syntax-object name `(ann ,name : ,(read-one)))]
[(@) (let ([elems (let loop ([es '()])
(skip-whitespace port)
(if (equal? #\} (peek-char port))
(reverse es)
(loop (cons (read-one) es))))])
(datum->syntax-object name `(inst ,name : ,@elems)))]
;; arbitrary property annotation
[(PROP) (skip-whitespace port)
(let* ([prop-name (syntax-e (read-one))])
(skip-whitespace port)
(syntax-property name prop-name (read-one)))]
;; type annotation
[else (syntax-property name 'type-label (syntax-object->datum next))])))
(skip-whitespace port)
(let ([c (read-char port)])
#;(printf "char: ~a" c)
(unless (equal? #\} c)
(let-values ([(l c p) (port-next-location port)])
(raise-read-error (format "typed expression ~a not properly terminated" (syntax-object->datum name)) src l c p 1)))))))
(define parse-id-type
(case-lambda
[(ch port src line col pos)
;; `read-syntax' mode
(datum->syntax-object
#f
(parse port
(lambda () (read-syntax src port ))
src)
(let-values ([(l c p) (port-next-location port)])
(list src line col pos (and pos (- p pos)))))]))
(define readtable
(make-readtable #f #\{ 'dispatch-macro parse-id-type))
(define (*read inp)
(parameterize ([current-readtable readtable])
(read inp)))
(define (*read-syntax src port)
(parameterize ([current-readtable readtable])
(read-syntax src port)))
(provide (rename *read read) (rename *read-syntax read-syntax))
)

392
collects/typed-scheme/typed-scheme.scrbl Normal file
View File

@ -0,0 +1,392 @@
#lang scribble/doc
@begin[(require scribble/manual)
(require (for-label typed-scheme/lang/main))]
@begin[
(define (item* header . args) (apply item @bold[header]{: } args))
(define-syntax-rule (tmod forms ...) (schememod typed-scheme forms ...))
]
@title[#:tag "top"]{@bold{Typed Scheme}: Scheme with Static Types}
@(defmodulelang typed-scheme #:use-sources (typed-scheme/lang/main))
Typed Scheme is a Scheme-like language, with a type system that
supports common Scheme programming idioms. Explicit type declarations
are required --- that is, there is no type inference. The language
supports a number of features from previous work on type systems that
make it easier to type Scheme programs, as well as a novel idea dubbed
@italic{occurrence typing} for case discrimination.
Typed Scheme is also designed to integrate with the rest of your PLT
Scheme system. It is possible to convert a single module to Typed
Scheme, while leaving the rest of the program unchanged. The typed
module is protected from the untyped code base via
automatically-synthesized contracts.
Further information on Typed Scheme is available from
@link["http://www.ccs.neu.edu/home/samth/typed-scheme"]{the homepage}.
@section{Starting with Typed Scheme}
If you already know PLT Scheme, or even some other Scheme, it should be
easy to start using Typed Scheme.
@subsection{A First Function}
The following program defines the Fibonacci function in PLT Scheme:
@schememod[scheme
(define (fib n)
(cond [(= 0 n) 1]
[(= 1 n) 1]
[else (+ (fib (- n 1)) (fib (- n 2)))]))
]
This program defines the same program using Typed Scheme.
@schememod[typed-scheme
(: fib (Number -> Number))
(define (fib n)
(cond [(= 0 n) 1]
[(= 1 n) 1]
[else (+ (fib (- n 1)) (fib (- n 2)))]))
]
There are two differences between these programs:
@itemize{
@item*[@elem{The Language}]{@schememodname[scheme] has been replaced by @schememodname[typed-scheme].}
@item*[@elem{The Type Annotation}]{We have added a type annotation
for the @scheme[fib] function, using the @scheme[:] form.} }
In general, these are most of the changes that have to be made to a
PLT Scheme program to transform it into a Typed Scheme program.
@margin-note{Changes to uses of @scheme[require] may also be necessary
- these are described later.}
@subsection[#:tag "complex"]{Adding more complexity}
Other typed binding forms are also available. For example, we could have
rewritten our fibonacci program as follows:
@schememod[typed-scheme
(: fib (Number -> Number))
(define (fib n)
(let ([base? (or (= 0 n) (= 1 n))])
(if base? 1
(+ (fib (- n 1)) (fib (- n 2))))))
]
This program uses the @scheme[let] binding form, but no new type
annotations are required. Typed Scheme infers the type of
@scheme[base?].
We can also define mutually-recursive functions:
@schememod[typed-scheme
(: my-odd? (Number -> Boolean))
(define (my-odd? n)
(if (= 0 n) #f
(my-even? (- n 1))))
(: my-even? (Number -> Boolean))
(define (my-even? n)
(if (= 0 n) #t
(my-odd? (- n 1))))
(display (my-even? 12))
]
As expected, this program prints @schemeresult[#t].
@subsection{Defining New Datatypes}
If our program requires anything more than atomic data, we must define
new datatypes. In Typed Scheme, structures can be defined, similarly
to PLT Scheme structures. The following program defines a date
structure and a function that formats a date as a string, using PLT
Scheme's built-in @scheme[format] function.
@schememod[typed-scheme
(define-typed-struct Date ([day : Number] [month : String] [year : Number]))
(: format-date (Date -> String))
(define (format-date d)
(format "Today is day ~a of ~a in the year ~a"
(Date-day d) (Date-month d) (Date-year d)))
(display (format-date (make-Date 28 "November" 2006)))
]
Here we see the new built-in type @scheme[String] as well as a definition
of the new user-defined type @scheme[my-date]. To define
@scheme[my-date], we provide all the information usually found in a
@scheme[define-struct], but added type annotations to the fields using
the @scheme[define-typed-struct] form.
Then we can use the functions that this declaration creates, just as
we would have with @scheme[define-struct].
@subsection{Recursive Datatypes and Unions}
Many data structures involve multiple variants. In Typed Scheme, we
represent these using @italic{union types}, written @scheme[(U t1 t2 ...)].
@schememod[typed-scheme
(define-type-alias Tree (U leaf node))
(define-typed-struct leaf ([val : Number]))
(define-typed-struct node ([left : Tree] [right : Tree]))
(: tree-height (Tree -> Number))
(define (tree-height t)
(cond [(leaf? t) 1]
[else (max (tree-height (node-left t))
(tree-height (node-right t)))]))
(: tree-sum (Tree -> Number))
(define (tree-sum t)
(cond [(leaf? t) (leaf-val t)]
[else (+ (tree-sum (node-left t))
(tree-sum (node-right t)))]))
]
In this module, we have defined two new datatypes: @scheme[leaf] and
@scheme[node]. We've also defined the type alias @scheme[Tree] to be
@scheme[(U node leaf)], which represents a binary tree of numbers. In
essence, we are saying that the @scheme[tree-height] function accepts
a @scheme[Tree], which is either a @scheme[node] or a @scheme[leaf],
and produces a number.
In order to calculate interesting facts about trees, we have to take
them apart and get at their contents. But since accessors such as
@scheme[node-left] require a @scheme[node] as input, not a
@scheme[Tree], we have to determine which kind of input we
were passed.
For this purpose, we use the predicates that come with each defined
structure. For example, the @scheme[leaf?] predicate distinguishes
@scheme[leaf]s from all other Typed Scheme values. Therefore, in the
first branch of the @scheme[cond] clause in @scheme[tree-sum], we know
that @scheme[t] is a @scheme[leaf], and therefore we can get its value
with the @scheme[leaf-val] function.
In the else clauses of both functions, we know that @scheme[t] is not
a @scheme[leaf], and since the type of @scheme[t] was @scheme[Tree] by
process of elimination we can determine that @scheme[t] must be a
@scheme[node]. Therefore, we can use accessors such as
@scheme[node-left] and @scheme[node-right] with @scheme[t] as input.
@section{Polymorphism}
Virtually every Scheme program uses lists and sexpressions. Fortunately, Typed
Scheme can handle these as well. A simple list processing program can be
written like this:
@schememod[typed-scheme
(: sum-list ((Listof Number) -> Number))
(define (sum-list l)
(cond [(null? l) 0]
[else (+ (car l) (sum-list (cdr l)))]))
]
This looks similar to our earlier programs --- except for the type
of @scheme[l], which looks like a function application. In fact, it's
a use of the @italic{type constructor} @scheme[Listof], which takes
another type as its input, here @scheme[Number]. We can use
@scheme[Listof] to construct the type of any kind of list we might
want.
We can define our own type constructors as well. For example, here is
an analog of the @tt{Maybe} type constructor from Haskell:
@schememod[typed-scheme
(define-typed-struct Nothing ())
(define-typed-struct (a) Just ([v : a]))
(define-type-alias (Maybe a) (U Nothing (Just a)))
(: find (Number (Listof Number) -> (Maybe Number)))
(define (find v l)
(cond [(null? l) (make-Nothing)]
[(= v (car l)) (make-Just v)]
[else (find v (cdr l))]))
]
The first @scheme[define-typed-struct] defines @scheme[Nothing] to be
a structure with no contents.
The second definition
@schemeblock[
(define-typed-struct (a) Just ([v : a]))
]
creates a parameterized type, @scheme[Just], which is a structure with
one element, whose type is that of the type argument to
@scheme[Just]. Here the type parameters (only one, @scheme[a], in
this case) are written before the type name, and can be referred to in
the types of the fields.
The type alias definiton
@schemeblock[
(define-type-alias (Maybe a) (U Nothing (Just a)))
]
creates a parameterized alias --- @scheme[Maybe] is a potential
container for whatever type is supplied.
The @scheme[find] function takes a number @scheme[v] and list, and
produces @scheme[(make-Just v)] when the number is found in the list,
and @scheme[(make-Nothing)] otherwise. Therefore, it produces a
@scheme[(Maybe Number)], just as the annotation specified.
@section[#:tag "type-ref"]{Type Reference}
@subsubsub*section{Base Types}
These types represent primitive Scheme data.
@defidform[Number]{Any number}
@defidform[Boolean]{Either @scheme[#t] or @scheme[#f]}
@defidform[String]{A string}
@defidform[Keyword]{A PLT Scheme literal keyword}
@defidform[Symbol]{A symbol}
@defidform[Any]{Any value}
@subsubsub*section{Type Constructors}
The following constructors are parameteric in their type arguments.
@defform[(Listof t)]{Homogenous lists of @scheme[t]}
@defform[(Vectorof t)]{Homogenous vectors of @scheme[t]}
@defform[(Option t)]{Either @scheme[t] of @scheme[#f]}
@;{
@schemeblock[
(define: f : (Number -> Number) (lambda: ([x : Number]) 3))
]
}
@begin[
(require (for-syntax scheme/base))
(define-syntax (definfixform stx)
(syntax-case stx ()
[(_ dummy . rest) #'(begin (specform . rest))]))
#;
(define-syntax (definfixform stx)
(syntax-case stx ()
[(_ id spec desc ...)
#'(*defforms (quote-syntax id)
'()
'(spec)
(list (lambda (x) (schemeblock0 spec)))
'()
'()
(lambda () (list desc ...)))]))
]
@defform[(Pair s t)]{is the pair containing @scheme[s] as the @scheme[car]
and @scheme[t] as the @scheme[cdr]}
@defform[(-> dom ... rng)]{is the type of functions from the (possibly-empty)
sequence @scheme[dom ...] to the @scheme[rng] type.}
@defform[(U t ...)]{is the union of the types @scheme[t ...]}
@defform[(case-lambda fun-ty ...)]{is a function that behaves like all of
the @scheme[fun-ty]s. The @scheme[fun-ty]s must all be function
types constructed with @scheme[->].}
@defform/none[(t t1 t2 ...)]{is the instantiation of the parametric type
@scheme[t] at types @scheme[t1 t2 ...]}
@defform[(All (v ...) t)]{is a parameterization of type @scheme[t], with
type variables @scheme[v ...]}
@defform[(values t ...)]{is the type of a sequence of multiple values, with
types @scheme[t ...]. This can only appear as the return type of a
function.}
@defform/none[v]{where @scheme[v] is a number, boolean or string, is the singleton type containing
only that value}
@defform/none[i]{where @scheme[i] is an identifier can be a reference to a type
name or a type variable}
@defform[(Rec n t)]{is a recursive type where @scheme[n] is bound to the
recursive type in the body @scheme[t]}
Other types cannot be written by the programmer, but are used
internally and may appear in error messages.
@defform/none[(struct:n (t ...))]{is the type of structures named
@scheme[n] with field types @scheme[t]. There may be multiple such
types with the same printed representation.}
@defform/none[<n>]{is the printed representation of a reference to the
type variable @scheme[n]}
@section[#:tag "special-forms"]{Special Form Reference}
Typed Scheme provides a variety of special forms above and beyond
those in PLT Scheme. They are used for annotating variables with types,
creating new types, and annotating expressions.
@subsection{Binding Forms}
@scheme[_loop], @scheme[_f], @scheme[_a], and @scheme[_v] are names, @scheme[_t] is a type.
@scheme[_e] is an expression and @scheme[_body] is a block.
@defform*[[(define: (f [v : t] ...) : t body)
(define: v : t e)]]{}
@defform[
(pdefine: (a ...) (f [v : t] ...) : t body)]{}
@defform*[[
(let: ([v : t e] ...) body)
(let: loop : t0 ([v : t e] ...) body)]]{where @scheme[_t0] is the type of the
result of @scheme[_loop] (and thus the result of the entire expression).}
@defform[
(letrec: ([v : t e] ...) body)]{}
@defform[
(let*: ([v : t e] ...) body)]{}
@defform*[[
(lambda: ([v : t] ...) body)
(lambda: ([v : t] ... . [v : t]) body)]]{}
@defform*[[
(plambda: (a ...) ([v : t] ...) body)
(plambda: (a ...) ([v : t] ... . [v : t]) body)]]{}
@defform[
(case-lambda: [formals body] ...)]{where @scheme[_formals] is like
the second element of a @scheme[lambda:]}
@defform[
(pcase-lambda: (a ...) [formals body] ...)]{where @scheme[_formals] is like
the third element of a @scheme[plambda:]}
@subsection{Structure Definitions}
@defform*[[
(define-typed-struct name ([f : t] ...))
(define-typed-struct (name parent) ([f : t] ...))
(define-typed-struct (v ...) name ([f : t] ...))
(define-typed-struct (v ...) (name parent) ([f : t] ...))]]
@subsection{Type Aliases}
@defform*[[(define-type-alias name t)
(define-type-alias (name v ...) t)]]{}
@subsection{Type Annotation}
@defform[
(: v t)
]
@litchar{#{v : t}} This is legal only for binding occurences of @scheme[_v].
@litchar{#{e :: t}} This is legal only in expression contexts.
@subsection{Require}
Here, @scheme[_m] is a module spec, @scheme[_pred] is an identifier
naming a predicate, and @scheme[_r] is an optionally-renamed identifier.
@defform*[[
(require/typed r t m)
(require/typed m [r t] ...)
]]{}
@defform[(require/opaque-type t pred m)]{}
@defform[(require-typed-struct name ([f : t] ...) m)]{}

150
collects/typed-scheme/typed-scheme.ss Normal file
View File

@ -0,0 +1,150 @@
#lang scheme/base
(require "private/prims.ss"
"private/init-envs.ss"
"private/extra-procs.ss"
"private/internal-forms.ss"
"private/base-env.ss"
(for-syntax
scheme/base
"private/type-utils.ss"
"private/typechecker.ss"
"private/type-rep.ss"
"private/provide-handling.ss"
"private/type-environments.ss" "private/tc-utils.ss"
"private/type-env.ss" "private/type-name-env.ss"
"private/type-alias-env.ss"
"private/utils.ss"
"private/internal-forms.ss"
"private/init-envs.ss"
"private/type-effect-convenience.ss"
"private/effect-rep.ss"
"private/rep-utils.ss"
"private/type-contract.ss"
"private/nest.ss"
syntax/kerncase
mzlib/list
mzlib/plt-match))
(provide
;; provides syntax such as define: and define-typed-struct
(all-from-out "private/prims.ss")
;; provides some pointless procedures - should be removed
(all-from-out "private/extra-procs.ss"))
(provide-tnames)
(provide-extra-tnames)
(provide (rename-out [module-begin #%module-begin]
[with-handlers: with-handlers]
[top-interaction #%top-interaction]
[#%plain-lambda lambda]
[#%plain-app #%app]
[require require]))
(define-for-syntax catch-errors? #f)
(define-syntax (module-begin stx)
(define module-name (syntax-property stx 'enclosing-module-name))
;(printf "BEGIN: ~a~n" (syntax->datum stx))
(with-logging-to-file
(log-file-name (syntax-src stx) module-name)
(syntax-case stx ()
[(mb forms ...)
(nest
([begin (set-box! typed-context? #t)
(start-timing module-name)]
[with-handlers
([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e))))
(lambda (e) (tc-error "Internal error: ~a" e))])]
[parameterize (;; this parameter is for parsing types
[current-tvars initial-tvar-env]
;; this parameter is just for printing types
;; this is a parameter to avoid dependency issues
[current-type-names
(lambda ()
(append
(type-name-env-map (lambda (id ty)
(cons (syntax-e id) ty)))
(type-alias-env-map (lambda (id ty)
(cons (syntax-e id) ty)))))]
;; reinitialize seen type variables
[type-name-references null])]
[begin (do-time "Initialized Envs")]
;; local-expand the module
;; pmb = #%plain-module-begin
[with-syntax ([new-mod
(local-expand #`(#%plain-module-begin
forms ...)
'module-begin
null
#;stop-list)])]
[with-syntax ([(pmb body2 ...) #'new-mod])]
[begin (do-time "Local Expand Done")]
[with-syntax ([after-code (parameterize ([orig-module-stx stx]
[expanded-module-stx #'new-mod])
(type-check #'(body2 ...)))]
[check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))]
[(transformed-body ...) (remove-provides #'(body2 ...))])]
[with-syntax ([(transformed-body ...) (change-contract-fixups #'(transformed-body ...))])])
(do-time "Typechecked")
(printf "checked ~a~n" module-name)
#;(printf "created ~a types~n" (count!))
#;(printf "tried to create ~a types~n" (all-count!))
#;(printf "created ~a union types~n" (union-count!))
;; reconstruct the module with the extra code
#'(#%module-begin transformed-body ... after-code check-syntax-help))])))
(define-syntax (top-interaction stx)
(syntax-case stx ()
[(_ . (module . rest))
(eq? 'module (syntax-e #'module))
#'(module . rest)]
[(_ . form)
(nest
([begin (set-box! typed-context? #t)]
[parameterize (;; this paramter is for parsing types
[current-tvars initial-tvar-env]
;; this parameter is just for printing types
;; this is a parameter to avoid dependency issues
[current-type-names
(lambda ()
(append
(type-name-env-map (lambda (id ty)
(cons (syntax-e id) ty)))
(type-alias-env-map (lambda (id ty)
(cons (syntax-e id) ty)))))])]
;(do-time "Initialized Envs")
;; local-expand the module
[let ([body2 (local-expand #'(#%top-interaction . form) 'top-level null)])]
[parameterize ([orig-module-stx #'form]
[expanded-module-stx body2])]
;; typecheck the body, and produce syntax-time code that registers types
[let ([type (tc-toplevel-form body2)])])
(kernel-syntax-case body2 #f
[(head . _)
(or (free-identifier=? #'head #'define-values)
(free-identifier=? #'head #'define-syntaxes)
(free-identifier=? #'head #'require)
(free-identifier=? #'head #'provide)
(free-identifier=? #'head #'begin)
(type-equal? -Void (tc-result-t type)))
body2]
;; construct code to print the type
[_
(nest
([with-syntax ([b body2]
[ty-str (match type
[(tc-result: t)
(format "- : ~a\n" t)]
[x (int-err "bad type result: ~a" x)])])])
#`(let ([v b] [type 'ty-str])
(begin0
v
(printf type))))]))]))