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

Add recursive type alias support to TR

Browse Source 
This expands the `Name` type functionality to go
beyond struct names and allows arbitrary recursive
type aliases to use the environment for indirection.

In addition, such aliases can be mutually recursive.
This commit is contained in:
Asumu Takikawa 2013-07-30 12:21:44 -04:00
parent 389aa9fcd8
commit a8cc430d0f
38 changed files with 1185 additions and 153 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/guide/more.scrbl
View File

@ -207,6 +207,7 @@ Any type can be given a name with @racket[define-type].
@racketblock[(define-type NN (-> Number Number))]
Anywhere the name @racket[NN] is used, it is expanded to
@racket[(-> Number Number)]. Type names may not be recursive.
@racket[(-> Number Number)]. Type names may be recursive
or even mutually recursive.
@(close-eval the-eval)

25
pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl
View File

@ -408,15 +408,34 @@ corresponding to @|define-struct-id| from @racketmodname[racket/base].}
The first form defines @racket[name] as type, with the same meaning as
@racket[t]. The second form is equivalent to
@racket[(define-type name (All (v ...) t))]. Type names may
refer to other types defined in the same module, but
cycles among them are prohibited.
refer to other types defined in the same or enclosing scopes.
@ex[(define-type IntStr (U Integer String))
(define-type (ListofPairs A) (Listof (Pair A A)))]
If @racket[#:omit-define-syntaxes] is specified, no definition of
@racket[name] is created. In this case, some other definition of @racket[name]
is necessary.}
is necessary.
If the body of the type definition refers to itself, then the
type definition is recursive. Recursion may also occur mutually,
if a type refers to a chain of other types that eventually refers
back to itself.
@ex[(define-type BT (U Number (Pair BT BT)))
(let ()
(define-type (Even A) (U Null (Pairof A (Odd A))))
(define-type (Odd A) (Pairof A (Even A)))
(: even-lst (Even Integer))
(define even-lst '(1 2))
even-lst)]
However, the recursive reference may not occur immediately inside
the type:
@ex[(define-type Foo Foo)
(define-type Bar (U Bar False))]
}
@section{Generating Predicates Automatically}

9
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-structs.rkt
View File

