Use pairs for objects on arrow types
Previously, function types looked something like
U_n|V_n
S ---------> T where n is a natural number representing
∅ a function argument by its index
They now look like
U_(n,m)|V_(n,m)
S -----------------> T where the pair indicates the mth argument
∅ bound by a function n lambdas away
This allows the use of curried predicates in occurrence typing
This commit is contained in:
Asumu Takikawa
parent
7305013934
commit
4c17c2091c
|
|
@ -98,16 +98,16 @@
|
|||
[(TypeFilter: t p i)
|
||||
`(make-TypeFilter ,(sub t) ,(sub p) ,(if (identifier? i)
|
||||
`(quote-syntax ,i)
|
||||
i))]
|
||||
`(list ,(car i) ,(cadr i))))]
|
||||
[(NotTypeFilter: t p i)
|
||||
`(make-NotTypeFilter ,(sub t) ,(sub p)
|
||||
,(if (identifier? i)
|
||||
`(quote-syntax ,i)
|
||||
i))]
|
||||
`(list ,(car i) ,(cadr i))))]
|
||||
[(Path: p i)
|
||||
`(make-Path ,(sub p) ,(if (identifier? i)
|
||||
`(quote-syntax ,i)
|
||||
i))]
|
||||
`(list ,(car i) ,(cadr i))))]
|
||||
[(? Rep? rep)
|
||||
`(,(gen-constructor (car (vector->list (struct->vector rep))))
|
||||
,@(map sub (Rep-values rep)))]
|
||||
|
|
|
|||
|
|
@ -14,8 +14,10 @@
|
|||
'FilterSet
|
||||
(λ (e) (or (FilterSet? e) (NoFilter? e)))))
|
||||
|
||||
|
||||
(define name-ref/c (or/c identifier? integer?))
|
||||
;; A Name-Ref is any value that represents an object.
|
||||
;; As an identifier, it represents a free variable in the environment
|
||||
;; As a list, it represents a De Bruijn indexed bound variable
|
||||
(define name-ref/c (or/c identifier? (list/c integer? integer?)))
|
||||
(define (hash-name v) (if (identifier? v) (hash-id v) (list v)))
|
||||
|
||||
(def-filter Bot () [#:fold-rhs #:base])
|
||||
|
|
|
|||
|
|
@ -11,21 +11,111 @@
|
|||
combine-props
|
||||
tc-results->values)
|
||||
|
||||
;; abstract-results
|
||||
;;
|
||||
;; Given results from the range of a lambda, abstract any
|
||||
;; identifier objects into index (numeric) objects. This is effectively
|
||||
;; doing a kind of De Bruijn indexing for objects.
|
||||
;;
|
||||
;; When the body of a lambda is type-checked, its filters and object
|
||||
;; may refer to variables that are in scope in that body. Since these
|
||||
;; names are not in scope outside of the lambda, the type of the function
|
||||
;; will instead store their De Bruijn indices.
|
||||
;;
|
||||
;; For example, given the function
|
||||
;;
|
||||
;; (λ (x) (number? x))
|
||||
;;
|
||||
;; the typechecker will check the body and return
|
||||
;;
|
||||
;; Boolean ; N_x | !N_x ; ∅
|
||||
;;
|
||||
;; but the `x`s have to be converted to indices to get the type
|
||||
;;
|
||||
;; N_(0,0) | !N_(0,0)
|
||||
;; Any -------------------> Boolean
|
||||
;; ∅
|
||||
;;
|
||||
;; where the index (0,0) indicates the first argument of
|
||||
;; the current function
|
||||
;;
|
||||
;; Comparatively, a curried predicate like
|
||||
;;
|
||||
;; (λ (x) (λ (y)(number? x)))
|
||||
;;
|
||||
;; gets the type
|
||||
;;
|
||||
;; N_(1,0) | !N_(1,0)
|
||||
;; Any -> Any -------------------> Boolean
|
||||
;; ∅
|
||||
;;
|
||||
;; (ignoring filters on the first arrow)
|
||||
;; where the index (1,0) indicates the first argument of
|
||||
;; the enclosing lambda.
|
||||
;;
|
||||
;; The paper "Logical Types for Untyped Languages" takes a different
|
||||
;; approach where all function types carry their names, so that the first
|
||||
;; example would have the type:
|
||||
;;
|
||||
;; N_x | !N_x
|
||||
;; x:Any ------------> Boolean
|
||||
;; ∅
|
||||
;;
|
||||
;; See tc-subst.rkt for the functions that take an abstracted function
|
||||
;; type and substitute in a concrete object.
|
||||
;;
|
||||
(define/cond-contract (abstract-results results arg-names)
|
||||
(tc-results/c (listof identifier?) . -> . SomeValues/c)
|
||||
(define keys (for/list ([(nm k) (in-indexed arg-names)]) k))
|
||||
(define keys (for/list ([(nm k) (in-indexed arg-names)]) (list 0 k)))
|
||||
(match results
|
||||
[(tc-any-results:) (make-AnyValues)]
|
||||
[(tc-results: ts fs os dty dbound)
|
||||
(make-ValuesDots
|
||||
(for/list ([t (in-list ts)] [f (in-list fs)] [o (in-list os)])
|
||||
(make-Result t (abstract-filter arg-names keys f) (abstract-object arg-names keys o)))
|
||||
(make-Result (abstract-type arg-names keys t)
|
||||
(abstract-filter arg-names keys f)
|
||||
(abstract-object arg-names keys o)))
|
||||
dty dbound)]
|
||||
[(tc-results: ts fs os)
|
||||
(make-Values
|
||||
(for/list ([t (in-list ts)] [f (in-list fs)] [o (in-list os)])
|
||||
(make-Result t (abstract-filter arg-names keys f) (abstract-object arg-names keys o))))]))
|
||||
(make-Result (abstract-type arg-names keys t)
|
||||
(abstract-filter arg-names keys f)
|
||||
(abstract-object arg-names keys o))))]))
|
||||
|
||||
;; Abstract all given id objects into index objects (keys) in
|
||||
;; the given type
|
||||
(define/cond-contract (abstract-type ids keys type)
|
||||
(-> (listof identifier?) (listof name-ref/c) Type/c Type/c)
|
||||
(define (at type) (abstract-type ids keys type))
|
||||
(define (af filter) (abstract-filter ids keys filter))
|
||||
(define (ao obj) (abstract-object ids keys obj))
|
||||
(type-case
|
||||
(#:Type at #:Filter af #:Object ao)
|
||||
type
|
||||
[#:arr
|
||||
dom rng rest drest kws
|
||||
(let ([at*
|
||||
;; when a new function type is encountered, increase
|
||||
;; the scope count in the keys so that names are
|
||||
;; substituted with the correct level of nesting
|
||||
(λ (type)
|
||||
(abstract-type ids (add-scope keys) type))])
|
||||
(make-arr (map at dom)
|
||||
(at* rng) ; only increase scope in range
|
||||
(and rest (at rest))
|
||||
(and drest (cons (at (car drest)) (cdr drest)))
|
||||
(map at kws)))]))
|
||||
|
||||
;; add-scope : Listof<name-ref/c> -> Listof<name-ref/c>
|
||||
;; Add a scope to the index object
|
||||
(define (add-scope keys)
|
||||
(for/list ([depth+arg keys])
|
||||
(match-define (list depth arg) depth+arg)
|
||||
(list (+ 1 depth) arg)))
|
||||
|
||||
;; Abstract all given id objects into index objects (keys) in
|
||||
;; the given object
|
||||
(define/cond-contract (abstract-object ids keys o)
|
||||
(-> (listof identifier?) (listof name-ref/c) Object? Object?)
|
||||
(define (lookup y)
|
||||
|
|
@ -37,6 +127,8 @@
|
|||
[(Path: p (lookup: idx)) (make-Path p idx)]
|
||||
[_ -no-obj]))
|
||||
|
||||
;; Abstract all given id objects into index objects (keys) in
|
||||
;; the given filter set
|
||||
(define/cond-contract (abstract-filter ids keys fs)
|
||||
(-> (listof identifier?) (listof name-ref/c) FilterSet/c FilterSet/c)
|
||||
(match fs
|
||||
|
|
@ -47,8 +139,8 @@
|
|||
(define/cond-contract (abo xs idxs f)
|
||||
((listof identifier?) (listof name-ref/c) Filter/c . -> . Filter/c)
|
||||
(define/cond-contract (lookup y)
|
||||
(identifier? . -> . (or/c #f integer?))
|
||||
(for/first ([x (in-list xs)] [i (in-list idxs)] #:when (free-identifier=? x y)) i))
|
||||
(identifier? . -> . (or/c #f (list/c integer? integer?)))
|
||||
(for/first ([x (in-list xs)] [i (in-list idxs)] #:when (free-identifier=? x y)) i))
|
||||
(define-match-expander lookup:
|
||||
(syntax-rules ()
|
||||
[(_ i) (or (? identifier? (app lookup (? values i)))
|
||||
|
|
|
|||
|
|
@ -21,11 +21,12 @@
|
|||
(->* (Result? (listof Object?)) ((listof Type/c)) (values Type/c FilterSet? Object?))
|
||||
(match-define (Result: t fs old-obj) r)
|
||||
(for/fold ([t t] [fs fs] [old-obj old-obj])
|
||||
([(o k) (in-indexed (in-list objs))]
|
||||
([(o arg) (in-indexed (in-list objs))]
|
||||
[arg-ty (if ts (in-list ts) (in-cycle (in-value #f)))])
|
||||
(values (subst-type t k o #t)
|
||||
(subst-filter-set fs k o #t arg-ty)
|
||||
(subst-object old-obj k o #t))))
|
||||
(define key (list 0 arg))
|
||||
(values (subst-type t key o #t)
|
||||
(subst-filter-set fs key o #t arg-ty)
|
||||
(subst-object old-obj key o #t))))
|
||||
|
||||
;; Substitution of objects into a filter set
|
||||
;; This is essentially ψ+|ψ- [o/x] from the paper
|
||||
|
|
@ -54,10 +55,10 @@
|
|||
#:Object (lambda (f) (subst-object f k o polarity)))
|
||||
t
|
||||
[#:arr dom rng rest drest kws
|
||||
;; here we have to increment the count for the domain, where the new bindings are in scope
|
||||
(let* ([arg-count (+ (length dom) (if rest 1 0) (if drest 1 0) (length kws))]
|
||||
[st* (if (integer? k)
|
||||
(λ (t) (subst-type t (if (number? k) (+ arg-count k) k) o polarity))
|
||||
(let* ([st* (if (pair? k)
|
||||
;; Add a scope if we are substituting an index and
|
||||
;; not a free variable by name
|
||||
(λ (t) (subst-type t (add-scope k) o polarity))
|
||||
st)])
|
||||
(make-arr (map st dom)
|
||||
(st* rng)
|
||||
|
|
@ -65,6 +66,11 @@
|
|||
(and drest (cons (st (car drest)) (cdr drest)))
|
||||
(map st kws)))]))
|
||||
|
||||
;; add-scope : name-ref/c -> name-ref/c
|
||||
;; Add a scope from an index object
|
||||
(define (add-scope key)
|
||||
(list (+ (car key) 1) (cadr key)))
|
||||
|
||||
;; Substitution of objects into objects
|
||||
;; This is o [o'/x] from the paper
|
||||
(define/cond-contract (subst-object t k o polarity)
|
||||
|
|
@ -142,9 +148,9 @@
|
|||
#:Object for-object)
|
||||
t
|
||||
[#:arr dom rng rest drest kws
|
||||
;; here we have to increment the count for the domain, where the new bindings are in scope
|
||||
(let* ([arg-count (+ (length dom) (if rest 1 0) (if drest 1 0) (length kws))]
|
||||
[st* (lambda (t) (index-free-in? (if (number? k) (+ arg-count k) k) t))])
|
||||
(let* ([st* (if (pair? k)
|
||||
(lambda (t) (index-free-in? (add-scope k) t))
|
||||
for-type)])
|
||||
(for-each for-type dom)
|
||||
(st* rng)
|
||||
(and rest (for-type rest))
|
||||
|
|
@ -167,8 +173,9 @@
|
|||
(open-Result r (map (lambda (i) (make-Path null i))
|
||||
formals)))])
|
||||
(ret ts fs os
|
||||
(for/fold ([dty dty]) ([(o k) (in-indexed (in-list formals))])
|
||||
(subst-type dty k (make-Path null o) #t))
|
||||
(for/fold ([dty dty]) ([(o idx) (in-indexed (in-list formals))])
|
||||
(define key (list 0 idx))
|
||||
(subst-type dty key (make-Path null o) #t))
|
||||
dbound))
|
||||
(ret ts fs os dty dbound))]
|
||||
[(Values: (list (and rs (Result: ts fs os)) ...))
|
||||
|
|
|
|||
|
|
@ -117,17 +117,23 @@
|
|||
(c:-> Filter/c Filter/c FilterSet?)
|
||||
(make-FilterSet + -))
|
||||
|
||||
;; Abbreviation for filters
|
||||
;; `i` can be an integer for backwards compatibility
|
||||
(define/cond-contract (-filter t i [p null])
|
||||
(c:->* (Type/c name-ref/c) ((c:listof PathElem?)) Filter/c)
|
||||
(if (or (type-equal? Univ t) (and (identifier? i) (is-var-mutated? i)))
|
||||
-top
|
||||
(make-TypeFilter t p i)))
|
||||
(c:->* (Type/c (c:or/c integer? name-ref/c)) ((c:listof PathElem?)) Filter/c)
|
||||
(define i* (if (integer? i) (list 0 i) i))
|
||||
(if (or (type-equal? Univ t) (and (identifier? i) (is-var-mutated? i)))
|
||||
-top
|
||||
(make-TypeFilter t p i*)))
|
||||
|
||||
;; Abbreviation for not filters
|
||||
;; `i` can be an integer for backwards compatibility
|
||||
(define/cond-contract (-not-filter t i [p null])
|
||||
(c:->* (Type/c name-ref/c) ((c:listof PathElem?)) Filter/c)
|
||||
(if (or (type-equal? -Bottom t) (and (identifier? i) (is-var-mutated? i)))
|
||||
-top
|
||||
(make-NotTypeFilter t p i)))
|
||||
(c:->* (Type/c (c:or/c integer? name-ref/c)) ((c:listof PathElem?)) Filter/c)
|
||||
(define i* (if (integer? i) (list 0 i) i))
|
||||
(if (or (type-equal? -Bottom t) (and (identifier? i) (is-var-mutated? i)))
|
||||
-top
|
||||
(make-NotTypeFilter t p i*)))
|
||||
|
||||
(define (-filter-at t o)
|
||||
(match o
|
||||
|
|
@ -199,9 +205,9 @@
|
|||
|
||||
(define (->acc dom rng path)
|
||||
(make-Function (list (make-arr* dom rng
|
||||
#:filters (-FS (-not-filter (-val #f) 0 path)
|
||||
(-filter (-val #f) 0 path))
|
||||
#:object (make-Path path 0)))))
|
||||
#:filters (-FS (-not-filter (-val #f) (list 0 0) path)
|
||||
(-filter (-val #f) (list 0 0) path))
|
||||
#:object (make-Path path (list 0 0))))))
|
||||
|
||||
(define (cl->* . args)
|
||||
(define (funty-arities f)
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@
|
|||
|
||||
|
||||
(define (name-ref=? a b)
|
||||
(or (eq? a b)
|
||||
(or (equal? a b)
|
||||
(and (identifier? a)
|
||||
(identifier? b)
|
||||
(free-identifier=? a b))))
|
||||
|
|
|
|||
|
|
@ -838,9 +838,9 @@
|
|||
;; instantiating non-dotted terms
|
||||
[tc-e/t (inst (plambda: (a) ([x : a]) x) Integer)
|
||||
(make-Function (list (make-arr* (list -Integer) -Integer
|
||||
#:filters (-FS (-not-filter (-val #f) 0)
|
||||
(-filter (-val #f) 0))
|
||||
#:object (make-Path null 0))))]
|
||||
#:filters (-FS (-not-filter (-val #f) (list 0 0))
|
||||
(-filter (-val #f) (list 0 0)))
|
||||
#:object (make-Path null (list 0 0)))))]
|
||||
[tc-e/t (inst (plambda: (a) [x : a *] (apply list x)) Integer)
|
||||
((list) -Integer . ->* . (-lst -Integer))]
|
||||
|
||||
|
|
@ -1765,6 +1765,21 @@
|
|||
(Any -> Boolean : #:+ (Integer @ x) #:- (! Integer @ x))))
|
||||
(if (f 'dummy) (add1 x) 2))
|
||||
(t:-> Univ -Integer : (-FS -top (-filter -Integer 0)))]
|
||||
|
||||
;; This test ensures that curried predicates have
|
||||
;; the correct filters so that they can be used for
|
||||
;; occurrence typing.
|
||||
[tc-e
|
||||
(let ()
|
||||
(define f (λ (x) (λ (y) (number? x))))
|
||||
(: b (U Number String))
|
||||
(define b 5)
|
||||
(define g (f b))
|
||||
;; this doesn't type-check unless OT is working
|
||||
(if (g "foo") (add1 b) 3)
|
||||
(void))
|
||||
;; type doesn't really matter, just make sure it typechecks
|
||||
-Void]
|
||||
)
|
||||
(test-suite
|
||||
"tc-literal tests"
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user