suzanne.soy/typed-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.

original commit: a8cc430d0fc7090dd758e0f6738296edcb4d8490
This commit is contained in:
Asumu Takikawa 2013-07-30 12:21:44 -04:00
parent f6f23ef043
commit 8ff305e328
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"