@ -35,10 +35,11 @@
...)
...)]))
(define -Srcloc (make-Name #'srcloc))
(define -Date (make-Name #'date))
(define -Arity-At-Least (make-Name #'arity-at-least))
(define -Exn (make-Name #'exn))
(define -Srcloc (make-Name #'srcloc null #f #t))
(define -Date (make-Name #'date null #f #t))
(define -Arity-At-Least
(make-Name #'arity-at-least null #f #t))
(define -Exn (make-Name #'exn null #f #t))
(define (initialize-structs)

35
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt
View File

@ -504,22 +504,35 @@ This file defines two sorts of primitives. All of them are provided into any mod
(syntax/loc stx
((plambda: (A ...) (bn ...) . body) e ...))]))
;; Syntax classes for `define-type-alias`
(begin-for-syntax
(define-syntax-class type-alias-rest
#:literals (All)
#:attributes (args)
(pattern (All (arg:id ...) rest)
#:with args #'(arg ...))
(pattern type:expr #:with args #'#f)))
(define-syntax (define-type-alias stx)
(syntax-parse stx
[(_ tname:id rest (~optional (~and omit #:omit-define-syntaxes)
#:defaults
([omit #f])))
[(_ tname:id rest:type-alias-rest
(~optional (~and omit #:omit-define-syntaxes)
#:defaults
([omit #f])))
(define/with-syntax stx-err-fun
#'(lambda (stx)
(raise-syntax-error
'type-check
"type name used out of context"
stx
(and (stx-pair? stx) (stx-car stx)))))
#`(begin
#,(if (not (attribute omit))
(ignore #'(define-syntax tname
(lambda (stx)
(raise-syntax-error
'type-check
"type name used out of context"
stx
(and (stx-pair? stx) (stx-car stx))))))
(ignore #'(define-syntax tname stx-err-fun))
#'(begin))
#,(internal (syntax/loc stx (define-type-alias-internal tname rest))))]
#,(internal (syntax/loc stx
(define-type-alias-internal tname rest
rest.args))))]
[(_ (tname:id args:id ...) rest)
(syntax/loc stx (define-type-alias tname (All (args ...) rest)))]))

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

@ -78,7 +78,12 @@
`(->acc (list ,@(map sub dom)) ,(sub t) ,(sub pth))]
[(Union: elems) (split-union elems)]
[(Base: n cnt pred _) (int-err "Base type not in predefined-type-table" n)]
[(Name: stx) `(make-Name (quote-syntax ,stx))]
[(Name: stx deps args struct?)
`(make-Name (quote-syntax ,stx)
(list ,@(map (λ (x) `(quote-syntax ,x)) deps))
,(and args
`(list ,@(map (λ (x) `(quote-syntax ,x)) args)))
,struct?)]
[(fld: t acc mut) `(make-fld ,(sub t) (quote-syntax ,acc) ,mut)]
[(Struct: name parent flds proc poly? pred-id)
`(make-Struct (quote-syntax ,name) ,(sub parent)

326
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/type-alias-helper.rkt vendored Normal file
View File

@ -0,0 +1,326 @@
#lang racket/base
;; This module provides helper functions for type aliases
(require "../utils/utils.rkt"
(utils tc-utils)
(env type-alias-env type-name-env)
(rep type-rep)
(private parse-type)
(typecheck internal-forms)
(types resolve base-abbrev)
data/queue
racket/dict
racket/format
racket/list
racket/match
syntax/id-table
syntax/kerncase
(for-template
(typecheck internal-forms)
racket/base))
(provide find-strongly-connected-type-aliases
check-type-alias-contractive
get-type-alias-info
register-all-type-aliases
parse-type-alias)
;; A Vertex is a
;; (vertex Identifier Boolean Option<Integer> Option<Integer> Listof<Id>)
;;
;; interp. a vertex in a graph, we only use this for Tarjan's algorithm
;; id - identifier (labels vertices)
;; stack? - whether this vertex is on the stack (for speed)
;; index - index tracked in Tarjan's algorithm
;; lowlink - see index
;; adjacent - list of adjacent vertices
(struct vertex (id [stack? #:mutable] [index #:mutable]
[lowlink #:mutable] adjacent)
#:transparent)
;; Dict<Id, (List Type Listof<Id>)> -> Listof<Listof<Id>>
;; Find strongly connected type aliases in order to
;; find mutually recursive aliases
;;
;; Returns the components in topologically sorted order
(define (find-strongly-connected-type-aliases dep-map)
(define vertex-map (make-free-id-table))
(for ([(id adjacent) (in-dict dep-map)])
(free-id-table-set! vertex-map id (vertex id #f #f #f adjacent)))
;; Implements Tarjan's algorithm. See Wikipedia
;; http://en.wikipedia.org/wiki/Tarjan's_strongly_connected_components_algorithm
(define (tarjan vertices)
(define (strongly-connected vtx)
(set-vertex-index! vtx index)
(set-vertex-lowlink! vtx index)
(set! index (add1 index))
(enqueue-front! stack vtx)
(set-vertex-stack?! vtx #t)
(for ([successor-id (in-list (vertex-adjacent vtx))])
(define successor (free-id-table-ref vertices successor-id))
(cond [(not (vertex-index successor))
(strongly-connected successor)
(set-vertex-lowlink! vtx
(min (vertex-lowlink vtx)
(vertex-lowlink successor)))]
[(vertex-stack? successor)
(set-vertex-lowlink! vtx
(min (vertex-lowlink vtx)
(vertex-index successor)))]))
;; sets a result component if this was a root vertex
(when (= (vertex-lowlink vtx) (vertex-index vtx))
(define new-scc
(for/list ([elem (in-queue stack)]
#:final (equal? vtx elem))
(dequeue! stack)
(set-vertex-stack?! elem #f)
(vertex-id elem)))
(set! sccs (cons new-scc sccs))))
;; the body
(define index 0)
(define stack (make-queue))
(define sccs '())
(for ([(id vtx) (in-dict vertices)]
#:unless (vertex-index vtx))
(strongly-connected vtx))
sccs)
(tarjan vertex-map))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Data definitions for aliases
;;
;; A TypeAliasInfo is a (list Syntax (Listof Identifier))
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; check-type-alias-contractive : Id Type -> Void
;;
;; This function checks if the given type alias is
;; "contractive" or "productive"
;; i.e., that you can unfold a good type like μx.int->x to
;; μx.int->int->int->...x but a type like
;; μx.x only unfolds to itself
;;
(define (check-type-alias-contractive id type)
(define/match (check type)
[((Union: elems)) (andmap check elems)]
[((Name: name-id _ _ _))
(and (not (free-identifier=? name-id id))
(check (resolve-once type)))]
[((App: rator rands stx))
(and (check rator) (check rands))]
[((Mu: _ body)) (check body)]
[((Poly: names body)) (check body)]
[((PolyDots: names body)) (check body)]
[(_) #t])
(unless (check type)
(tc-error/stx
id
"Recursive types are not allowed directly inside their definition")))
;; get-type-alias-info : Listof<Syntax> -> Listof<Id> Dict<Id, TypeAliasInfo>
;;
;; Given the syntaxes representing type alias definitions, return
;; the information needed to register them later
(define (get-type-alias-info type-aliases)
(for/lists (_1 _2) ([type-alias (in-list type-aliases)])
(define-values (id type-stx args) (parse-type-alias type-alias))
;; Register type alias names with a dummy value so that it's in
;; scope for the registration later.
;;
;; The `(make-Value (gensym))` expression is used to make sure
;; that unions don't collapse the aliases too soon.
(register-resolved-type-alias id Err)
(register-type-name
id
(if args
(make-Poly (map syntax-e args) (make-Value (gensym)))
(make-Value (gensym))))
(values id (list id type-stx args))))
;; register-all-type-aliases : Listof<Id> Dict<Id, TypeAliasInfo> -> Void
;;
;; Given parsed type aliases and a type alias map, do the work
;; of actually registering the type aliases. If struct names or
;; other definitions need to be registered, do that before calling
;; this function.
(define (register-all-type-aliases type-alias-names type-alias-map)
;; Disable resolve caching for the extent of this setup.
;; Makes sure Name types don't get cached too soon.
(parameterize ([current-cache-resolve? #f])
;; Find type alias dependencies
;; The two maps defined here contains the dependency structure
;; of type aliases in two senses:
;; (1) other type aliases referenced in a type alias
;; (2) other type aliases referenced by some class in a
;; type alias in a #:implements clause
;;
;; The second is necessary in order to prevent recursive
;; #:implements clauses and to determine the order in which
;; recursive type aliases should be initialized.
(define-values (type-alias-dependency-map type-alias-class-map)
(for/lists (_1 _2)
([(name alias-info) (in-dict type-alias-map)])
(define links-box (box null))
(define class-box (box null))
(define type
(parameterize ([current-type-alias-name name]
[current-referenced-aliases links-box]
[current-referenced-class-parents class-box])
(parse-type (car alias-info))))
(define pre-dependencies
(remove-duplicates (unbox links-box) free-identifier=?))
(define (filter-by-type-alias-names names)
(for/list ([id (in-list names)]
#:when (memf (λ (id2) (free-identifier=? id id2))
type-alias-names))
id))
(define alias-dependencies
(filter-by-type-alias-names pre-dependencies))
(define class-dependencies
(filter-by-type-alias-names (unbox class-box)))
(values (cons name alias-dependencies)
(cons name class-dependencies))))
(define components
(find-strongly-connected-type-aliases type-alias-dependency-map))
(define class-components
(find-strongly-connected-type-aliases type-alias-class-map))
;; helper function for defining singletons
(define (has-self-cycle? component [map type-alias-dependency-map])
(define id (car component))
(memf (λ (id2) (free-identifier=? id id2))
(dict-ref map id)))
;; A singleton component can be either a self-cycle or a node that
;; that does not participate in cycles, so we disambiguate
(define-values (acyclic-singletons recursive-aliases)
(for/fold ([singletons '()] [other '()])
([component (in-list components)])
(if (and (= (length component) 1)
(not (has-self-cycle? component)))
(values (cons (car component) singletons) other)
(values singletons (append component other)))))
;; Check that no #:implements clauses are recursive
(define counterexample
(for/or ([component class-components])
(and (or (not (= (length component) 1))
(has-self-cycle? component type-alias-class-map))
component)))
(when counterexample
(tc-error/stx
(car counterexample)
"Recursive #:implements clause not allowed"))
;; Split recursive aliases into those involving classes
;; (in reverse topological order) and the rest of the aliases
(define class-aliases
(for/list ([component (in-list (reverse class-components))]
#:when (member (car component)
recursive-aliases
free-identifier=?))
(car component)))
(define other-recursive-aliases
(for/list ([alias (in-list recursive-aliases)]
#:unless (member alias
class-aliases
free-identifier=?))
alias))
;; Reconstruct type alias dependency map based on class parent
;; information. This ensures that the `deps` field is precise
;; in all type aliases involving class types
(define (get-all-parent-deps id)
(define (get-deps parent)
(cdr (assoc parent type-alias-dependency-map free-identifier=?)))
(define parents (cdr (assoc id type-alias-class-map free-identifier=?)))
(cond [(null? parents) null]
[else
(define all-deps
(for/list ([parent parents])
(append (get-deps parent)
(get-all-parent-deps parent))))
(apply append all-deps)]))
(define new-dependency-map/classes
(for/list ([(id deps) (in-dict type-alias-dependency-map)])
(cond [(dict-has-key? type-alias-class-map id)
(define new-deps
(remove-duplicates (append (get-all-parent-deps id) deps)
free-identifier=?))
(cons id new-deps)]
[else (cons id deps)])))
;; Do another pass on dependency map, using the connected
;; components analysis data to determine which dependencies are
;; actually needed for mutual recursion. Drop all others.
(define new-dependency-map
(for/list ([(id deps) (in-dict new-dependency-map/classes)])
;; find the component this `id` participated in so
;; that we can drop `deps` that aren't in that component
(define component
(findf (λ (component) (member id component free-identifier=?))
components))
(define new-deps
(filter (λ (dep) (member dep component free-identifier=?)) deps))
(cons id new-deps)))
;; Actually register recursive type aliases
(for ([id (in-list recursive-aliases)])
(define record (dict-ref type-alias-map id))
(match-define (list _ args) record)
(define deps (dict-ref new-dependency-map id))
(register-resolved-type-alias id (make-Name id deps args #f)))
;; Register non-recursive type aliases
;;
;; Note that the connected component algorithm returns results
;; in topologically sorted order, so we want to go through in the
;; reverse order of that to avoid unbound type aliases.
(for ([id (in-list acyclic-singletons)])
(define type-stx (car (dict-ref type-alias-map id)))
(register-resolved-type-alias id (parse-type type-stx)))
;; Finish registering recursive aliases
;; names-to-refine : Listof<Id>
;; types-to-refine : Listof<Type>
;; tvarss : Listof<Listof<Symbol>>
(define-values (names-to-refine types-to-refine tvarss)
(for/lists (_1 _2 _3)
([id (in-list (append other-recursive-aliases class-aliases))])
(define record (dict-ref type-alias-map id))
(match-define (list type-stx args) record)
(define type
;; make sure to reject the type if it uses polymorphic
;; recursion (see resolve.rkt)
(parameterize ([current-check-polymorphic-recursion args])
(parse-type type-stx)))
(register-type-name id type)
(add-constant-variance! id args)
(check-type-alias-contractive id type)
(values id type args)))
;; Finally, do a last pass to refine the variance
(refine-variance! names-to-refine types-to-refine tvarss)))
;; Syntax -> Syntax Syntax Syntax Option<Integer>
;; Parse a type alias internal declaration
(define (parse-type-alias form)
(kernel-syntax-case* form #f
(define-type-alias-internal values)
[(define-values ()
(begin (quote-syntax (define-type-alias-internal nm ty args))
(#%plain-app values)))
(values #'nm #'ty (syntax-e #'args))]
;; this version is for `let`-like bodies
[(begin (quote-syntax (define-type-alias-internal nm ty args))
(#%plain-app values))
(values #'nm #'ty (syntax-e #'args))]
[_ (int-err "not define-type-alias")]))

39
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/type-name-env.rkt vendored
View File

@ -7,7 +7,7 @@
(require syntax/id-table
(env type-alias-env)
(utils tc-utils)
(rep type-rep)
(rep type-rep free-variance)
(types utils))
(provide register-type-name
@ -18,7 +18,9 @@
register-type-variance!
lookup-type-variance
type-variance-env-map)
type-variance-env-map
add-constant-variance!
refine-variance!)
;; a mapping from id -> type (where id is the name of the type)
(define the-mapping
@ -50,7 +52,9 @@
(define (add-alias from to)
(when (lookup-type-name to (lambda () #f))
(register-resolved-type-alias from (make-Name to))))
(register-resolved-type-alias
from
(make-Name to null #f #t))))
;; a mapping from id -> listof[Variance] (where id is the name of the type)
@ -62,13 +66,38 @@
(define (register-type-variance! id variance)
(free-id-table-set! variance-mapping id variance))
(define (lookup-type-variance id )
(free-id-table-ref variance-mapping id))
(define (lookup-type-variance id)
(free-id-table-ref
variance-mapping id
(lambda () (lookup-variance-fail id))))
;; map over the-mapping, producing a list
;; (id variance -> T) -> listof[T]
(define (type-variance-env-map f)
(free-id-table-map variance-mapping f))
;; Listof<Type> Listof<Option<Listof<Type-Var>>> -> Void
;; Refines the variance of a type in the name environment
(define (refine-variance! names types tvarss)
(let loop ()
(define sames?
(for/and ([name (in-list names)]
[type (in-list types)]
[tvars (in-list tvarss)])
(cond
[(or (not tvars) (null? tvars)) #t]
[else
(define free-vars (free-vars-hash (free-vars* type)))
(define variance (map (λ (v) (hash-ref free-vars v Constant)) tvars))
(define old-variance (lookup-type-variance name))
(register-type-variance! name variance)
(equal? variance old-variance)])))
(unless sames? (loop))))
;; Id Option<Listof<Type-Var>> -> Void
;; Initialize variance of the given id to Constant for all type vars
(define (add-constant-variance! name vars)
(unless (or (not vars) (null? vars))
(register-type-variance! name (map (lambda (_) Constant) vars))))

8
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
View File

@ -450,6 +450,12 @@
;; constrain v to be above S (but don't mention V)
(singleton (var-promote S V) v Univ)]
;; recursive names should get resolved as they're seen
[(s (? Name? t))
(cg s (resolve-once t))]
[((? Name? s) t)
(cg (resolve-once s) t)]
;; constrain b1 to be below T, but don't mention the new vars
[((Poly: v1 b1) T) (cgen (append v1 V) X Y b1 T)]
@ -477,7 +483,7 @@
(cset-meet proc-c (cgen/flds V X Y flds flds*)))]
;; two struct names, need to resolve b/c one could be a parent
[((Name: n) (Name: n*))
[((Name: n _ _ #t) (Name: n* _ _ #t))
(if (free-identifier=? n n*)
null
(let ((rn (resolve-once S)) (rn* (resolve-once T)))

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

@ -37,7 +37,32 @@
[parse-tc-results/id (syntax? c:any/c . c:-> . tc-results/c)]
[parse-literal-alls (syntax? . c:-> . (c:listof (c:or/c (c:listof identifier?) (c:list/c (c:listof identifier?) identifier?))))])
(provide star ddd/bound)
(provide star ddd/bound
current-referenced-aliases
current-referenced-class-parents
current-type-alias-name)
;; current-type-alias-name : Parameter<(Option Id)>
;; This parameter stores the name of the type alias that is
;; being parsed (set in type-alias-helper.rkt), #f if the
;; parsing is not for a type alias
(define current-type-alias-name (make-parameter #f))
;; current-referenced-aliases : Parameter<Option<Box<List<Id>>>>
;; This parameter is used to coordinate with the type-checker to determine
;; if a type alias should be recursive or not
;;
;; interp. the argument is #f if not checking for type aliases.
;; Otherwise, it should be a box containing a list of
;; identifiers (i.e., type aliases in the syntax)
(define current-referenced-aliases (make-parameter #f))
;; current-referenced-class-parents : Parameter<Option<Box<List<Id>>>>
;; This parameter is used to coordinate with the type-checker about
;; the dependency structure of class types using #:implements
;;
;; interp. same as above
(define current-referenced-class-parents (make-parameter #f))
(define-literal-syntax-class #:for-label car)
(define-literal-syntax-class #:for-label cdr)
@ -450,13 +475,11 @@
=>
(lambda (t)
;(printf "found a type alias ~a\n" #'id)
(when (current-referenced-aliases)
(define alias-box (current-referenced-aliases))
(set-box! alias-box (cons #'id (unbox alias-box))))
(add-disappeared-use (syntax-local-introduce #'id))
t)]
;; if it's a type name, we just use the name
[(lookup-type-name #'id (lambda () #f))
(add-disappeared-use (syntax-local-introduce #'id))
;(printf "found a type name ~a\n" #'id)
(make-Name #'id)]
[(free-identifier=? #'id #'->)
(tc-error/delayed "Incorrect use of -> type constructor")
Err]
@ -481,7 +504,7 @@
[args (parse-types #'(arg args ...))])
(resolve-app-check-error rator args stx)
(match rator
[(Name: _) (make-App rator args stx)]
[(Name: _ _ _ _) (make-App rator args stx)]
[(Poly: _ _) (instantiate-poly rator args)]
[(Mu: _ _) (loop (unfold rator) args)]
[(Error:) Err]
@ -560,10 +583,10 @@
;;; Utilities for (Class ...) type parsing
;; process-class-clauses : Option<F> Syntax FieldDict MethodDict AugmentDict
;; process-class-clauses : Option<F> Type Stx FieldDict MethodDict AugmentDict
;; -> Option<Id> FieldDict MethodDict AugmentDict
;; Merges #:implements class type and the current class clauses appropriately
(define (merge-with-parent-type row-var stx fields methods augments)
(define (merge-with-parent-type row-var parent-type parent-stx fields methods augments)
;; (Listof Symbol) Dict Dict String -> (Values Dict Dict)
;; check for duplicates in a class clause
(define (check-duplicate-clause names super-names types super-types err-msg)
@ -583,18 +606,16 @@
types (dict-remove super-types maybe-dup)
err-msg)]
[else
(tc-error/stx stx err-msg maybe-dup)])]
(tc-error/stx parent-stx err-msg maybe-dup)])]
[else (values types super-types)]))
(define parent-type (parse-type stx))
(define (match-parent-type parent-type)
(match parent-type
(define resolved (resolve parent-type))
(match resolved
[(Class: row-var _ fields methods augments _)
(values row-var fields methods augments)]
[(? Mu?)
(match-parent-type (unfold parent-type))]
[_ (tc-error "expected a class type for #:implements clause, got ~a"
parent-type)]))
resolved)]))
(define-values (super-row-var super-fields
super-methods super-augments)
(match-parent-type parent-type))
@ -670,8 +691,8 @@
(syntax-parse stx
[(kw (~var clause (class-type-clauses parse-type)))
(add-disappeared-use #'kw)
(define parent-types (stx->list #'clause.extends-types))
(define parent-stxs (stx->list #'clause.extends-types))
(define parent-types (map parse-type parent-stxs))
(define given-inits (attribute clause.inits))
(define given-fields (attribute clause.fields))
(define given-methods (attribute clause.methods))
@ -683,31 +704,68 @@
(and (attribute clause.init-rest)
(parse-type (attribute clause.init-rest))))
(check-function-types given-methods)
(check-function-types given-augments)
;; Only proceed to create a class type when the parsing
;; process isn't looking for recursive type alias references.
;; (otherwise the merging process will error)
(cond [(or (null? parent-stxs)
(not (current-referenced-aliases)))
;; merge with all given parent types, erroring if needed
(define-values (row-var fields methods augments)
(for/fold ([row-var given-row-var]
[fields given-fields]
[methods given-methods]
[augments given-augments])
([parent-type parent-types])
(merge-with-parent-type row-var parent-type fields
methods augments)))
(check-function-types given-methods)
(check-function-types given-augments)
;; check constraints on row var for consistency with class
(when (and row-var (has-row-constraints? (F-n row-var)))
(define constraints (lookup-row-constraints (F-n row-var)))
(check-constraints given-inits (car constraints))
(check-constraints fields (cadr constraints))
(check-constraints methods (caddr constraints))
(check-constraints augments (cadddr constraints)))
;; merge with all given parent types, erroring if needed
(define-values (row-var fields methods augments)
(for/fold ([row-var given-row-var]
[fields given-fields]
[methods given-methods]
[augments given-augments])
([parent-type parent-types]
[parent-stx parent-stxs])
(merge-with-parent-type row-var parent-type parent-stx
fields methods augments)))
(define class-type
(make-Class row-var given-inits fields methods augments given-init-rest))
;; check constraints on row var for consistency with class
(when (and row-var (has-row-constraints? (F-n row-var)))
(define constraints (lookup-row-constraints (F-n row-var)))
(check-constraints given-inits (car constraints))
(check-constraints fields (cadr constraints))
(check-constraints methods (caddr constraints))
(check-constraints augments (cadddr constraints)))
class-type]))
(define class-type
(make-Class row-var given-inits fields methods augments given-init-rest))
class-type]
[else
;; Conservatively assume that if there *are* #:implements
;; clauses, then the current type alias will be recursive
;; through one of the type aliases in the #:implements clauses.
;;
;; This is needed because it's hard to determine if a type
;; in the #:implements clauses depends on the current
;; type alias at this point. Otherwise, we would have to
;; parse all type aliases again.
;;
;; An example type that is a problem without this assumption is
;; alias = (Class #:implements Foo%) where Foo%
;; has a class clause referring to alias
;; since "alias" will be a non-recursive alias
;;
;; Without the approximation, we may miss recursive references
;; which can cause infinite looping elsewhere in TR.
;;
;; With the approximation, we have spurious recursive references
;; which may cause more indirection through the Name environment
;; or generate worse contracts.
(define alias-box (current-referenced-aliases))
(set-box! alias-box (cons (current-type-alias-name)
(unbox alias-box)))
(define class-box (current-referenced-class-parents))
(set-box! class-box (append parent-stxs (unbox class-box)))
;; Ok to return Error here, since this type will
;; get reparsed in another pass
(make-Error)
])]))
;; check-function-types : Dict<Name, Type> -> Void
;; ensure all types recorded in the dictionary are function types

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

@ -7,7 +7,7 @@
syntax/parse
(rep type-rep filter-rep object-rep)
(utils tc-utils)
(env type-name-env)
(env type-name-env type-alias-env)
(rep rep-utils)
(types resolve union utils kw-types)
(prefix-in t: (types abbrev numeric-tower))
@ -194,7 +194,94 @@
(define (t->sc/method t) (t->sc/function t fail typed-side recursive-values loop #t))
(define (t->sc/fun t) (t->sc/function t fail typed-side recursive-values loop #f))
(match type
[(or (App: _ _ _) (Name: _)) (t->sc (resolve-once type))]
;; Applications of implicit recursive type aliases
;;
;; We special case this rather than just resorting to standard
;; App resolution (see case below) because the resolution process
;; will make type->static-contract infinite loop.
[(App: (Name: name _ _ #f) rands _)
;; Key with (cons name 'app) instead of just name because the
;; application of the Name is not necessarily the same as the
;; Name type alone
(cond [(hash-ref recursive-values (cons name 'app) #f)]
[else
(define name* (generate-temporary name))
(recursive-sc (list name*)
(list
(t->sc (resolve-once type)
#:recursive-values
(hash-set recursive-values
(cons name 'app)
(recursive-sc-use name*))))
(recursive-sc-use name*))])]
;; Implicit recursive aliases
[(Name: name-id dep-ids args #f)
;; FIXME: this may not be correct for different aliases that have
;; the same name that are somehow used together, if that's
;; possible
(define name (syntax-e name-id))
(define deps (map syntax-e dep-ids))
(cond [;; recursive references are looked up, see F case
(hash-ref recursive-values name #f) =>
(λ (rv) (triple-lookup rv typed-side))]
[else
;; see Mu case, which uses similar machinery
(match-define (and n*s (list untyped-n* typed-n* both-n*))
(generate-temporaries (list name name name)))
(define-values (untyped-deps typed-deps both-deps)
(values (generate-temporaries deps)
(generate-temporaries deps)
(generate-temporaries deps)))
;; Set recursive references for the `name` itself
(define *rv
(hash-set recursive-values name
(triple (recursive-sc-use untyped-n*)
(recursive-sc-use typed-n*)
(recursive-sc-use both-n*))))
;; Add in references for the dependency aliases
(define rv
(for/fold ([rv *rv])
([dep (in-list deps)]
[untyped-dep (in-list untyped-deps)]
[typed-dep (in-list typed-deps)]
[both-dep (in-list both-deps)])
(hash-set rv dep
(triple (recursive-sc-use untyped-dep)
(recursive-sc-use typed-dep)
(recursive-sc-use both-dep)))))
(define resolved-name (resolve-once type))
(define resolved-deps
(map (λ (dep) (lookup-type-alias dep values)) dep-ids))
;; resolved-deps->scs : (U 'untyped 'typed 'both)
;; -> (Listof Static-Contract)
(define (resolved-deps->scs typed-side)
(for/list ([resolved-dep resolved-deps])
(loop resolved-dep typed-side rv)))
;; Now actually generate the static contracts
(case typed-side
[(both) (recursive-sc
(append (list both-n*) both-deps)
(cons (loop resolved-name 'both rv)
(resolved-deps->scs 'both))
(recursive-sc-use both-n*))]
[(typed untyped)
(define untyped (loop resolved-name 'untyped rv))
(define typed (loop resolved-name 'typed rv))
(define both (loop resolved-name 'both rv))
(define-values (untyped-dep-scs typed-dep-scs both-dep-scs)
(values
(resolved-deps->scs 'untyped)
(resolved-deps->scs 'typed)
(resolved-deps->scs 'both)))
(recursive-sc
(append n*s untyped-deps typed-deps both-deps)
(append (list untyped typed both)
untyped-dep-scs typed-dep-scs both-dep-scs)
(recursive-sc-use (if (from-typed? typed-side) typed-n* untyped-n*)))])])]
;; Ordinary type applications or struct type names, just resolve
[(or (App: _ _ _) (Name: _ _ _ #t)) (t->sc (resolve-once type))]
[(Univ:) (if (from-typed? typed-side) any-wrap/sc any/sc)]
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
(listof/sc (t->sc elem-ty))]

20
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt
View File

@ -111,10 +111,20 @@
(def-type F ([n symbol?]) [#:frees (single-free-var n) empty-free-vars]
[#:fold-rhs #:base])
;; id is an Identifier
;; This will always resolve to a struct
(def-type Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f]
[#:fold-rhs #:base])
;; Name, an indirection of a type through the environment
;;
;; interp.
;; A type name, potentially recursive or mutually recursive or pointing
;; to a type for a struct type
;; id is the name stored in the environment
;; deps are the other aliases this depends on, if any
;; args are the type parameters for this type (or #f if none)
;; struct? indicates if this maps to a struct type
(def-type Name ([id identifier?]
[deps (listof identifier?)]
[args (or/c #f (listof identifier?))]
[struct? boolean?])
[#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
;; rator is a type
;; rands is a list of types
@ -123,7 +133,7 @@
[#:intern (cons (Rep-seq rator) (map Rep-seq rands))]
[#:frees (λ (f)
(match rator
((Name: n)
((Name: n _ _ _)
(instantiate-frees n (map f rands)))
(else (f (resolve-app rator rands stx)))))]

23
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
View File

@ -324,17 +324,20 @@
(define-values (super-row super-inits super-fields
super-methods super-augments super-init-rest)
(match super-type
[(tc-result1: (Class: super-row super-inits super-fields
super-methods super-augments super-init-rest))
(values super-row super-inits super-fields
super-methods super-augments super-init-rest)]
[(tc-result1: t)
(tc-error/expr/fields "type mismatch"
#:more "superclass expression should produce a class"
#:stx (hash-ref parse-info 'superclass-expr)
"expected" "a class"
"given" t)
(values #f null null null null #f)]))
(match (resolve t)
[(Class: super-row super-inits super-fields
super-methods super-augments super-init-rest)
(values super-row super-inits super-fields
super-methods super-augments super-init-rest)]
[t
(tc-error/expr/fields "type mismatch"
#:more "superclass expression should produce a class"
#:stx (hash-ref parse-info 'superclass-expr)
"expected" "a class"
"given" t)
(values #f null null null null #f)])]
[_ (int-err "Unhandled result")]))
(define super-init-names (dict-keys super-inits))
(define super-field-names (dict-keys super-fields))
(define super-method-names (dict-keys super-methods))

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt
View File

@ -99,7 +99,7 @@
(define-internal-classes
[type-alias
(define-type-alias-internal name type)]
(define-type-alias-internal name type args)]
[type-refinement
(declare-refinement-internal predicate)]
[typed-struct

5
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
View File

@ -143,10 +143,11 @@
;; row var wasn't in the same position in some cases
(fail))
(define idx (car row-var-idxs))
(cond [(Class? (list-ref argtys-t idx))
(define resolved-argty (resolve (list-ref argtys-t idx)))
(cond [(Class? resolved-argty)
(define substitution
(hash row-var
(t-subst (infer-row constraints (list-ref argtys-t idx)))))
(t-subst (infer-row constraints resolved-argty))))
(tc/funapp f-stx args-stx (ret (subst-all substitution f-ty))
argtys expected)]
[else (fail)])]

29
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
View File

@ -4,7 +4,8 @@
(except-in (types utils abbrev union filter-ops) -> ->* one-of/c)
(only-in (types abbrev) (-> t:->))
(private type-annotation parse-type syntax-properties)
(env lexical-env type-alias-env global-env type-env-structs scoped-tvar-env)
(env lexical-env type-alias-env type-alias-helper
global-env type-env-structs scoped-tvar-env)
(rep type-rep filter-rep)
syntax/free-vars
(typecheck signatures tc-metafunctions tc-subst internal-forms)
@ -101,14 +102,24 @@
[clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
;; Collect the declarations, which are represented as expression.
;; We put them back into definitions to reuse the existing machinery
(for ([body (in-list exprs)])
(syntax-parse #`(define-values () #,body)
[t:type-alias
(register-resolved-type-alias #'t.name (parse-type #'t.type))]
[t:type-declaration
(register-type-if-undefined #'t.id (parse-type #'t.type))
(register-scoped-tvars #'t.id (parse-literal-alls #'t.type))]
[_ (void)]))
(define-values (type-aliases declarations)
(for/fold ([aliases '()] [declarations '()])
([body (in-list exprs)])
(syntax-parse #`(define-values () #,body)
[t:type-alias
(values (cons #'t aliases) declarations)]
[t:type-declaration
(values aliases (cons (list #'t.id #'t.type) declarations))]
[_ (values aliases declarations)])))
(define-values (alias-names alias-map) (get-type-alias-info type-aliases))
(register-all-type-aliases alias-names alias-map)
(for ([declaration declarations])
(match-define (list id type) declaration)
(register-type-if-undefined id (parse-type type))
(register-scoped-tvars id (parse-literal-alls type)))
;; add scoped type variables, before we get to typechecking
;; FIXME: can this pass be fused with the one immediately above?
(for ([n (in-list names)] [b (in-list exprs)])

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

@ -4,7 +4,7 @@
(require "../utils/utils.rkt"
racket/match syntax/stx
(typecheck signatures tc-funapp)
(types base-abbrev utils type-table)
(types base-abbrev resolve utils type-table)
(rep type-rep)
(utils tc-utils))
@ -14,8 +14,8 @@
(define (tc/send form rcvr method args [expected #f])
(define (do-check rcvr-type)
(match rcvr-type
[(tc-result1: (Instance: (? Mu? type)))
(do-check (ret (make-Instance (unfold type))))]
[(tc-result1: (Instance: (? needs-resolving? type)))
(do-check (ret (make-Instance (resolve type))))]
[(tc-result1: (Instance: (and c (Class: _ _ _ methods _ _))))
(match (tc-expr method)
[(tc-result1: (Value: (? symbol? s)))

40
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
View File

@ -8,7 +8,7 @@
(rep type-rep object-rep free-variance)
(private parse-type syntax-properties)
(types abbrev utils resolve substitute type-table struct-table)
(env global-env type-name-env tvar-env)
(env global-env type-name-env type-alias-env tvar-env)
(utils tc-utils)
(typecheck def-binding internal-forms)
(for-syntax syntax/parse racket/base))
@ -120,7 +120,13 @@
(define/cond-contract (register-sty! sty names desc)
(c:-> Struct? struct-names? struct-desc? void?)
(register-type-name (struct-names-type-name names)
;; a type alias needs to be registered here too, to ensure
;; that parse-type will map the identifier to this Name type
(define type-name (struct-names-type-name names))
(register-resolved-type-alias
type-name
(make-Name type-name null #f #t))
(register-type-name type-name
(make-Poly (struct-desc-tvars desc) sty)))
@ -139,10 +145,13 @@
;; the base-type, with free type variables
(define name-type
(make-Name (struct-names-type-name names)
null #f #t))
(define poly-base
(if (null? tvars)
(make-Name (struct-names-type-name names))
(make-App (make-Name (struct-names-type-name names)) (map make-F tvars) #f)))
name-type
(make-App name-type (map make-F tvars) #f)))
;; is this structure covariant in *all* arguments?
(define covariant?
@ -210,25 +219,13 @@
null
(register-struct-bindings! sty names desc si)))))
;; Listof<Parsed-Struct> -> Void
;; Refines the variance of struct types in the name environment
(define (refine-struct-variance! parsed-structs)
(define stys (map parsed-struct-sty parsed-structs))
(define tvarss (map (compose struct-desc-tvars parsed-struct-desc) parsed-structs))
(let loop ()
(define sames
(for/list ((sty (in-list stys)) (tvars (in-list tvarss)))
(cond
((null? tvars) #t)
(else
(define name (Struct-name sty))
(define free-vars (free-vars-hash (free-vars* sty)))
(define variance (map (λ (v) (hash-ref free-vars v Constant)) tvars))
(define old-variance (lookup-type-variance name))
(register-type-variance! name variance)
(equal? variance old-variance)))))
(unless (andmap values sames)
(loop))))
(define names (map Struct-name stys))
(refine-variance! names stys tvarss))
;; check and register types for a define struct
;; tc/struct : Listof[identifier] (U identifier (list identifier identifier))
@ -285,7 +282,8 @@
(c:-> identifier? (c:or/c #f identifier?) (c:listof identifier?)
(c:listof Type/c) (c:or/c #f identifier?)
c:any/c)
(define parent-type (and parent (resolve-name (make-Name parent))))
(define parent-type
(and parent (resolve-name (make-Name parent null #f #t))))
(define parent-tys (map fld-t (get-flds parent-type)))
(define names (get-struct-names nm fld-names #f))

31
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
View File

@ -8,7 +8,8 @@
(types utils abbrev type-table struct-table)
(private parse-type type-annotation type-contract syntax-properties)
(env global-env init-envs type-name-env type-alias-env
lexical-env env-req mvar-env scoped-tvar-env)
lexical-env env-req mvar-env scoped-tvar-env
type-alias-helper)
(utils tc-utils)
(typecheck provide-handling def-binding tc-structs
typechecker internal-forms)
@ -41,13 +42,6 @@
[t:typed-struct (attribute t.tvars)]
[t:typed-struct/exec null]))
(define (add-constant-variance! name vars)
(unless (null? vars)
(register-type-variance! name (map (lambda (_) Constant) vars))))
;; syntax? -> (listof def-binding?)
(define (tc-toplevel/pass1 form)
(parameterize ([current-orig-stx form])
@ -249,10 +243,6 @@
[(define-syntaxes (nm ...) . rest) (syntax->list #'(nm ...))]
[_ #f]))
(define (parse-type-alias form)
(syntax-parse form
[t:type-alias (values #'t.name #'t.type)]))
;; actually do the work on a module
;; produces prelude and post-lude syntax objects
;; syntax-list -> (values syntax syntax)
@ -269,16 +259,23 @@
define/fixup-contract?))
(do-time "Form splitting done")
;(printf "before parsing type aliases~n")
(for-each (compose register-type-alias parse-type-alias) type-aliases)
(define-values (type-alias-names type-alias-map)
(get-type-alias-info type-aliases))
;; Add the struct names to the type table, but not with a type
;(printf "before adding type names~n")
(let ((names (map name-of-struct struct-defs))
(type-vars (map type-vars-of-struct struct-defs)))
(for ([name names])
(register-resolved-type-alias
name (make-Name name null #f #t)))
(for-each register-type-name names)
(for-each add-constant-variance! names type-vars))
;(printf "after adding type names~n")
;; resolve all the type aliases, and error if there are cycles
(resolve-type-aliases parse-type)
(register-all-type-aliases type-alias-names type-alias-map)
;; Parse and register the structure types
(define parsed-structs
(for/list ((def (in-list struct-defs)))
@ -405,7 +402,9 @@
[_
;; Handle type aliases
(when (type-alias? form)
((compose register-type-alias parse-type-alias) form))
(define-values (alias-names alias-map)
(get-type-alias-info (list form)))
(register-all-type-aliases alias-names alias-map))
;; Handle struct definitions
(when (typed-struct? form)
(define name (name-of-struct form))

5
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
View File

@ -13,7 +13,8 @@
"types/kw-types.rkt"
"types/utils.rkt"
"utils/utils.rkt"
"utils/tc-utils.rkt")
"utils/tc-utils.rkt"
"env/type-name-env.rkt")
(for-syntax racket/base syntax/parse))
;; printer-type: (one-of/c 'custom 'debug)
@ -386,7 +387,7 @@
[(? Rep-stx a) (syntax->datum (Rep-stx a))]
[(Univ:) 'Any]
;; names are just the printed as the original syntax
[(Name: stx) (syntax-e stx)]
[(Name: id _ _ _) (syntax-e id)]
;; If a type has a name, then print it with that name.
;; However, we expand the alias in some cases
;; (i.e., the fuel is > 0) for the :type form.

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

@ -35,12 +35,12 @@
[(list _ (F: _)) #t]
[(list (Opaque: _) _) #t]
[(list _ (Opaque: _)) #t]
[(list (Name: n) (Name: n*))
[(list (Name: n _ _ _) (Name: n* _ _ _))
(or (free-identifier=? n n*)
(overlap (resolve-once t1) (resolve-once t2)))]
[(list _ (Name: _))
[(list _ (Name: _ _ _ _))
(overlap t1 (resolve-once t2))]
[(list (Name: _) _)
[(list (Name: _ _ _ _) _)
(overlap (resolve-once t1) t2)]
[(list (? Mu?) _) (overlap (unfold t1) t2)]
[(list _ (? Mu?)) (overlap t1 (unfold t2))]
@ -118,7 +118,7 @@
(if (subtype old rem)
(Un) ;; the empty type
(match (list old rem)
[(list (or (App: _ _ _) (Name: _)) t)
[(list (or (App: _ _ _) (Name: _ _ _ _)) t)
;; must be different, since they're not subtypes
;; and n must refer to a distinct struct type
old]

79
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/resolve.rkt
View File

@ -10,15 +10,34 @@
racket/format)
(provide resolve-name resolve-app needs-resolving?
resolve resolve-app-check-error)
resolve resolve-app-check-error
current-cache-resolve?
current-check-polymorphic-recursion)
(provide/cond-contract [resolve-once (Type/c . -> . (or/c Type/c #f))])
(define-struct poly (name vars) #:prefab)
;; This parameter allows other parts of the typechecker to
;; request that the resolve cache isn't updated. This is needed
;; by the setup for recursive type aliases, since certain Name
;; types should not be cached while their mapping is still being
;; computed.
(define current-cache-resolve? (make-parameter #f))
;; Parameter<Option<Listof<Symbol>>>
;; This parameter controls whether or not the resolving process
;; should check for polymorphic recursion in implicit recursive
;; type names. This should only need to be enabled at type alias
;; definition time.
;;
;; If not #f, it should be a list of symbols that correspond
;; to the type parameters of the type being parsed.
(define current-check-polymorphic-recursion (make-parameter #f))
(define (resolve-name t)
(match t
[(Name: n) (let ([t (lookup-type-name n)])
(if (Type/c? t) t #f))]
[(Name: n _ _ _) (let ([t (lookup-type-name n)])
(if (Type/c? t) t #f))]
[_ (int-err "resolve-name: not a name ~a" t)]))
(define already-resolving? (make-parameter #f))
@ -31,7 +50,7 @@
(unless (= n (length rands))
(tc-error "wrong number of arguments to polymorphic type: expected ~a and got ~a"
n (length rands)))]
[(Name: n)
[(Name: n _ _ #t)
(when (and (current-poly-struct)
(free-identifier=? n (poly-name (current-poly-struct))))
(define num-rands (length rands))
@ -48,6 +67,50 @@
" does not match the given number:"
" expected " num-poly
", given " num-rands))))]
[(Name: _ _ args #f)
(cond [args
(define num-rands (length rands))
(define num-args (length args))
(unless (= num-rands num-args)
(tc-error (~a "The expected number of arguments for "
rator " does not match the given number:"
" expected " num-args
", given " num-rands)))
;; Does not allow polymorphic recursion since both type
;; inference and equirecursive subtyping for polymorphic
;; recursion are difficult.
;;
;; Type inference is known to be undecidable in general, but
;; practical algorithms do exist[1] that do not diverge in
;; practice.
;;
;; It is possible that equirecursive subtyping with polymorphic
;; recursion is as difficult as equivalence of DPDAs[2], which is
;; known to be decidable[3], but good algorithms may not exist.
;;
;; [1] Fritz Henglein. "Type inference with polymorphic recursion"
;; TOPLAS 1993
;; [2] Marvin Solomon. "Type definitions with parameters"
;; POPL 1978
;; [3] Geraud Senizergues.
;; "L(A)=L(B)? decidability results from complete formal systems"
;; TCS 2001.
;;
;; check-argument : Type Id -> Void
;; Check argument to make sure there's no polymorphic recursion
(define (check-argument given-type arg-name)
(define ok?
(if (F? given-type)
(type-equal? given-type (make-F (syntax-e arg-name)))
(not (member (syntax-e arg-name) (fv given-type)))))
(unless ok?
(tc-error (~a "Recursive type " rator " cannot be applied at"
" a different type in its recursive invocation"))))
(define current-vars (current-check-polymorphic-recursion))
(when current-vars
(for-each check-argument rands current-vars))]
[else
(tc-error "Type ~a cannot be applied, arguments were: ~a" rator rands)])]
[(Mu: _ _) (void)]
[(App: _ _ _) (void)]
[(Error:) (void)]
@ -59,7 +122,7 @@
[already-resolving? #t])
(resolve-app-check-error rator rands stx)
(match rator
[(Name: _)
[(Name: _ _ _ _)
(let ([r (resolve-name rator)])
(and r (resolve-app r rands stx)))]
[(Poly: _ _) (instantiate-poly rator rands)]
@ -81,8 +144,10 @@
[(Mu: _ _) (unfold t)]
[(App: r r* s)
(resolve-app r r* s)]
[(Name: _) (resolve-name t)])])
(when (and r* (not (currently-subtyping?)))
[(Name: _ _ _ _) (resolve-name t)])])
(when (and r*
(not (currently-subtyping?))
(current-cache-resolve?))
(hash-set! resolver-cache seq r*))
r*)))

20
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
View File

@ -181,8 +181,11 @@
(lambda (stx)
(syntax-case stx ()
[(_ i)
#'(or (and (Name: _) (app resolve-once (? Struct? i)))
(App: (and (Name: _) (app resolve-once (Poly: _ (? Struct? i)))) _ _))])))
#'(or (and (Name: _ _ _ #t)
(app resolve-once (? Struct? i)))
(App: (and (Name: _ _ _ #t)
(app resolve-once (Poly: _ (? Struct? i))))
_ _))])))
(define (subtype/flds* A flds flds*)
(for/fold ([A A]) ([f (in-list flds)] [f* (in-list flds*)] #:break (not A))
@ -210,7 +213,8 @@
(or (free-identifier=? s-name p-name)
(match s
[(Poly: _ (? Struct? s*)) (in-hierarchy? s* par)]
[(Struct: _ (and (Name: _) p) _ _ _ _) (in-hierarchy? (resolve-once p) par)]
[(Struct: _ (and (Name: _ _ _ #t) p) _ _ _ _)
(in-hierarchy? (resolve-once p) par)]
[(Struct: _ (? Struct? p) _ _ _ _) (in-hierarchy? p par)]
[(Struct: _ (Poly: _ p) _ _ _ _) (in-hierarchy? p par)]
[(Struct: _ #f _ _ _ _) #f]
@ -582,6 +586,16 @@
(subtype* s-out t-out))]
[((Param: in out) t)
(subtype* A0 (cl->* (-> out) (-> in -Void)) t)]
[((Instance: (? needs-resolving? s)) other)
(let ([s* (resolve-once s)])
(if (Type/c? s*)
(subtype* A0 (make-Instance s*) other)
#f))]
[(other (Instance: (? needs-resolving? t)))
(let ([t* (resolve-once t)])
(if (Type/c? t*)
(subtype* A0 other (make-Instance t*))
#f))]
[((Instance: (Class: _ _ field-map method-map augment-map _))
(Instance: (Class: _ _ field-map* method-map* augment-map* _)))
(define (subtype-clause? map map*)

6
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-error.rkt
View File

@ -14,7 +14,8 @@
#:rest (c:listof c:any/c) . c:->* . c:any/c)]
[lookup-fail (identifier? . c:-> . Type/c)]
[lookup-type-fail (identifier? . c:-> . Type/c)])
[lookup-type-fail (identifier? . c:-> . Type/c)]
[lookup-variance-fail (identifier? . c:-> . void?)])
;; produce a type-checking error, and also return a result (e.g., a type)
(define (tc-error/expr msg
@ -66,3 +67,6 @@
(define (lookup-type-fail i)
(tc-error/expr "~a is not bound as a type" (syntax-e i)))
(define (lookup-variance-fail i)
(int-err "~a is bound but missing a variance" (syntax-e i)))

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/union.rkt
View File

@ -27,7 +27,7 @@
;; If a union element is a Name application, then it should not
;; be checked for subtyping since that can cause infinite
;; loops if this is called during type instantiation.
[((App: (and (Name: _) rator) rands stx) _)
[((App: (? Name? rator) rands stx) _)
;; However, we should check if it's a well-formed application
;; so that bad applications are rejected early.
(resolve-app-check-error rator rands stx)

4
pkgs/typed-racket-pkgs/typed-racket-more/typed/pict.rkt
View File

@ -6,10 +6,10 @@
make-Union)))
(begin-for-syntax
(define -pict (make-Name #'pict))
(define -pict (make-Name #'pict null #f #t))
(define -pict-path
(make-Union (list (-val #f) -pict (-lst -pict))))
(define -child (make-Name #'child))
(define -child (make-Name #'child null #f #t))
(define -pin-arrow-line
(->key -Real
-pict

28
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/even-odd-recursive-contract.rkt Normal file
View File

@ -0,0 +1,28 @@
#;
(exn-pred #rx"blaming: \\(interface for even->odd\\)")
#lang racket/load
;; Test mutually recursive type alias contract generation
;; with polymorphism
(module untyped racket
(define (even->odd elem lst) (cons 3 lst))
(provide even->odd))
(module poly-even/odd typed/racket
(define-type (Even A) (U Null (Pairof A (Odd A))))
(define-type (Odd A) (Pairof A (Even A)))
(: even-lst (Even Integer))
(define even-lst '(1 2 3 4))
(: odd-lst (Odd Integer))
(define odd-lst '(1 2 3))
(require/typed 'untyped
[even->odd (All (A) (A (Even A) -> (Odd A)))])
(even->odd 3 even-lst) )
(require 'poly-even/odd)

8
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion-2.rkt Normal file
View File

@ -0,0 +1,8 @@
#;
(exn-pred #rx"cannot be applied at a different type")
#lang typed/racket
;; Polymorphic recursion should fail
(define-type (Foo A) (Listof (Foo (Listof A))))

12
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion-3.rkt Normal file
View File

@ -0,0 +1,12 @@
#;
(exn-pred #rx"cannot be applied at a different type")
#lang typed/racket
;; Polymorphic recursion should fail through mutual recursion
(define-type (Foo A) (Listof (Bar (Listof A))))
(define-type (Bar B) (Listof (Foo (Listof B))))
(define-type (Foo2 A) (Listof (Bar2 (Listof A))))
(define-type (Bar2 B) (Listof (Foo2 B)))

39
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion.rkt Normal file
View File

@ -0,0 +1,39 @@
#;
(exn-pred #rx"cannot be applied at a different type")
#lang typed/racket
;; Example from Wikipedia
;; http://en.wikipedia.org/w/index.php?title=Polymorphic_recursion&oldid=543854337
;; Note that the following code does not work, but some
;; of it could work if polymorphic recursion were implemented
;; in the future.
;;
;; Right now the type definition of Nested should throw a static error
(struct: (A B) :<: ([left : A] [right : B])
#:transparent)
(struct: ε ())
;; Note that this type uses polymorphic recursion
(define-type (Nested A)
(U (:<: A (Nested (Listof A))) ε))
(: nested (Nested Integer))
(define nested
(:<: 1 (:<: (list 2 3 4) (:<: (list (list 4 5) (list 7) (list 8 9)) (ε)))))
;; inference loops forever for this one...
(: nested-length (All (A) ((Nested A) -> Integer)))
(define (nested-length n)
(if (ε? n)
0
;; explicit instantiation needed
(add1 ((inst nested-length (Listof A)) (:<:-right n)))))
;; Test subtyping with polymorphic recursion
(: nested2 (Nested Number))
(define nested2 nested)
(provide nested nested-length :<: Nested ε)

8
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/recursive-type-application.rkt Normal file
View File

@ -0,0 +1,8 @@
#;
(exn-pred #rx"does not match the given number:")
#lang typed/racket
;; Check bad arity for recursive invocation of Foo
(define-type (Foo A) (Listof (Foo A A)))

31
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/both-recursive-types.rkt Normal file
View File

@ -0,0 +1,31 @@
#lang typed/racket
;; Make sure that recursive types defined using
;; different recursion methods are compatible with
;; each other
(define-type (L1 A) (U Null (Pairof A (L1 A))))
(define-type (L2 A) (Rec X (U Null (Pairof A X))))
(define-type (L3 A) (Rec X (U Null (Pairof A (L3 A)))))
(: x (L1 Integer))
(define x '(1 2 3))
(: y (L2 Number))
(define y x)
(: z (L3 Number))
(define z x)
(: a (Listof Number))
(define a x)
(: b (L1 Number))
(define b a)
(: c (L1 Number))
(define c y)
(: d (L1 Number))
(define d z)

75
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/even-odd-recursive-type.rkt Normal file
View File

@ -0,0 +1,75 @@
#lang racket
(require rackunit)
(module num-even/odd typed/racket
(define-type Even (U Null (Pairof Number Odd)))
(define-type Odd (Pairof Number Even))
(: even-lst Even)
(define even-lst '(1 2 3 4))
(: odd-lst Odd)
(define odd-lst '(1 2 3)))
(module poly-even/odd typed/racket
(define-type (Even A) (U Null (Pairof A (Odd A))))
(define-type (Odd A) (Pairof A (Even A)))
(: even-lst (Even Integer))
(define even-lst '(1 2 3 4))
(: odd-lst (Odd Integer))
(define odd-lst '(1 2 3))
(: even->odd (All (A) (A (Even A) -> (Odd A))))
(define (even->odd elem lst)
(cons elem lst))
(provide even->odd Even Odd even-lst odd-lst))
;; make sure it works in a let
(module let-even/odd typed/racket
(let ()
(define-type (Even A) (U Null (Pairof A (Odd A))))
(define-type (Odd B) (Pairof B (Even B)))
(: even-lst (Even Integer))
(define even-lst '(1 2 3 4))
(: odd-lst (Odd Integer))
(define odd-lst '(1 2 3))
(cons 3 even-lst)))
(module even/odd* typed/racket
;; weird variant that alternates types between
;; Even and Odd
(define-type (Even A B) (U Null (Pairof A (Odd A B))))
(define-type (Odd A B) (Pairof B (Even A B)))
(: even-lst (Even Integer String))
(define even-lst '(1 "b" 3 "a"))
(: odd-lst (Odd Integer String))
(define odd-lst '("b" 2 "a"))
;; specialized for more interesting contract
(: even->odd (String (Even Integer String) -> (Odd Integer String)))
(define (even->odd elem lst) (cons elem lst))
(provide even-lst odd-lst even->odd))
(require (prefix-in a: 'num-even/odd))
(require (prefix-in b: 'poly-even/odd))
(require (prefix-in c: 'let-even/odd))
(require (prefix-in d: 'even/odd*))
;; make sure contract generation on even/odd* worked
(cons 3 d:odd-lst)
(check-equal? (d:even->odd "c" d:even-lst) '("c" 1 "b" 3 "a"))
(check-exn exn:fail:contract? (λ () (d:even->odd 1 d:even-lst)))
(b:even->odd "c" b:even-lst)
(check-exn exn:fail:contract? (λ () (b:even->odd "c" b:odd-lst)))

26
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/non-recursive-and-recursive-type-aliases.rkt Normal file
View File

@ -0,0 +1,26 @@
#lang typed/racket
;; This test used to fail when the non-recursive type
;; aliases were registered *after* the recursive ones.
;;
;; Thanks to Havvy from IRC for the test
(define-type magic/int Integer)
(define-type magic/float Flonum)
(define-type magic/str String)
(define-type magic/symbol Symbol)
(define-type magic/map HashTable)
(define-type magic/invokable (magic/any * -> magic/any))
(define-type magic/any (U magic/int
magic/float
magic/str
magic/symbol
magic/map
magic/invokable))
(: x magic/any)
(define x "magic/str")
(: f magic/invokable)
(define f (lambda: (rst : magic/any *) (car rst)))

38
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/rec-type-alias-variance.rkt Normal file
View File

@ -0,0 +1,38 @@
#lang typed/racket
;; Test subtyping and variance for recursive type aliases
(define-type (B X)
(U (Listof X) (Setof (B X))))
(: b1 (B String))
(define b1 (list "foo"))
(: b2 (B (U String Symbol)))
(define b2 b1)
(: f (All (Y) (Y -> (B Y))))
(define (f x) (list x))
(: g (All (X) (X -> (B X))))
(define g f)
;; Adapted from struct variance test
(define-type (Boxer D) (List (Boxer2 D)))
(define-type (Boxer2 D) (List (D -> Void) (Boxer D)))
(: f-Boxer (All (D) ((Boxer D) D -> Void)))
(define (f-Boxer boxer v)
((car (car boxer)) v))
;; The last line in this example would error without
;; registering the variance
(define-type (Even A) (U Null (Pairof A (Odd A))))
(define-type (Odd A) (Pairof A (Even A)))
(: even->odd (All (A) (A (Even A) -> (Odd A))))
(define (even->odd elem lst)
(cons elem lst))
(even->odd 3 '(1 2))

20
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/recursive-type-alias-top-level.rkt Normal file
View File

@ -0,0 +1,20 @@
#lang racket
;; Make sure type aliases are registered from a module
;; to another context appropriately
(require racket/sandbox)
(define evaluator
(call-with-trusted-sandbox-configuration
(λ () (make-evaluator 'typed/racket))))
(evaluator '(require typed/racket))
(evaluator '(module a typed/racket
(define-type (Foo A) (Option (Listof (Foo A))))
(: x (Foo Integer))
(define x #f)
(provide x)))
(evaluator '(require 'a))
(evaluator 'x)

1
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/all-tests.rkt
View File

@ -34,6 +34,7 @@
"contract-tests.rkt"
"interactive-tests.rkt"
"type-printer-tests.rkt"
"type-alias-helper.rkt"
"class-tests.rkt"
"class-util-tests.rkt"
"check-below-tests.rkt"

78
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/type-alias-helper.rkt Normal file
View File

@ -0,0 +1,78 @@
#lang racket/base
;; Unit tests for the type-alias-helper.rkt module
(require "test-utils.rkt"
racket/set
rackunit
syntax/id-table
typed-racket/env/type-alias-helper)
(provide tests)
(gen-test-main)
;; two aliases in their own components
(define example-1
(list (cons #'x (list #'x))
(cons #'y (list #'y))))
;; all one component
(define example-2
(list (cons #'x (list #'x #'y))
(cons #'y (list #'x))))
;; two components, one with two nodes
(define example-3
(list (cons #'x (list #'y))
(cons #'y (list #'x))
(cons #'z (list))))
;; one with cycles, two that form a line
(define example-4
(list (cons #'x (list #'y))
(cons #'y (list #'x))
(cons #'a (list #'b))
(cons #'b (list))))
;; two large cycles
(define example-5
(list (cons #'x (list #'y #'z))
(cons #'y (list #'x))
(cons #'z (list #'x #'y))
(cons #'a (list #'b))
(cons #'b (list #'c))
(cons #'c (list #'a))))
;; check topological order
(define example-6
(list (cons #'a (list #'b))
(cons #'d (list))
(cons #'c (list #'d #'e))
(cons #'b (list #'c))
(cons #'e (list #'f))
(cons #'f (list))))
;; helper function for the tests below
;; ignores order of ids in the components and the
;; order of the components (because neither are stable
;; except for topological ordering).
(define (equal-id-sets? x y)
(define (id-lsts->id-sets id-lsts)
(for/set ([id-lst id-lsts])
(for/set ([id id-lst]) (syntax-e id))))
(equal? (id-lsts->id-sets x)
(id-lsts->id-sets y)))
(define-binary-check (check-equal?/id equal-id-sets? actual expected))
(define tests
(test-suite
"Tests for type-alias-helper"
(check-equal?/id (find-strongly-connected-type-aliases example-1)
(list (list #'x) (list #'y)))
(check-equal?/id (find-strongly-connected-type-aliases example-2)
(list (list #'x #'y)))
(check-equal?/id (find-strongly-connected-type-aliases example-3)
(list (list #'z) (list #'x #'y)))
(check-equal?/id (find-strongly-connected-type-aliases example-4)
(list (list #'a) (list #'b) (list #'y #'x)))
(check-equal?/id (find-strongly-connected-type-aliases example-5)
(list (list #'b #'a #'c) (list #'z #'x #'y)))
(check-equal?/id (find-strongly-connected-type-aliases example-6)
(list (list #'a) (list #'b) (list #'c)
(list #'e) (list #'f) (list #'d)))))

17
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -2398,6 +2398,23 @@
void))
(display "hello" accumulator/not-thread-safe))
-Void]
;; Additional tests for recursive type aliases
[tc-e ;; The types here are valid, but uninhabitable.
(let () (define-type-alias A (Listof B))
(define-type-alias B (Listof A))
"dummy")
#:ret (ret -String -true-filter)]
[tc-e (let () (define-type-alias A (Listof B))
(define-type-alias B (U #f (Listof A)))
(: a A)
(define a (list #f (list (list #f))))
(void))
-Void]
[tc-err (let () (define-type-alias A (Class #:implements A)) "dummy")
#:msg "Recursive #:implements clause not allowed"]
[tc-err (let () (define-type-alias X (U X #f)) "dummy")
#:msg "Recursive types are not allowed directly inside"]
)
(test-suite
"tc-literal tests"