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

commit work to new branch, doesn't work yet

Browse Source 
svn: r13427

original commit: 3ab3c8d3685d30c827c600d93a0930eff7e1902d
This commit is contained in:
Sam Tobin-Hochstadt 2009-02-04 20:19:41 +00:00
parent 5570ebc151
commit cfab8a698f
20 changed files with 551 additions and 159 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/typed-scheme/infer/infer-unit.ss
View File

@ -100,9 +100,9 @@
(define (cgen/eff V X t s)
(match* (t s)
[(e e) (empty-cset X)]
[((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: s))
[((Latent-Restrict-Effect: t k) (Latent-Restrict-Effect: s k))
(cset-meet (cgen V X t s) (cgen V X s t))]
[((Latent-Remove-Effect: t) (Latent-Remove-Effect: s))
[((Latent-Remove-Effect: t k) (Latent-Remove-Effect: s k))
(cset-meet (cgen V X t s) (cgen V X s t))]
[(_ _) (fail! t s)]))

37
collects/typed-scheme/infer/signatures.ss
View File

@ -1,29 +1,42 @@
#lang scheme/base
(require scheme/unit)
(require scheme/unit scheme/contract "constraint-structs.ss" "../utils/utils.ss")
(require (rep type-rep) (utils unit-utils))
(provide (all-defined-out))
(define-signature dmap^
(dmap-meet))
([cnt dmap-meet (dmap? dmap? . -> . dmap?)]))
(define-signature promote-demote^
(var-promote var-demote))
([cnt var-promote (Type? (listof symbol?) . -> . Type?)]
[cnt var-demote (Type? (listof symbol?) . -> . Type?)]))
(define-signature constraints^
(exn:infer?
fail-sym
([cnt exn:infer? (any/c . -> . boolean?)]
[cnt fail-sym symbol?]
;; inference failure - masked before it gets to the user program
(define-syntaxes (fail!)
(syntax-rules ()
[(_ s t) (raise fail-sym)]))
cset-meet cset-meet*
[cnt cset-meet (cset? cset? . -> . cset?)]
[cnt cset-meet* ((listof cset?) . -> . cset?)]
no-constraint
empty-cset
insert
cset-combine
c-meet))
[cnt empty-cset ((listof symbol?) . -> . cset?)]
[cnt insert (cset? symbol? Type? Type? . -> . cset?)]
[cnt cset-combine ((listof cset?) . -> . cset?)]
[cnt c-meet ((c? c?) (symbol?) . ->* . c?)]))
(define-signature restrict^
(restrict))
([cnt restrict (Type? Type? . -> . Type?)]))
(define-signature infer^
(infer infer/vararg infer/dots))
([cnt infer (((listof symbol?) (listof Type?) (listof Type?) Type? (listof symbol?)) ((or/c #f Type?)) . ->* . any)]
[cnt infer/vararg (((listof symbol?)
(listof Type?)
(listof Type?)
Type? Type?
(listof symbol?))
((or/c #f Type?)) . ->* . any)]
[cnt infer/dots (((listof symbol?)
symbol?
(listof Type?) (listof Type?) Type? Type? (listof symbol?))
(#:expected (or/c #f Type?)) . ->* . any)]))

7
collects/typed-scheme/private/base-env.ss
View File

@ -46,7 +46,8 @@
[null (-val null)]
[number? (make-pred-ty N)]
[char? (make-pred-ty -Char)]
[integer? (make-pred-ty -Integer)]
[integer? (Univ . -> . B : (list (make-Latent-Restrict-Effect N)) (list (make-Latent-Remove-Effect -Integer)))]
[exact-integer? (make-pred-ty -Integer)]
[boolean? (make-pred-ty B)]
[add1 (cl->* (-> -Integer -Integer)
(-> N N))]
@ -107,8 +108,8 @@
[filter (-poly (a b) (cl->*
((a . -> . B
:
(list (make-Latent-Restrict-Effect b))
(list (make-Latent-Remove-Effect b)))
(list (make-Latent-Restrict-Effect b 0))
(list (make-Latent-Remove-Effect b 0)))
(-lst a)
. -> .
(-lst b))

7
collects/typed-scheme/private/base-types-extra.ss
View File

@ -11,9 +11,12 @@
;; special types names that are not bound to particular types
(define-other-types
-> U mu Un All Opaque Vectorof
Parameter Tuple Class Values)
-> U mu All Opaque
Parameter Tuple Class Values Instance
pred)
(provide (rename-out [All ∀]
[U Un]
[Tuple List]
[mu Rec]))

13
collects/typed-scheme/private/base-types.ss
View File

@ -12,20 +12,21 @@
[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]
#;[List (-lst Univ)]
[EOF (-val eof)]
[Syntax Any-Syntax]
[Identifier Ident]
[Procedure top-func]
[Keyword -Keyword]
[Listof -Listof]
[Vectorof (-poly (a) (make-Vector a))]
[Option (-poly (a) (-opt a))]
[HashTable (-poly (a b) (-HT a b))]
[Promise (-poly (a) (-Promise a))]
[Pair (-poly (a b) (-pair a b))]
[Boxof (-poly (a) (make-Box a))]
[Syntax Any-Syntax]
[Identifier Ident]
[Procedure top-func]

242
collects/typed-scheme/private/parse-type.ss
View File

@ -1,17 +1,21 @@
#lang scheme/base
(provide parse-type parse-type/id)
(provide parse-type parse-type/id parse-type*)
(require (except-in "../utils/utils.ss" extend))
(require (except-in "../utils/utils.ss" extend id))
(require (except-in (rep type-rep) make-arr)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
(utils tc-utils)
"union.ss"
syntax/stx
stxclass stxclass/util
(env type-environments type-name-env type-alias-env)
"type-utils.ss"
scheme/match)
(prefix-in t: "base-types-extra.ss")
scheme/match
"stxclass-util.ss"
(for-template scheme/base "base-types-extra.ss"))
(define enable-mu-parsing (make-parameter #t))
@ -23,8 +27,238 @@
(define (stx-cadr stx) (stx-car (stx-cdr stx)))
(define (parse-type stx)
(define-syntax-class star
(pattern star:id
#:when (eq? '* #'star.datum)))
(define-syntax-class ddd
(pattern ddd:id
#:when (eq? '... #'ddd.datum)))
(define-syntax-class tvar
#:description "type variable"
(pattern v:id
#:with val (lookup (current-tvars) #'v.datum (lambda (_) #f))
#:with name #'v.datum
#:with datum #'v.datum
#:when #'val))
(define-syntax-class dotted-tvar
#:description "type variable bound with ..."
(pattern v:tvar
#:when (Dotted? #'v.val)
#:with t (Dotted-t #'v.val)
#:with val #'v.val
#:with name #'v.datum
#:with datum #'v.datum))
(define-syntax-class dotted-both-tvar
#:transparent
(pattern v:dotted-tvar
#:when (DottedBoth? #'v.val)
#:with t (Dotted-t #'v.val)
#:with val #'v.val
#:with name #'v.datum
#:with datum #'v.datum))
(define-syntax-class (type/tvars syms var-tys)
(pattern ty
#:with t (parameterize ([current-tvars (extend-env syms
var-tys
(current-tvars))])
(parse-type* #'ty))))
(define-syntax-class (type/tvar sym var-ty)
(pattern ty
#:declare ty (type/tvars (list sym) (list var-ty))
#:with t #'ty.t))
(define-syntax-class fun-ty
#:literals (t:-> :)
#:description "function type"
;; FIXME - shouldn't have to use syntax->datum
(pattern (dom*:type t:-> rng:type : pred:type)
#:when (add-type-name-reference #'t:->)
#:with t (make-pred-ty (list #'dom*.t) #'rng.t #'pred.t)
#:with (dom ...) (list #'dom*))
(pattern (dom:type ... rest:type _:star t:-> rng:type)
#:when (add-type-name-reference #'t:->)
#:with t (->* (syntax->datum #'(dom.t ...)) #'rest.t #'rng.t))
(pattern (dom:type ... rest _:ddd bound:dotted-tvar t:-> rng:type)
#:with rest.t (parse/get #'rest t (type/tvar #'bound.name (make-DottedBoth (make-F #'bound.name))))
#:when (add-type-name-reference #'t:->)
#:with t
(let ([var #'bound.val])
(make-Function
(list
(make-arr-dots (syntax->datum #'(dom.t ...))
#'rng.t
#'rest.t
#'bound.name)))))
(pattern (dom:type ... t:-> rng:type)
#:when (add-type-name-reference #'t:->)
#:with t (->* (syntax->datum #'(dom.t ...)) #'rng.t)))
(define-syntax-class fun-ty/one
(pattern f:fun-ty
#:with arr (match #'f.t [(Function: (list a)) a])))
(define-syntax-class values-ty
#:literals (values)
(pattern (values ts:type ... rest _:ddd bound:dotted-tvar)
#:with rest.t (parse/get #'rest t (type/tvar #'bound.name (make-DottedBoth (make-F #'bound.name))))
#:with t
(make-ValuesDots (syntax->datum #'(ts.t ...))
#'rest.t
#'bound.name))
(pattern (values ts:type ...)
#:with t (-values (syntax->datum #'(ts.t ...)))))
(define-syntax-class type-name
(pattern i:id
#:when (lookup-type-name #'i (lambda () #f))
#:with t #'(make-Name #'i)
#:when (add-type-name-reference #'i)))
(define-syntax-class type-alias
(pattern i:id
#:with t (lookup-type-alias #'i parse-type* (lambda () #f))
#:when #'t
#:when (add-type-name-reference #'i)))
(define-syntax-class all-type
#:literals (t:All)
(pattern (t:All (v:id ... v-last:id _:ddd) b)
#:with b.t (parse/get #'b t (type/tvars (cons #'v-last.datum (syntax->datum #'(v ...)))
(cons (make-Dotted (make-F #'v-last.datum))
(map make-F (syntax->datum #'(v ...))))))
#:when (add-type-name-reference #'All)
#:with t (make-PolyDots (syntax->datum #'(v ... v-last)) #'b.t))
(pattern (t:All (v:id ...) b)
#:with b.t (parse/get #'b t (type/tvars (syntax->datum #'(v ...)) (map make-F (syntax->datum #'(v ...)))))
#:when (add-type-name-reference #'All)
#:with t (make-Poly (syntax->datum #'(v ...)) #'b.t)))
(define-syntax-class type-app
(pattern (i arg:type args:type ...)
#:when (identifier? #'i)
#:declare i type
#:with t
(let loop
([rator #'i.t] [args (syntax->datum #'(arg.t args.t ...))])
(match rator
[(Name: _)
;; FIXME - need orig stx
(make-App rator args #'here)]
[(Poly: ns _)
(if (not (= (length args) (length ns)))
(begin
(tc-error/delayed "Wrong number of arguments to type ~a, expected ~a but got ~a" rator (length ns) (length args))
(instantiate-poly rator (map (lambda _ Err) ns)))
(instantiate-poly rator args))]
[(Mu: _ _) (loop (unfold rator) args)]
[(Error:) Err]
[_ (tc-error/delayed "Type ~a cannot be applied, arguments were: ~a" rator args)
Err]))))
(define-syntax-class not-kw-id
(pattern i:id
#:when (not (for/or ([e (syntax->list
#'(quote t:pred t:Tuple case-lambda t:U t:Rec t:Opaque t:Parameter t:Class t:Instance
t:-> t:All))])
(free-identifier=? e #'i)))
#:when (not (memq #'i.datum '(* ...)))
#:with datum #'i.datum))
(define-syntax-class type
#:literals (quote t:pred t:Tuple case-lambda t:U t:Rec t:Opaque t:Parameter t:Class t:Instance)
(pattern ty
#:declare ty (3d Type?)
#:with t #'ty.datum)
(pattern i:dotted-both-tvar
#:with t #'i.t)
#;
(pattern i:dotted-tvar
#:when (tc-error/stx #'i "Type variable ~a must be used with ..." #'i.datum)
#:with t Err)
(pattern i:tvar
#:when (not (Dotted? #'i.val))
#:with t #'i.val)
(pattern i:type-alias
#:with t #'i.t)
(pattern i:type-name
#:with t #'i.t)
#;
(pattern i:not-kw-id
#:with t Err
#:when (tc-error/stx #'i "Unbound type name ~a" #'i.datum)
)
(pattern ty:all-type
#:with t #'ty.t)
(pattern (t:Rec x:id b)
#:when (enable-mu-parsing)
#:with b.t (parse/get #'b t (type/tvar #'x.datum (make-F #'x.datum)))
#:when (add-type-name-reference #'t:Rec)
#:with t (if (memq #'x.datum (fv #'b.t))
(make-Mu #'x.datum #'b.t)
#'b.t))
(pattern (t:pred ty:type)
#:when (add-type-name-reference #'t:pred)
#:with t (make-pred-ty #'ty.t))
(pattern (t:Parameter ty:type)
#:when (add-type-name-reference #'t:Paramter)
#:with t (-Param #'ty.t #'ty.t))
(pattern (t:Parameter t1:type t2:type)
#:when (add-type-name-reference #'t:Paramter)
#:with t (-Param #'t1.t #'t2.t))
(pattern (t:Opaque p?:id)
#:when (add-type-name-reference #'t:Opaque)
#:with t (make-Opaque #'p? (syntax-local-certifier)))
(pattern (t:U ty:type ...)
#:with t (apply Un (syntax->datum #'(ty.t ...))))
(pattern (t:Tuple ty:type ...)
#:with t (-Tuple (syntax->datum #'(ty.t ...))))
(pattern fty:fun-ty
#:with t #'fty.t)
(pattern vt:values-ty
#:with t #'vt.t)
(pattern (fst:type . rst:type)
#:with t (-pair #'fst.t #'rst.t))
(pattern (quote v:atom)
#:with t (-val #'v.datum))
(pattern (case-lambda f:fun-ty/one ...)
#:with t (make-Function (syntax->datum #'(f.arr ...))))
(pattern (t:Class (pos-args:type ...) ([fname:id fty:type ((rest:boolean) #:opt) ...*] ...) ([mname:id mty:type] ...))
#:with t
(make-Class
(syntax->datum #'(pos-args.t ...))
(syntax->datum #'([fname.datum fty.t rest.datum] ...))
(syntax->datum #'([mname.datum mty.t] ...))))
(pattern (t:Instance ty:type)
#:with t
(if (not (or (Mu? #'ty.t) (Class? #'ty.t) (Union? #'ty.t) (Error? #'ty.t)))
(begin (tc-error/delayed "Argument to Instance must be a class type, got ~a" #'ty.t)
(make-Instance Err))
(make-Instance #'ty.t)))
(pattern tapp:type-app
#:with t #'tapp.t)
(pattern v:atom
#:when (not (symbol? #'v.datum))
#:with t (-val #'v.datum)))
(define (parse-type* stx)
(parameterize ([current-orig-stx stx])
(parse/get stx t type)))
(define (parse-type stx)
(parameterize ([current-orig-stx stx])
(syntax-case* stx ()
symbolic-identifier=?
[t

2
collects/typed-scheme/private/require-contract.ss
View File

@ -25,7 +25,7 @@
[(require/contract nm cnt lib)
(identifier? #'nm)
#`(begin (require (only-in lib [nm tmp]))
(define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))]
(define-ignored nm (contract cnt tmp '(interface for #,(syntax->datum #'nm)) 'never-happen (quote-syntax nm))))]
[(require/contract (orig-nm nm) cnt lib)
#`(begin (require (only-in lib [orig-nm tmp]))
(define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))]))

33
collects/typed-scheme/private/stxclass-util.ss Normal file
View File

@ -0,0 +1,33 @@
#lang scheme/base
(require stxclass (for-syntax stxclass scheme/base stxclass/util))
(provide (all-defined-out))
(define-syntax (parse/get stx)
(syntax-parse stx
[(_ arg:expr attr:id pat)
(let* ([i (generate-temporary)]
[get-i (datum->syntax
i
(string->symbol
(string-append (symbol->string (syntax-e i))
"."
(symbol->string #'attr.datum))))])
(quasisyntax/loc stx
(syntax-parse arg
[#,i #:declare #,i pat #'#,get-i])))]))
(define (atom? v)
(or (number? v) (string? v) (boolean? v) (symbol? v) (keyword? v) (char? v) (bytes? v) (regexp? v)))
(define-syntax-class (3d pred)
(pattern s
#:with datum (syntax-e #'s)
#:when (pred #'datum)))
(define-pred-stxclass atom atom?)
(define-pred-stxclass byte-pregexp byte-pregexp?)
(define-pred-stxclass byte-regexp byte-regexp?)
(define-pred-stxclass regexp regexp?)
(define-pred-stxclass bytes bytes?)

10
collects/typed-scheme/private/subtype.ss
View File

@ -81,15 +81,15 @@
(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*))
(match* (e1 e2)
[(e e) #t]
[((Latent-Restrict-Effect: t k) (Latent-Restrict-Effect: t* k))
(and (subtype t t*)
(subtype t* t))]
[(list (Latent-Remove-Effect: t) (Latent-Remove-Effect: t*))
[((Latent-Remove-Effect: t k) (Latent-Remove-Effect: t* k))
(and (subtype t t*)
(subtype t* t))]
[else #f]))
[(_ _) #f]))
;(trace sub-eff)

10
collects/typed-scheme/private/type-effect-convenience.ss
View File

@ -38,10 +38,10 @@
(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)]
[(Latent-Var-True-Effect: k) (-vet v)]
[(Latent-Var-False-Effect: k) (-vef v)]
[(Latent-Restrict-Effect: t k) (make-Restrict-Effect t v)]
[(Latent-Remove-Effect: t k) (make-Remove-Effect t v)]
[(True-Effect:) eff]
[(False-Effect:) eff]
[_ (int-err "can't add var ~a to effect ~a" v eff)]))
@ -208,7 +208,7 @@
(define make-pred-ty
(case-lambda
[(in out t)
(->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
(->* in out : (list (make-Latent-Restrict-Effect t 0)) (list (make-Latent-Remove-Effect t 0)))]
[(t) (make-pred-ty (list Univ) B t)]))
(define -Pathlike (*Un -Path -String))

13
collects/typed-scheme/private/type-effect-printer.ss
View File

@ -32,10 +32,10 @@
(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)")]
[(Latent-Restrict-Effect: t k) (fp "(restrict ~a ~a)" t k)]
[(Latent-Remove-Effect: t k) (fp "(remove ~a ~a)" t k)]
[(Latent-Var-True-Effect: k) (fp "(var #t ~a)" k)]
[(Latent-Var-False-Effect: k) (fp "(var #f ~a)" k)]
[(True-Effect:) (fp "T")]
[(False-Effect:) (fp "F")]
[(Var-True-Effect: v) (fp "(var #t ~a)" (syntax-e v))]
@ -64,9 +64,10 @@
(when drest
(fp "~a ... ~a " (car drest) (cdr drest)))
(fp "-> ~a" rng)
(match* (thn-eff els-eff)
(match* (thn-eff els-eff)
[((list) (list)) (void)]
[((list (Latent-Restrict-Effect: t)) (list (Latent-Remove-Effect: t))) (fp " : ~a" t)]
[((list (Latent-Restrict-Effect: t 0)) (list (Latent-Remove-Effect: t 0))) (fp " : ~a" t)]
[((list (Latent-Restrict-Effect: t k)) (list (Latent-Remove-Effect: t k))) (fp " : ~a_~a" t k)]
[(_ _) (fp " : ~a ~a" thn-eff els-eff)])
(fp ")")]))
(define (tuple? t)

14
collects/typed-scheme/rep/effect-rep.ss
View File

@ -27,13 +27,19 @@
[#:fold-rhs (*Remove-Effect (type-rec-id t) v)])
;; t is a Type
(de Latent-Restrict-Effect (t))
;; k is a nat
(de Latent-Restrict-Effect (t k) [#:frees (free-vars* t) (free-idxs* t)]
[#:fold-rhs (*Latent-Restrict-Effect (type-rec-id t) k)])
;; t is a Type
(de Latent-Remove-Effect (t))
;; k is a nat
(de Latent-Remove-Effect (t k) [#:frees (free-vars* t) (free-idxs* t)]
[#:fold-rhs (*Latent-Remove-Effect (type-rec-id t) k)])
(de Latent-Var-True-Effect () [#:frees #f] [#:fold-rhs #:base])
;; k is a nat
(de Latent-Var-True-Effect (k) [#:frees #f] [#:fold-rhs #:base])
(de Latent-Var-False-Effect () [#:frees #f] [#:fold-rhs #:base])
;; k is a nat
(de Latent-Var-False-Effect (k) [#:frees #f] [#:fold-rhs #:base])
;; could also have latent true/false effects, but seems pointless

2
collects/typed-scheme/rep/rep-utils.ss
View File

@ -11,7 +11,7 @@
scheme/base
syntax/struct
syntax/stx
(utils utils)))
(except-in (utils utils))))
(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq)

146
collects/typed-scheme/ts-reference.scrbl
View File

@ -19,25 +19,33 @@
@section[#:tag "type-ref"]{Type Reference}
@subsubsub*section{Base Types}
These types represent primitive Scheme data.
@defidform[Number]{A @gtech{number}}
@defidform[Integer]{An @gtech{integer}}
@defidform[Boolean]{Either @scheme[#t] or @scheme[#f]}
@defidform[String]{A @gtech{string}}
@defidform[Keyword]{A literal @gtech{keyword}}
@defidform[Symbol]{A @gtech{symbol}}
@defidform[Void]{@|void-const|}
@defidform[Port]{A @gtech{port}}
@defidform[Path]{A @rtech{path}}
@defidform[Char]{A @gtech{character}}
@deftogether[(
@defidform[Number]
@defidform[Integer]
@defidform[Boolean]
@defidform[String]
@defidform[Keyword]
@defidform[Symbol]
@defidform[Void]
@defidform[Input-Port]
@defidform[Output-Port]
@defidform[Path]
@defidform[Regexp]
@defidform[PRegexp]
@defidform[Syntax]
@defidform[Bytes]
@defidform[Namespace]
@defidform[EOF]
@defidform[Char])]{
These types represent primitive Scheme data.}
@defidform[Any]{Any value}
@defidform[Any]{Any Scheme value. All other types are subtypes of @scheme[Any].}
The following base types are parameteric in their type arguments.
@defform[(Listof t)]{Homogenous @gtech{lists} of @scheme[t]}
@defform[(Boxof t)]{A @gtech{box} of @scheme[t]}
@defform[(Vectorof t)]{Homogenous @gtech{vectors} of @scheme[t]}
@defform[(Listof t)]{Homogenous @rtech{lists} of @scheme[t]}
@defform[(Boxof t)]{A @rtech{box} of @scheme[t]}
@defform[(Vectorof t)]{Homogenous @rtech{vectors} of @scheme[t]}
@defform[(Option t)]{Either @scheme[t] of @scheme[#f]}
@defform*[[(Parameter t)
(Parameter s t)]]{A @rtech{parameter} of @scheme[t]. If two type arguments are supplied,
@ -100,46 +108,60 @@ creating new types, and annotating expressions.
@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*[[
(let: ([v : t e] ...) . body)
(let: loop : t0 ([v : t e] ...) . body)]]{
Local bindings, like @scheme[let], each with
associated types. In the second form, @scheme[_t0] is the type of the
result of @scheme[_loop] (and thus the result of the entire
expression as well as the final
expression in @scheme[body]).}
@deftogether[[
@defform[(letrec: ([v : t e] ...) . body)]
@defform[(let*: ([v : t e] ...) . body)]]]{Type-annotated versions of
@scheme[letrec] and @scheme[let*].}
@subsection{Anonymous Functions}
@defform/subs[(lambda: formals . body)
([formals ([v : t] ...)
([v : t] ... . [v : t])])]{
A function of the formal arguments @scheme[v], where each formal
argument has the associated type. If a rest argument is present, then
it has type @scheme[(Listof t)].}
@defform[(λ: formals . body)]{
An alias for the same form using @scheme[lambda:].}
@defform[(plambda: (a ...) formals . body)]{
A polymorphic function, abstracted over the type variables
@scheme[a]. The type variables @scheme[a] are bound in both the types
of the formal, and in any type expressions in the @scheme[body].}
@defform[(case-lambda: [formals body] ...)]{
A function of multiple arities. Note that each @scheme[formals] must have a
different arity.}
@defform[(pcase-lambda: (a ...) [formals body] ...)]{
A polymorphic function of multiple arities.}
@subsection{Definitions}
@defform*[[(define: v : t e)
(define: (f [v : t] ...) : t . body)
(define: (a ...) (f [v : t] ...) : t . body)]]{
(define: (f . formals) : t . body)
(define: (a ...) (f . formals) : t . body)]]{
These forms define variables, with annotated types. The first form
defines @scheme[v] with type @scheme[t] and value @scheme[e]. The
second and third forms defines a function @scheme[f] with appropriate
types. In most cases, use of @scheme[:] is preferred to use of @scheme[define:].}
@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 second element of a @scheme[lambda:].}
@subsection{Structure Definitions}
@defform*[[
(define-struct: name ([f : t] ...))
(define-struct: (name parent) ([f : t] ...))
(define-struct: (v ...) name ([f : t] ...))
(define-struct: (v ...) (name parent) ([f : t] ...))]]{
@defform/subs[
(define-struct: maybe-type-vars name-spec ([f : t] ...))
([maybe-type-vars code:blank (v ...)]
[name-spec name (name parent)])]{
Defines a @rtech{structure} with the name @scheme[name], where the
fields @scheme[f] have types @scheme[t]. The second and fourth forms
define @scheme[name] to be a substructure of @scheme[parent]. The
last two forms define structures that are polymorphic in the type
fields @scheme[f] have types @scheme[t]. When @scheme[parent], the
structure is a substructure of @scheme[parent]. When
@scheme[maybe-type-vars] is present, the structure is polymorphic in the type
variables @scheme[v].}
@subsection{Type Aliases}
@ -172,7 +194,7 @@ This is legal only in expression contexts.}
appropriate number of type variables. This is legal only in expression
contexts.}
@litchar|{#{e @ t ...}}| This is identical to @scheme[(inst e t ...)].
@schemevarfont|{#{e @ t ...}}| This is identical to @scheme[(inst e t ...)].
@subsection{Require}
@ -183,7 +205,16 @@ naming a predicate, and @scheme[_r] is an optionally-renamed identifier.
(require/typed r t m)
(require/typed m [r t] ...)
]]{The first form requires @scheme[r] from module @scheme[m], giving
it type @scheme[t]. The second form generalizes this to multiple identifiers.}
it type @scheme[t]. The second form generalizes this to multiple
identifiers.
In both cases, the identifiers are protected with @rtech{contracts} which
enforce the type @scheme[t]. If this contract fails, the module
@scheme[m] is blamed.
Some types, notably polymorphic types constructed with @scheme[All],
cannot be converted to contracts and raise a static error when used in
a @scheme[require/typed] form.}
@defform[(require/opaque-type t pred m)]{
This defines a new type @scheme[t]. @scheme[pred], imported from
@ -191,4 +222,23 @@ module @scheme[m], is a predicate for this type. The type is defined
as precisely those values to which @scheme[pred] produces
@scheme[#t]. @scheme[pred] must have type @scheme[(Any -> Boolean)].}
@defform[(require-typed-struct name ([f : t] ...) m)]{}
@defform*[[(require-typed-struct name ([f : t] ...) m)
(require-typed-struct (name parent) ([f : t] ...) m)]]{
Requires all the functions associated with the structure @scheme[name] from the module @scheme[m],
with the appropriate types. The structure predicate has the
appropriate Typed Scheme filter type so that it may be used as a
predicate in @scheme[if] expressions in Typed Scheme.
In the second form, @scheme[parent] must already be a structure type
known to Typed Scheme, either via @scheme[define-struct:] or
@scheme[require-typed-struct].
}
@defform/subs[(do: : u ([id : t init-expr step-expr-maybe] ...)
(stop?-expr finish-expr ...)
expr ...+)
([step-expr-maybe code:blank
step-expr])]{
Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and
the final body @scheme[expr] having the type @scheme[u].
}

5
collects/typed-scheme/typecheck/check-subforms-unit.ss
View File

@ -12,7 +12,7 @@
(export check-subforms^)
;; find the subexpressions that need to be typechecked in an ignored form
;; syntax -> void
;; syntax -> any
(define (check-subforms/with-handlers form)
(define handler-tys '())
(define body-ty #f)
@ -48,6 +48,7 @@
[_ (void)])))
(ret (apply Un body-ty handler-tys)))
;; syntax type -> any
(define (check-subforms/with-handlers/check form expected)
(let loop ([form form])
(parameterize ([current-orig-stx form])
@ -73,7 +74,7 @@
(ret expected))
;; typecheck the expansion of a with-handlers form
;; syntax -> type
;; syntax -> any
(define (check-subforms/ignore form)
(let loop ([form form])
(kernel-syntax-case* form #f ()

39
collects/typed-scheme/typecheck/signatures.ss
View File

@ -1,28 +1,49 @@
#lang scheme/base
(require scheme/unit)
(require scheme/unit scheme/contract "../utils/utils.ss")
(require (rep type-rep)
(utils unit-utils)
(private type-utils))
(provide (all-defined-out))
(define-signature typechecker^
(type-check tc-toplevel-form))
([cnt type-check (syntax? . -> . syntax?)]
[cnt tc-toplevel-form (syntax? . -> . any)]))
(define-signature tc-expr^
(tc-expr tc-expr/check tc-expr/check/t check-below tc-literal tc-exprs tc-exprs/check tc-expr/t))
([cnt tc-expr (syntax? . -> . tc-result?)]
[cnt tc-expr/check (syntax? Type? . -> . tc-result?)]
[cnt tc-expr/check/t (syntax? Type? . -> . Type?)]
[cnt check-below (->d ([s (or/c Type? tc-result?)] [t Type?]) () [_ (if (Type? s) Type? tc-result?)])]
[cnt tc-literal (any/c . -> . Type?)]
[cnt tc-exprs ((listof syntax?) . -> . tc-result?)]
[cnt tc-exprs/check ((listof syntax?) Type? . -> . tc-result?)]
[cnt tc-expr/t (syntax? . -> . Type?)]))
(define-signature check-subforms^
(check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check))
([cnt check-subforms/ignore (syntax? . -> . any)]
[cnt check-subforms/with-handlers (syntax? . -> . any)]
[cnt check-subforms/with-handlers/check (syntax? Type? . -> . any)]))
(define-signature tc-if^
(tc/if-onearm tc/if-twoarm tc/if-onearm/check tc/if-twoarm/check))
([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/if-twoarm/check (syntax? syntax? syntax? Type? . -> . tc-result?)]))
(define-signature tc-lambda^
(tc/lambda tc/lambda/check tc/rec-lambda/check))
([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/lambda/check (syntax? syntax? syntax? Type? . -> . tc-result?)]
[cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type?) Type? . -> . Type?)]))
(define-signature tc-app^
(tc/app tc/app/check tc/funapp))
([cnt tc/app (syntax? . -> . tc-result?)]
[cnt tc/app/check (syntax? Type? . -> . tc-result?)]
[cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type?) . -> . tc-result?)]))
(define-signature tc-let^
(tc/let-values tc/letrec-values tc/let-values/check tc/letrec-values/check))
([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/let-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)]
[cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)]))
(define-signature tc-dots^
(tc/dots))
([cnt tc/dots (syntax? . -> . (values Type? symbol?))]))

74
collects/typed-scheme/typecheck/tc-app-unit.ss
View File

@ -2,6 +2,8 @@
(require (only-in "../utils/utils.ss" debug in-syntax printf/log in-pairs rep utils private env [infer r:infer]))
(require "signatures.ss"
stxclass
(for-syntax stxclass)
(rep type-rep effect-rep)
(utils tc-utils)
(private subtype type-utils union type-effect-convenience type-effect-printer resolve-type
@ -359,7 +361,7 @@
"")))))
(define-syntax (handle-clauses stx)
(syntax-case stx ()
(syntax-parse stx
[(_ (lsts ... rngs) f-stx pred infer t argtypes expected)
(with-syntax ([(vars ... rng) (generate-temporaries #'(lsts ... rngs))])
(syntax/loc stx
@ -368,8 +370,8 @@
(let ([substitution (infer vars ... rng)])
(and substitution
(log-result substitution)
(or expected
(ret (subst-all substitution rng))))))
(ret (or expected
(subst-all substitution rng))))))
(poly-fail t argtypes #:name (and (identifier? f-stx) f-stx)))))]))
(define (poly-fail t argtypes #:name [name #f])
@ -501,6 +503,40 @@
(check-below t expected)
(ret expected))
(define-syntax-class lv-clause
#:transparent
(pattern [(v:id ...) e:expr]))
(define-syntax-class lv-clauses
#:transparent
(pattern (cl:lv-clause ...)
#:with (e ...) #'(cl.e ...)
#:with (vs ...) #'((cl.v ...) ...)))
(define-syntax-class core-expr
#:literals (reverse letrec-syntaxes+values let-values #%plain-app
if letrec-values begin #%plain-lambda set! case-lambda
begin0 with-continuation-mark)
#:transparent
(pattern (let-values cls:lv-clauses body)
#:with (expr ...) #'(cls.e ... body))
(pattern (letrec-values cls:lv-clauses body)
#:with (expr ...) #'(cls.e ... body))
(pattern (letrec-syntaxes+values _ cls:lv-clauses body)
#:with (expr ...) #'(cls.e ... body))
(pattern (#%plain-app expr ...))
(pattern (if expr ...))
(pattern (with-continuation-mark expr ...))
(pattern (begin expr ...))
(pattern (begin0 expr ...))
(pattern (#%plain-lambda _ e)
#:with (exprs ...) #'(e))
(pattern (case-lambda [_ exprs] ...))
(pattern (set! _ e)
#:with (exprs ...) #'(e))
(pattern _
#:with (exprs ...) #'()))
;; expr id -> type or #f
;; if there is a binding in stx of the form:
;; (let ([x (reverse name)]) e)
@ -508,28 +544,20 @@
(define (find-annotation stx name)
(define (find s) (find-annotation s name))
(define (match? b)
(kernel-syntax-case* b #f (reverse)
[[(v) (#%plain-app reverse n)]
(free-identifier=? name #'n)
(begin ;(printf "found annotation: ~a ~a~n~a~n" (syntax-e name) (syntax-e #'v) (type-annotation #'v))
(type-annotation #'v))]
(syntax-parse b
#:literals (#%plain-app reverse)
[c:lv-clause
#:with (#%plain-app reverse n:id) #'c.e
#:when (free-identifier=? name #'n)
(type-annotation #'v)]
[_ #f]))
(kernel-syntax-case*
stx #f (reverse letrec-syntaxes+values)
[(let-values (binding ...) body)
(cond [(ormap match? (syntax->list #'(binding ...)))]
(syntax-parse stx
#:literals (let-values)
[(let-values cls:lv-clauses body)
(cond [(ormap match? (syntax->list #'cls))]
[else (find #'body)])]
[(#%plain-app e ...) (ormap find (syntax->list #'(e ...)))]
[(if e1 e2 e3) (ormap find (syntax->list #'(e1 e2 e3)))]
[(letrec-values ([(v ...) e] ...) b)
(ormap find (syntax->list #'(e ... b)))]
[(letrec-syntaxes+values _ ([(v ...) e] ...) b)
(ormap find (syntax->list #'(e ... b)))]
[(begin . es)
(ormap find (syntax->list #'es))]
[(#%plain-lambda (v ...) e)
(find #'e)]
[_ #f]))
[e:core-expr
(ormap find (syntax->list #'e.exprs))]))
(define (check-do-make-object cl pos-args names named-args)

44
collects/typed-scheme/typecheck/tc-expr-unit.ss
View File

@ -5,12 +5,14 @@
(require syntax/kerncase
scheme/match
"signatures.ss"
(r:private type-utils type-effect-convenience union subtype parse-type type-annotation)
(r:private type-utils type-effect-convenience union subtype
parse-type type-annotation stxclass-util)
(rep type-rep effect-rep)
(utils tc-utils)
(env lexical-env)
(only-in (env type-environments) lookup current-tvars extend-env)
scheme/private/class-internal
(except-in stxclass id)
(only-in srfi/1 split-at))
(require (for-template scheme/base scheme/private/class-internal))
@ -22,28 +24,23 @@
;; return the type of a literal value
;; scheme-value -> type
(define (tc-literal v-stx)
;; find the meet of the types of a list of expressions
;; list[syntax] -> type
(define (types-of-literals es)
(apply Un (map tc-literal es)))
(define v (syntax-e v-stx))
(cond
[(exact-integer? v) -Integer]
[(number? v) N]
[(char? v) -Char]
[(boolean? v) (-val v)]
[(null? v) (-val null)]
[(symbol? v) (-val v)]
[(string? v) -String]
[(keyword? v) (-val v)]
[(bytes? v) -Bytes]
[(list? v) (-Tuple (map tc-literal v))]
[(vector? v) (make-Vector (types-of-literals (vector->list v)))]
[(pregexp? v) -PRegexp]
[(byte-pregexp? v) -Byte-PRegexp]
[(byte-regexp? v) -Byte-Regexp]
[(regexp? v) -Regexp]
[else Univ]))
(syntax-parse v-stx
[i:boolean (-val #'i.datum)]
[i:identifier (-val #'i.datum)]
[i:exact-integer -Integer]
[i:number N]
[i:str -String]
[i:char -Char]
[i:keyword (-val #'i.datum)]
[i:bytes -Bytes]
[i:byte-pregexp -Byte-PRegexp]
[i:byte-regexp -Byte-Regexp]
[i:regexp -Regexp]
[(i ...)
(-Tuple (map tc-literal (syntax->list #'(i ...))))]
[i #:declare i (3d vector?)
(make-Vector (apply Un (map tc-literal (vector->list #'i.datum))))]
[_ Univ]))
;; do-inst : syntax type -> type
@ -190,7 +187,6 @@
(begin (tc-exprs/check (syntax->list #'es) Univ)
(tc-expr/check #'e expected))]
;; if
[(if tst body) (tc/if-onearm/check #'tst #'body expected)]
[(if tst thn els) (tc/if-twoarm/check #'tst #'thn #'els expected)]
;; lambda
[(#%plain-lambda formals . body)

4
collects/typed-scheme/typecheck/tc-lambda-unit.ss
View File

@ -199,16 +199,18 @@
(cons (car bodies) bodies*)
(cons (syntax-len (car formals)) nums-seen))]))))
;; tc/lambda : syntax syntax-list syntax-list -> tc-result
(define (tc/lambda form formals bodies)
(tc/lambda/internal form formals bodies #f))
;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic
;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> Type
;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result
(define (tc/lambda/internal form formals bodies expected)
(if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected))
(tc/plambda form formals bodies expected)
(ret (tc/mono-lambda formals bodies expected))))
;; tc/lambda : syntax syntax-list syntax-list Type -> tc-result
(define (tc/lambda/check form formals bodies expected)
(tc/lambda/internal form formals bodies expected))

4
collects/typed-scheme/utils/utils.ss
View File

@ -3,7 +3,8 @@
(require (for-syntax scheme/base)
mzlib/plt-match
scheme/require-syntax
mzlib/struct)
mzlib/struct
(except-in stxclass id))
(provide with-syntax* syntax-map start-timing do-time reverse-begin printf/log
with-logging-to-file log-file-name ==
@ -222,3 +223,4 @@
;; pads out t to be as long as s
(define (extend s t extra)
(append t (build-list (- (length s) (length t)) (lambda _ extra))))