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

initial intersection types addition

Browse Source 
Adds intersection types as a better way to handle the the case
when restrict cannot structurally intersect two types (e.g. when
you learn within a polymorphic function a variable x of type A
is also an Integer, but we dont know how A relates to Integer).
This allows for non-lossy refinements of type info while typechecking.
This commit is contained in:
Andrew Kent 2016-04-25 23:36:54 -04:00
parent 5552101f5b
commit b4a4c174e4
18 changed files with 212 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
typed-racket-lib/typed-racket/base-env/base-types-extra.rkt
View File

@ -22,7 +22,8 @@
(define-other-types
-> ->* case-> U Rec All Opaque Vector
Parameterof List List* Class Object Unit Values AnyValues Instance Refinement
pred Struct Struct-Type Prefab Top Bot Distinction Sequenceof)
pred Struct Struct-Type Prefab Top Bot Distinction Sequenceof
∩)
(provide (rename-out [All ∀]
[U Un]

4
typed-racket-lib/typed-racket/env/init-envs.rkt vendored
View File

@ -13,7 +13,7 @@
(rep type-rep object-rep prop-rep rep-utils free-variance)
(for-syntax syntax/parse racket/base)
(types abbrev union)
racket/dict racket/list racket/promise
racket/dict racket/list racket/set racket/promise
mzlib/pconvert racket/match)
(provide ;; convenience form for defining an initial environment
@ -84,6 +84,8 @@
`(->acc (list ,@(map sub dom)) ,(sub t) ,(sub pth))]
[(Result: t (PropSet: (TrueProp:) (TrueProp:)) (Empty:)) `(-result ,(sub t))]
[(Union: elems) (split-union elems)]
[(Intersection: elems) `(make-Intersection (set ,@(for/list ([elem (in-immutable-set elems)])
(sub elem))))]
[(Base: n cnt pred _) (int-err "Base type ~a not in predefined-type-table" n)]
[(Name: stx args struct?)
`(make-Name (quote-syntax ,stx) ,args ,struct?)]

15
typed-racket-lib/typed-racket/infer/infer-unit.rkt
View File

@ -19,7 +19,7 @@
"constraint-structs.rkt"
"signatures.rkt" "fail.rkt"
"promote-demote.rkt"
racket/match
racket/match racket/set
mzlib/etc
(contract-req)
(for-syntax
@ -525,6 +525,19 @@
[((? Mu? s) t) (cg (unfold s) t)]
[(s (? Mu? t)) (cg s (unfold t))]
;; find *an* element of elems which can be made a subtype of T
[((Intersection: ts) T)
(cset-join
(for*/list ([t (in-immutable-set ts)]
[v (in-value (cg t T))]
#:when v)
v))]
;; constrain S to be below *each* element of elems, and then combine the constraints
[(S (Intersection: ts))
(define cs (for/list/fail ([ts (in-immutable-set ts)]) (cg S ts)))
(and cs (cset-meet* (cons empty cs)))]
;; constrain *each* element of es to be below T, and then combine the constraints
[((Union: es) T)
(define cs (for/list/fail ([e (in-list es)]) (cg e T)))

42
typed-racket-lib/typed-racket/infer/restrict.rkt
View File

@ -12,8 +12,7 @@
;; restrict t1 to be a subtype of t2
;; if `pref' is 'new, use t2 when giving up, otherwise use t1
(define (restrict t1 t2 [pref 'new])
(define (restrict t1 t2)
;; build-type: build a type while propogating bottom
(define (build-type constructor . args)
(if (memf Bottom? args) -Bottom (apply constructor args)))
@ -21,7 +20,7 @@
;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
;; subtyping performs a similar check for the same
;; reason
(define (restrict* t1 t2 pref resolved)
(define (restrict* t1 t2 resolved)
(match* (t1 t2)
;; already a subtype
[(_ _) #:when (subtype t1 t2)
@ -34,35 +33,40 @@
;; structural recursion on types
[((Pair: a1 d1) (Pair: a2 d2))
(build-type -pair
(restrict* a1 a2 pref resolved)
(restrict* d1 d2 pref resolved))]
(restrict* a1 a2 resolved)
(restrict* d1 d2 resolved))]
;; FIXME: support structural updating for structs when structs are updated to
;; contain not only *if* they are polymorphic, but *which* fields are too
;;[((Struct: _ _ _ _ _ _)
;; (Struct: _ _ _ _ _ _))]
[((Syntax: t1*) (Syntax: t2*))
(build-type -Syntax (restrict* t1* t2* pref resolved))]
(build-type -Syntax (restrict* t1* t2* resolved))]
[((Promise: t1*) (Promise: t2*))
(build-type -Promise (restrict* t1* t2* pref resolved))]
(build-type -Promise (restrict* t1* t2* resolved))]
;; unions
[((Union: t1s) _) (apply Un (map (λ (t1*) (restrict* t1* t2 pref resolved)) t1s))]
[(_ (Union: t2s)) (apply Un (map (λ (t2*) (restrict* t1 t2* pref resolved)) t2s))]
[((Union: t1s) _) (apply Un (map (λ (t1*) (restrict* t1* t2 resolved)) t1s))]
[(_ (Union: t2s)) (apply Un (map (λ (t2*) (restrict* t1 t2* resolved)) t2s))]
;; intersections
[((Intersection: t1s) _)
(apply -unsafe-intersect (for/list ([t1 (in-immutable-set t1s)])
(restrict* t1 t2 resolved)))]
[(_ (Intersection: t2s))
(apply -unsafe-intersect (for/list ([t2 (in-immutable-set t2s)])
(restrict* t1 t2 resolved)))]
;; resolve resolvable types if we haven't already done so
[((? needs-resolving?) _) #:when (not (set-member? resolved (cons t1 t2)))
(restrict* (resolve t1) t2 pref (set-add resolved (cons t1 t2)))]
(restrict* (resolve t1) t2 (set-add resolved (cons t1 t2)))]
[(_ (? needs-resolving?)) #:when (not (set-member? resolved (cons t1 t2)))
(restrict* t1 (resolve t2) pref (set-add resolved (cons t1 t2)))]
(restrict* t1 (resolve t2) (set-add resolved (cons t1 t2)))]
;; we don't actually want this - want something that's a part of t1
[(_ _) #:when (subtype t2 t1)
t2]
;; there's no overlap, so the restriction is empty
[(_ _) #:when (not (overlap t1 t2))
(Un)]
;; t2 and t1 have a complex relationship, so we punt
[(_ _) (if (eq? pref 'new) t2 t1)]))
(restrict* t1 t2 pref (set)))
;; t2 and t1 have a complex relationship, so we intersect
;; (note: intersection checks for overlap)
[(_ _) (-unsafe-intersect t1 t2)]))
(restrict* t1 t2 (set)))

8
typed-racket-lib/typed-racket/private/parse-type.rkt
View File

@ -2,11 +2,12 @@
;; This module provides functions for parsing types written by the user
(require "../utils/utils.rkt"
(require (rename-in "../utils/utils.rkt" [infer infer-in])
(except-in (rep type-rep object-rep) make-arr)
(rename-in (types abbrev union utils prop-ops resolve
classes prefab signatures)
[make-arr* make-arr])
(only-in (infer-in infer) restrict)
(utils tc-utils stxclass-util literal-syntax-class)
syntax/stx (prefix-in c: (contract-req))
syntax/parse racket/sequence
@ -109,6 +110,7 @@
(define-literal-syntax-class #:for-label Bot)
(define-literal-syntax-class #:for-label Distinction)
(define-literal-syntax-class #:for-label Sequenceof)
(define-literal-syntax-class #:for-label ∩)
;; (Syntax -> Type) -> Syntax Any -> Syntax
;; See `parse-type/id`. This is a curried generalization.
@ -466,6 +468,10 @@
t*))))]
[(:U^ ts ...)
(apply Un (parse-types #'(ts ...)))]
[(:∩^ ts ...)
(for/fold ([ty Univ])
([t (in-list (parse-types #'(ts ...)))])
(restrict ty t))]
[(:quote^ t)
(parse-quoted-type #'t)]
[(:All^ . rest)

28
typed-racket-lib/typed-racket/private/type-contract.rkt
View File

@ -14,10 +14,10 @@
(private parse-type syntax-properties)
racket/match racket/syntax racket/list
racket/format
racket/dict
racket/dict racket/set
syntax/flatten-begin
(only-in (types abbrev) -Bottom -Boolean)
(static-contracts instantiate optimize structures combinators)
(static-contracts instantiate optimize structures combinators constraints)
;; TODO make this from contract-req
(prefix-in c: racket/contract)
(contract-req)
@ -211,6 +211,15 @@
ctc-cache sc-cache)))]
[_ form]))))
;; get-max-contract-kind
;; static-contract -> (or/c 'flat 'chaperone 'impersonator)
;; recurse into a contract finding the max
;; kind (e.g. flat < chaperone < impersonator)
(define (get-max-contract-kind sc)
(define (get-restriction sc)
(sc->constraints sc get-restriction))
(kind-max-max (contract-restrict-value (get-restriction sc))))
;; To avoid misspellings
(define impersonator-sym 'impersonator)
(define chaperone-sym 'chaperone)
@ -385,6 +394,21 @@
(if numeric-sc
(apply or/sc numeric-sc (map t->sc non-numeric))
(apply or/sc (map t->sc elems)))]
[(Intersection: ts)
(define-values (chaperones/impersonators others)
(for/fold ([cs/is null] [others null])
([elem (in-immutable-set ts)])
(define c (t->sc elem))
(if (equal? flat-sym (get-max-contract-kind c))
(values cs/is (cons c others))
(values (cons c cs/is) others))))
(cond
[(> (length chaperones/impersonators) 1)
(fail #:reason (~a "Intersection type contract contains"
" more than 1 non-flat contract: "
type))]
[else
(apply and/sc (append others chaperones/impersonators))])]
[(and t (Function: arrs))
#:when (any->bool? arrs)
;; Avoid putting (-> any T) contracts on struct predicates (where Boolean <: T)

57
typed-racket-lib/typed-racket/rep/type-rep.rkt
View File

@ -8,7 +8,7 @@
;; TODO use contract-req
(require (utils tc-utils)
"rep-utils.rkt" "object-rep.rkt" "prop-rep.rkt" "free-variance.rkt"
racket/match racket/list
racket/match racket/list racket/set
racket/contract
racket/lazy-require
racket/promise
@ -19,6 +19,7 @@
PolyDots-names:
PolyRow-names: PolyRow-fresh:
Type-seq
-unsafe-intersect
Mu-unsafe: Poly-unsafe:
PolyDots-unsafe:
Mu? Poly? PolyDots? PolyRow?
@ -53,8 +54,9 @@
;; Ugly hack - should use units
(lazy-require
("../types/union.rkt" (Un))
("../types/resolve.rkt" (resolve-app)))
("../types/union.rkt" (Un))
("../types/remove-intersect.rkt" (overlap))
("../types/resolve.rkt" (resolve-app)))
(define name-table (make-weak-hasheq))
@ -449,6 +451,55 @@
(define d* (remove-duplicates d))
(if (and (pair? d*) (null? (cdr d*))) (car d*) d*))])
;; Intersection
(def-type Intersection ([elems (and/c (set/c Type/c)
(λ (s) (>= (set-count s) 2)))])
[#:intern (for/set ([e (in-immutable-set elems)])
(Rep-seq e))]
[#:frees (λ (f) (combine-frees (for/list ([elem (in-immutable-set elems)])
(f elem))))]
[#:fold-rhs (let ([elems (for/list ([elem (in-immutable-set elems)])
(type-rec-id elem))])
(apply -unsafe-intersect elems))]
[#:key (let ()
(define d
(let loop ([ts (set->list elems)] [res null])
(cond [(null? ts) res]
[else
(define k (Type-key (car ts)))
(cond [(not k) (list #f)]
[(pair? k) (loop (cdr ts) (append k res))]
[else (loop (cdr ts) (cons k res))])])))
(define d* (remove-duplicates d))
(if (and (pair? d*) (null? (cdr d*))) (car d*) d*))])
;; constructor for intersections
;; in general, intersections should be built
;; using the 'restrict' operator, which worries
;; about actual subtyping, etc...
(define (-unsafe-intersect . ts)
(let loop ([elems (set)]
[ts ts])
(match ts
[(list)
(cond
[(set-empty? elems) (Univ)]
;; size = 1 ?
[(= 1 (set-count elems)) (set-first elems)]
;; size > 1, build an intersection
[else (*Intersection elems)])]
[(cons t ts)
(match t
[(? Bottom?) t]
[(Univ:) (loop elems ts)]
[(Intersection: ts*) (loop (set-union elems ts*) ts)]
[t (cond
[(for/or ([elem (in-immutable-set elems)]) (not (overlap elem t)))
(*Union (list))]
[else (loop (set-add elems t) ts)])])])))
(def-type Univ () [#:frees #f] [#:fold-rhs #:base])
;; in : Type

3
typed-racket-lib/typed-racket/static-contracts/constraints.rkt
View File

@ -61,7 +61,8 @@
contract-restrict-recursive-values
contract-restrict?
)
contract-restrict-value
kind-max-max)
(module structs racket/base
(require racket/contract

10
typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
View File

@ -366,18 +366,18 @@
(define (find-stx-type datum-stx [expected #f])
(match datum-stx
[(? syntax? (app syntax-e stx-e))
(match (and expected (resolve (restrict expected (-Syntax Univ) 'orig)))
(match (and expected (resolve (restrict expected (-Syntax Univ))))
[(Syntax: t) (-Syntax (find-stx-type stx-e t))]
[_ (-Syntax (find-stx-type stx-e))])]
[(or (? symbol?) (? null?) (? number?) (? extflonum?) (? boolean?) (? string?) (? char?)
(? bytes?) (? regexp?) (? byte-regexp?) (? keyword?))
(tc-literal #`#,datum-stx expected)]
[(cons car cdr)
(match (and expected (resolve (restrict expected (-pair Univ Univ) 'orig)))
(match (and expected (resolve (restrict expected (-pair Univ Univ))))
[(Pair: car-t cdr-t) (-pair (find-stx-type car car-t) (find-stx-type cdr cdr-t))]
[_ (-pair (find-stx-type car) (find-stx-type cdr))])]
[(vector xs ...)
(match (and expected (resolve (restrict expected -VectorTop 'orig)))
(match (and expected (resolve (restrict expected -VectorTop)))
[(Vector: t)
(make-Vector
(check-below
@ -393,11 +393,11 @@
[_ (make-HeterogeneousVector (for/list ([x (in-list xs)])
(generalize (find-stx-type x #f))))])]
[(box x)
(match (and expected (resolve (restrict expected -BoxTop 'orig)))
(match (and expected (resolve (restrict expected -BoxTop)))
[(Box: t) (-box (check-below (find-stx-type x t) t))]
[_ (-box (generalize (find-stx-type x)))])]
[(? hash? h)
(match (and expected (resolve (restrict expected -HashTop 'orig)))
(match (and expected (resolve (restrict expected -HashTop)))
[(Hashtable: kt vt)
(define kts (hash-map h (lambda (x y) (find-stx-type x kt))))
(define vts (hash-map h (lambda (x y) (find-stx-type y vt))))

6
typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
View File

@ -89,7 +89,7 @@
[i:regexp -Regexp]
[() -Null]
[(i . r)
(match (and expected (resolve (restrict expected (-pair Univ Univ) 'orig)))
(match (and expected (resolve (restrict expected (-pair Univ Univ))))
[(Pair: a-ty d-ty)
(-pair
(tc-literal #'i a-ty)
@ -97,7 +97,7 @@
[t
(-pair (tc-literal #'i) (tc-literal #'r))])]
[(~var i (3d vector?))
(match (and expected (resolve (restrict expected -VectorTop 'orig)))
(match (and expected (resolve (restrict expected -VectorTop)))
[(Vector: t)
(make-Vector
(check-below
@ -113,7 +113,7 @@
[_ (make-HeterogeneousVector (for/list ([l (in-vector (syntax-e #'i))])
(generalize (tc-literal l #f))))])]
[(~var i (3d hash?))
(match (and expected (resolve (restrict expected -HashTop 'orig)))
(match (and expected (resolve (restrict expected -HashTop)))
[(Hashtable: k v)
(let* ([h (syntax-e #'i)]
[ks (hash-map h (lambda (x y) (tc-literal x k)))]

2
typed-racket-lib/typed-racket/types/printer.rkt
View File

@ -460,6 +460,8 @@
[(Union: elems)
(define-values (covered remaining) (cover-union type ignored-names))
(cons 'U (append covered (map t->s remaining)))]
[(Intersection: elems)
(cons '∩ (for/list ([elem (in-immutable-set elems)]) (t->s elem)))]
[(Pair: l r) `(Pairof ,(t->s l) ,(t->s r))]
[(ListDots: dty dbound) `(List ,(t->s dty) ... ,dbound)]
[(F: nm) nm]

10
typed-racket-lib/typed-racket/types/remove-intersect.rkt
View File

@ -3,7 +3,7 @@
(require "../utils/utils.rkt"
(rep type-rep rep-utils)
(types union subtype resolve utils)
racket/match)
racket/match racket/set)
(provide (rename-out [*remove remove]) overlap)
@ -33,7 +33,7 @@
[else
(match (list t1 t2)
[(list-no-order (Univ:) _) #t]
[(list-no-order (F: _) _) #t]
[(list-no-order (or (B: _) (F: _)) _) #t]
[(list-no-order (Opaque: _) _) #t]
[(list (Name/simple: n) (Name/simple: n*))
(or (free-identifier=? n n*)
@ -44,6 +44,9 @@
[(list-no-order (Refinement: t _) s) (overlap t s)]
[(list-no-order (Union: ts) s)
(ormap (lambda (t*) (overlap t* s)) ts)]
[(list-no-order (Intersection: ts) s)
(for/and ([t (in-immutable-set ts)])
(overlap t s))]
[(list-no-order (? Poly?) _) #t] ;; conservative
[(list (Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))]
[(list-no-order (? Base? t) (? Value? s)) (subtype s t)] ;; conservative
@ -106,6 +109,9 @@
old]
[(list (Union: l) rem)
(apply Un (map (lambda (e) (*remove e rem)) l))]
[(list (Intersection: ts) rem)
(apply -unsafe-intersect
(for/list ([t (in-immutable-set ts)]) (*remove t rem)))]
[(list (? Mu? old) t) (*remove (unfold old) t)]
[(list (Poly: vs b) t) (make-Poly vs (*remove b rem))]
[_ old])))

15
typed-racket-lib/typed-racket/types/subtype.rkt
View File

@ -1,6 +1,7 @@
#lang racket/base
(require (except-in "../utils/utils.rkt" infer)
racket/match racket/function racket/lazy-require racket/list
racket/match racket/function racket/lazy-require
racket/list racket/set
(prefix-in c: (contract-req))
(rep type-rep prop-rep object-rep rep-utils)
(utils tc-utils early-return)
@ -272,6 +273,18 @@
;; value types
[((Value: v1) (Value: v2))
#:when (equal? v1 v2) A0]
[((Intersection: ss) t)
(and
(for/or ([s (in-immutable-set ss)])
(subtype* A0 s t))
A0)]
[(s (Intersection: ts))
(and
(for/fold ([A A0])
([t (in-immutable-set ts)]
#:break (not A))
(subtype* A s t))
A0)]
;; values are subtypes of their "type"
[((Value: v) (Base: _ _ pred _)) (if (pred v) A0 #f)]
;; tvars are equal if they are the same variable

19
typed-racket-test/succeed/intersection1.rkt Normal file
View File

@ -0,0 +1,19 @@
#lang racket/base
(module a typed/racket
(provide num-id)
(: num-id (∀ (A) (-> (∩ Number A) (∩ Number A))))
(define (num-id x) x))
(require 'a)
(let ()
(num-id 42)
(void))
(with-handlers ([exn:fail:contract?
(λ (ex) (void))])
(num-id "42"))

6
typed-racket-test/unit-tests/contract-tests.rkt
View File

@ -354,4 +354,10 @@
(class object% (super-new)
(define/public (m) "m"))
#:untyped)
;; intersection types
(t (-unsafe-intersect (-seq -Symbol) (-pair -Symbol (-lst -Symbol))))
(t/fail (-unsafe-intersect (-Number . -> . -Number) (-String . -> . -String))
"more than 1 non-flat contract")
(t/fail (-unsafe-intersect (-box -Symbol) (-box Univ))
"more than 1 non-flat contract")
))

8
typed-racket-test/unit-tests/parse-type-tests.rkt
View File

@ -406,6 +406,14 @@
;; GH issue #314
[FAIL ~> #:msg "unbound"]
;; intersections
[(∩) Univ]
[(∩ Any) Univ]
[(∩ String Symbol) -Bottom]
[(∩ (-> Number Number) (-> String String))
(-unsafe-intersect (t:-> -String -String)
(t:-> -Number -Number))]
))
;; FIXME - add tests for parse-values-type, parse-tc-results

7
typed-racket-test/unit-tests/remove-intersect-tests.rkt
View File

@ -2,6 +2,7 @@
(require "test-utils.rkt"
(for-syntax racket/base)
(r:infer infer)
(rep type-rep)
(types abbrev numeric-tower subtype union remove-intersect)
rackunit)
(provide tests)
@ -43,7 +44,11 @@
[-Sexp -Listof (-lst -Sexp)]
[(-val "one") -Fixnum (Un)]
[(Un (-val "one") (-val "two")) (Un (-val "one") (-val 1)) (-val "one")]
))
;; intersection cases
[(-v a) -String (-unsafe-intersect (-v a) -String)]
[-String (-v a) (-unsafe-intersect (-v a) -String)]
[(-> -Number -Number) (-> -String -String) (-unsafe-intersect (-> -Number -Number)
(-> -String -String))]))
(define-syntax (remo-tests stx)
(syntax-case stx ()

10
typed-racket-test/unit-tests/subtype-tests.rkt
View File

@ -50,6 +50,16 @@
[(Un (-val #f) (Un (-val 6) (-val 7))) (-mu x (Un -Number (Un -Boolean -Symbol)))]
[(Un -Number (-val #f) (-mu x (Un -Number -Symbol (make-Listof x))))
(-mu x (Un -Number -Symbol -Boolean (make-Listof x)))]
;; intersections
[(-unsafe-intersect -Number) -Number]
[(-unsafe-intersect -Number -Symbol) -Number]
[(-unsafe-intersect -Boolean -Number) -Number]
[(-unsafe-intersect -Number -Number) -Number]
[FAIL -Number (-unsafe-intersect -Boolean -Number)]
[(-unsafe-intersect -Boolean -Number) (-unsafe-intersect -Boolean -Number)]
[(-unsafe-intersect -Sexp
(Un -Null (-pair -Sexp (-unsafe-intersect (make-Listof Univ) -Sexp))))
(make-Listof Univ)]
;; sexps vs list*s of nums
[(-mu x (Un -Number -Symbol (make-Listof x))) (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))]
[(-mu x (Un -Number (make-Listof x))) (-mu x (Un -Number -Symbol (make-Listof x)))]