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

Make type->contract correctly respect variance.

Browse Source 
Track whether we are protecting values from the typed side and/or the
untyped side.

Closes PR 13662.
Closes PR 13663.
Closes PR 13665.

original commit: b5b13222c8eaf7e2152b77ab21d21568103c55c8
This commit is contained in:
Eric Dobson 2013-04-06 13:32:04 -07:00
parent 083f913c7c
commit 479f3be677
4 changed files with 100 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
collects/tests/typed-racket/fail/pr13662.rkt Normal file
View File

@ -0,0 +1,20 @@
#;
(exn-pred #rx"contract violation" #rx"blaming: untyped")
#lang racket/load
(module typed typed/racket
(provide b g)
(: b (Boxof (All (a) (a -> a))))
(define b ((inst box (All (a) (a -> a))) (lambda (a) a)))
(: g (Integer -> Integer))
(define (g x)
((unbox b) x)))
(module untyped racket
(require 'typed)
(set-box! b (lambda (x) "hello"))
(g 5))
(require 'untyped)

17
collects/tests/typed-racket/fail/pr13663.rkt Normal file
View File

@ -0,0 +1,17 @@
#;
(exn-pred #rx"contract violation" #rx"blaming: top-level")
#lang racket/load
(module typed typed/racket
(provide g)
(: f (Byte -> Natural))
(define (f x) (add1 x))
(: g ((Boxof Any) -> Void))
(define (g b)
(set-box! b f)))
(require 'typed)
(define b (box #f))
(g b)
(displayln ((unbox b) "foo"))

23
collects/tests/typed-racket/fail/pr13665.rkt Normal file
View File

@ -0,0 +1,23 @@
#;
(exn-pred #rx"contract violation"
#rx"higher-order value passed as `Any` in untyped code"
#rx"blaming: top-level")
#lang racket/load
(module typed typed/racket
(provide g)
(define-type Foo (Rec a (U (List Any) (Boxof a))))
(: f (Byte -> Natural))
(define (f x) (add1 x))
(: g (Foo -> Void))
(define (g b)
(when (box? b)
(set-box! b (list f)))))
(require 'typed)
(define b (box (list #f)))
(g b)
(displayln ((first (unbox b)) "foo"))

60
collects/typed-racket/private/type-contract.rkt
View File

@ -116,17 +116,36 @@
(define (contract-kind->keyword sym)
(string->keyword (symbol->string sym)))
(define (type->contract ty fail #:typed-side [from-typed? #t] #:kind [kind 'impersonator])
(define (from-typed? side)
(case side
[(typed both) #t]
[(untyped) #f]))
(define (from-untyped? side)
(case side
[(untyped both) #t]
[(typed) #f]))
(define (flip-side side)
(case side
[(typed) 'untyped]
[(untyped) 'typed]
[(both) 'both]))
(define (type->contract ty fail #:typed-side [typed-side #t] #:kind [kind 'impersonator])
(define vars (make-parameter '()))
(define current-contract-kind (make-parameter flat-sym))
(define (increase-current-contract-kind! kind)
(current-contract-kind (contract-kind-max (current-contract-kind) kind)))
(let/ec exit
(let loop ([ty ty] [pos? #t] [from-typed? from-typed?] [structs-seen null] [kind kind])
(let loop ([ty ty] [typed-side (if typed-side 'typed 'untyped)] [structs-seen null] [kind kind])
(define (t->c t #:seen [structs-seen structs-seen] #:kind [kind kind])
(loop t pos? from-typed? structs-seen kind))
(loop t typed-side structs-seen kind))
(define (t->c/neg t #:seen [structs-seen structs-seen] #:flat [kind kind])
(loop t (not pos?) (not from-typed?) structs-seen kind))
(loop t (flip-side typed-side) structs-seen kind))
(define (t->c/both t #:seen [structs-seen structs-seen] #:flat [kind kind])
(loop t 'both structs-seen kind))
(define (t->c/fun f #:method [method? #f])
(match f
[(Function: (list (top-arr:))) #'(case->)]
@ -205,7 +224,7 @@
(and rst (t->c/neg rst))))]
;; functions with filters or objects
[(arr: dom (Values: (list (Result: rngs _ _) ...)) rst #f '())
(if from-typed?
(if (not (from-untyped? typed-side))
(values (map t->c/neg dom)
null
(map t->c rngs)
@ -250,13 +269,13 @@
[(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
;; any/c doesn't provide protection in positive position
[(Univ:)
(cond [from-typed?
(cond [(from-typed? typed-side)
(set-chaperone!)
#'any-wrap/c]
[else #'any/c])]
;; we special-case lists:
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
(if (and (not from-typed?) (type-equal? elem-ty t:Univ))
(if (and (not (from-typed? typed-side)) (type-equal? elem-ty t:Univ))
#'list?
#`(listof #,(t->c elem-ty)))]
[(? (lambda (e) (eq? t:Any-Syntax e))) #'syntax?]
@ -331,13 +350,13 @@
[(Sequence: ts) #`(sequence/c #,@(map t->c ts))]
[(Vector: t)
(set-chaperone!)
#`(vectorof #,(t->c t))]
#`(vectorof #,(t->c/both t))]
[(HeterogeneousVector: ts)
(set-chaperone!)
#`(vector/c #,@(map t->c ts))]
#`(vector/c #,@(map t->c/both ts))]
[(Box: t)
(set-chaperone!)
#`(box/c #,(t->c t))]
#`(box/c #,(t->c/both t))]
[(Pair: t1 t2)
#`(cons/c #,(t->c t1) #,(t->c t2))]
[(Promise: t)
@ -347,20 +366,20 @@
#`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))]
[(Continuation-Mark-Keyof: t)
(set-chaperone!)
#`(continuation-mark-key/c #,(t->c t))]
#`(continuation-mark-key/c #,(t->c/both t))]
;; TODO: this is not quite right for case->
[(Prompt-Tagof: s (Function: (list (arr: (list ts ...) _ _ _ _))))
(set-chaperone!)
#`(prompt-tag/c #,@(map t->c ts) #:call/cc #,(t->c s))]
#`(prompt-tag/c #,@(map t->c/both ts) #:call/cc #,(t->c/both s))]
;; TODO
[(F: v) (cond [(assoc v (vars)) => second]
[else (int-err "unknown var: ~a" v)])]
[(Poly: vs b)
(if from-typed?
;; in positive position, no checking needed for the variables
(if (not (from-untyped? typed-side))
;; in typed positions, no checking needed for the variables
(parameterize ([vars (append (for/list ([v vs]) (list v #'any/c)) (vars))])
(t->c b))
;; in negative position, use `parameteric/c'
;; in untyped positions, use `parameteric/c'
(match-let ([(Poly-names: vs-nm _) ty])
(with-syntax ([(v ...) (generate-temporaries vs-nm)])
(set-impersonator!)
@ -372,12 +391,12 @@
(with-syntax ([(n*) (generate-temporaries (list n-nm))])
(parameterize ([vars (cons (list n #'n*) (vars))]
[current-contract-kind
(contract-kind-min kind chaperone-sym)])
(define ctc (t->c b))
(contract-kind-min kind chaperone-sym)])
(define ctc (t->c/both b))
#`(letrec ([n* (recursive-contract
#,ctc
#,(contract-kind->keyword
(current-contract-kind)))])
(current-contract-kind)))])
n*))))]
[(Instance: (? Mu? t))
(t->c (make-Instance (resolve-once t)))]
@ -410,10 +429,11 @@
(with-syntax* ([rec (generate-temporary 'rec)])
(define required-recursive-kind
(contract-kind-min kind (if mut? impersonator-sym chaperone-sym)))
(define t->c/mut (if mut? t->c/both t->c))
;(printf "kind: ~a mut-k: ~a req-rec-kind: ~a\n" kind (if mut? impersonator-sym chaperone-sym) required-recursive-kind)
(parameterize ((current-contract-kind (contract-kind-min kind chaperone-sym)))
(let ((fld-ctc (t->c fty #:seen (cons (cons ty #'rec) structs-seen)
#:kind required-recursive-kind)))
(let ((fld-ctc (t->c/mut fty #:seen (cons (cons ty #'rec) structs-seen)
#:kind required-recursive-kind)))
#`(let ((rec (recursive-contract struct-ctc #,(contract-kind->keyword (current-contract-kind)))))
#,fld-ctc))))))
#`(letrec ((struct-ctc (struct/c #,nm #,@field-contracts))) struct-ctc))]