From 7f2824d11c82ff59700ee2b3d5b1d61baa46ca47 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Mon, 3 Mar 2008 22:57:55 +0000 Subject: [PATCH] Add Typed Scheme as a collection. svn: r8864 original commit: 0d54ed5e7427f5e75e6274cc3c9625e676fc34bc --- collects/typed-scheme/info.ss | 4 + collects/typed-scheme/lang/main.ss | 9 + collects/typed-scheme/lang/minimal.ss | 29 + collects/typed-scheme/lang/reader.ss | 15 + collects/typed-scheme/private/base-env.ss | 570 ++++++++++++++++++ collects/typed-scheme/private/extra-procs.ss | 9 + collects/typed-scheme/private/mutated-vars.ss | 52 ++ collects/typed-scheme/private/parse-type.ss | 210 +++++++ collects/typed-scheme/private/prims.ss | 335 ++++++++++ .../typed-scheme/private/remove-intersect.ss | 96 +++ .../typed-scheme/private/require-contract.ss | 40 ++ collects/typed-scheme/private/resolve-type.ss | 79 +++ collects/typed-scheme/private/subtype.ss | 272 +++++++++ .../typed-scheme/private/type-annotation.ss | 92 +++ .../private/type-effect-convenience.ss | 231 +++++++ .../private/type-effect-printer.ss | 145 +++++ collects/typed-scheme/private/type-utils.ss | 78 +++ collects/typed-scheme/private/union.ss | 62 ++ collects/typed-scheme/typed-reader.ss | 90 +++ collects/typed-scheme/typed-scheme.scrbl | 392 ++++++++++++ collects/typed-scheme/typed-scheme.ss | 150 +++++ 21 files changed, 2960 insertions(+) create mode 100644 collects/typed-scheme/info.ss create mode 100644 collects/typed-scheme/lang/main.ss create mode 100644 collects/typed-scheme/lang/minimal.ss create mode 100644 collects/typed-scheme/lang/reader.ss create mode 100644 collects/typed-scheme/private/base-env.ss create mode 100644 collects/typed-scheme/private/extra-procs.ss create mode 100644 collects/typed-scheme/private/mutated-vars.ss create mode 100644 collects/typed-scheme/private/parse-type.ss create mode 100644 collects/typed-scheme/private/prims.ss create mode 100644 collects/typed-scheme/private/remove-intersect.ss create mode 100644 collects/typed-scheme/private/require-contract.ss create mode 100644 collects/typed-scheme/private/resolve-type.ss create mode 100644 collects/typed-scheme/private/subtype.ss create mode 100644 collects/typed-scheme/private/type-annotation.ss create mode 100644 collects/typed-scheme/private/type-effect-convenience.ss create mode 100644 collects/typed-scheme/private/type-effect-printer.ss create mode 100644 collects/typed-scheme/private/type-utils.ss create mode 100644 collects/typed-scheme/private/union.ss create mode 100644 collects/typed-scheme/typed-reader.ss create mode 100644 collects/typed-scheme/typed-scheme.scrbl create mode 100644 collects/typed-scheme/typed-scheme.ss diff --git a/collects/typed-scheme/info.ss b/collects/typed-scheme/info.ss new file mode 100644 index 00000000..e59bcb18 --- /dev/null +++ b/collects/typed-scheme/info.ss @@ -0,0 +1,4 @@ +#lang setup/infotab + +(define name "Typed Scheme") +(define scribblings '(("typed-scheme.scrbl"))) diff --git a/collects/typed-scheme/lang/main.ss b/collects/typed-scheme/lang/main.ss new file mode 100644 index 00000000..a31d5925 --- /dev/null +++ b/collects/typed-scheme/lang/main.ss @@ -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)) diff --git a/collects/typed-scheme/lang/minimal.ss b/collects/typed-scheme/lang/minimal.ss new file mode 100644 index 00000000..c732931f --- /dev/null +++ b/collects/typed-scheme/lang/minimal.ss @@ -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) ...))))))])) + \ No newline at end of file diff --git a/collects/typed-scheme/lang/reader.ss b/collects/typed-scheme/lang/reader.ss new file mode 100644 index 00000000..8794ba59 --- /dev/null +++ b/collects/typed-scheme/lang/reader.ss @@ -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]))) + diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss new file mode 100644 index 00000000..514259e8 --- /dev/null +++ b/collects/typed-scheme/private/base-env.ss @@ -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) + diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss new file mode 100644 index 00000000..cd8af3b2 --- /dev/null +++ b/collects/typed-scheme/private/extra-procs.ss @@ -0,0 +1,9 @@ +(module extra-procs mzscheme + (provide assert) + + (define (assert v) + (unless v + (error "Assertion failed - value was #f")) + v) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/mutated-vars.ss b/collects/typed-scheme/private/mutated-vars.ss new file mode 100644 index 00000000..b55ce41c --- /dev/null +++ b/collects/typed-scheme/private/mutated-vars.ss @@ -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?) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss new file mode 100644 index 00000000..f4e16dd9 --- /dev/null +++ b/collects/typed-scheme/private/parse-type.ss @@ -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))]))) + diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss new file mode 100644 index 00000000..29bb988a --- /dev/null +++ b/collects/typed-scheme/private/prims.ss @@ -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 ...)))))]))])) + + + diff --git a/collects/typed-scheme/private/remove-intersect.ss b/collects/typed-scheme/private/remove-intersect.ss new file mode 100644 index 00000000..6765e215 --- /dev/null +++ b/collects/typed-scheme/private/remove-intersect.ss @@ -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) + + diff --git a/collects/typed-scheme/private/require-contract.ss b/collects/typed-scheme/private/require-contract.ss new file mode 100644 index 00000000..c6157919 --- /dev/null +++ b/collects/typed-scheme/private/require-contract.ss @@ -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) +|# diff --git a/collects/typed-scheme/private/resolve-type.ss b/collects/typed-scheme/private/resolve-type.ss new file mode 100644 index 00000000..b07bf88d --- /dev/null +++ b/collects/typed-scheme/private/resolve-type.ss @@ -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) + +|# \ No newline at end of file diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss new file mode 100644 index 00000000..dcda390b --- /dev/null +++ b/collects/typed-scheme/private/subtype.ss @@ -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)) + + diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss new file mode 100644 index 00000000..3b61281a --- /dev/null +++ b/collects/typed-scheme/private/type-annotation.ss @@ -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))))) diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss new file mode 100644 index 00000000..d12f0cbd --- /dev/null +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -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)])))) + + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss new file mode 100644 index 00000000..94240489 --- /dev/null +++ b/collects/typed-scheme/private/type-effect-printer.ss @@ -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) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss new file mode 100644 index 00000000..edfc6dc8 --- /dev/null +++ b/collects/typed-scheme/private/type-utils.ss @@ -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))) diff --git a/collects/typed-scheme/private/union.ss b/collects/typed-scheme/private/union.ss new file mode 100644 index 00000000..a58d59fb --- /dev/null +++ b/collects/typed-scheme/private/union.ss @@ -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)) typedatum (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)) + ) diff --git a/collects/typed-scheme/typed-scheme.scrbl b/collects/typed-scheme/typed-scheme.scrbl new file mode 100644 index 00000000..c534db2b --- /dev/null +++ b/collects/typed-scheme/typed-scheme.scrbl @@ -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[]{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)]{} diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss new file mode 100644 index 00000000..4a856362 --- /dev/null +++ b/collects/typed-scheme/typed-scheme.ss @@ -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))))]))])) + + +