diff --git a/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl index aa676217..df5145b2 100644 --- a/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl +++ b/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl @@ -465,6 +465,25 @@ the type: (define-type Bar (U Bar False))] } +@section{Defining New Subtypes} + +@defform[(define-new-subtype name (constructor t))]{ +Defines a new type @racket[name] that is a subtype of @racket[t]. +The @racket[constructor] is defined as a function that takes a value of type +@racket[t] and produces a value of the new type @racket[name]. +A @racket[define-new-subtype] definition is only allowed at the top level of a +file or module. +@ex[(module m typed/racket + (provide Radians radians f) + (define-new-subtype Radians (radians Real)) + (: f : [Radians -> Real]) + (define (f a) + (sin a))) + (require 'm) + (radians 0) + (f (radians 0))] +} + @section{Generating Predicates Automatically} @defform[(make-predicate t)]{ diff --git a/typed-racket-lib/typed-racket/base-env/prims-struct.rkt b/typed-racket-lib/typed-racket/base-env/prims-struct.rkt index 9b3973e4..49037590 100644 --- a/typed-racket-lib/typed-racket/base-env/prims-struct.rkt +++ b/typed-racket-lib/typed-racket/base-env/prims-struct.rkt @@ -29,7 +29,8 @@ (begin-for-syntax (lazy-require [syntax/struct (build-struct-names)])) -(provide define-typed-struct -struct define-typed-struct/exec define-type-alias dtsi* dtsi/exec*) +(provide define-typed-struct -struct define-typed-struct/exec dtsi* dtsi/exec* + define-type-alias define-new-subtype) (define-for-syntax (with-type* expr ty) (with-type #`(ann #,expr #,ty))) @@ -209,3 +210,27 @@ #'(begin)) #,(internal (syntax/loc stx (define-type-alias-internal tname type poly-vars))))])) + +(define-syntax define-new-subtype + (lambda (stx) + (unless (memq (syntax-local-context) '(module module-begin)) + (raise-syntax-error 'define-new-subtype + "can only be used at module top-level")) + (syntax-parse stx + [(define-new-subtype ty:id (constructor:id rep-ty:expr)) + #:with gen-id (generate-temporary #'ty) + #:with 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 + #,(ignore + #'(begin + (define-syntax ty stx-err-fun) + (define constructor (lambda (x) x)))) + #,(internal (syntax/loc stx + (define-new-subtype-internal ty (constructor rep-ty) #:gen-id gen-id))))]))) + diff --git a/typed-racket-lib/typed-racket/base-env/prims.rkt b/typed-racket-lib/typed-racket/base-env/prims.rkt index f6fec418..6cd6f35f 100644 --- a/typed-racket-lib/typed-racket/base-env/prims.rkt +++ b/typed-racket-lib/typed-racket/base-env/prims.rkt @@ -39,6 +39,7 @@ the typed racket language. (all-from-out "case-lambda.rkt") (all-from-out (submod "prims-contract.rkt" forms)) define-type-alias + define-new-subtype define-typed-struct define-typed-struct/exec ann inst diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt index 1609ae74..c8fb942e 100644 --- a/typed-racket-lib/typed-racket/private/type-contract.rkt +++ b/typed-racket-lib/typed-racket/private/type-contract.rkt @@ -351,6 +351,8 @@ (listof/sc (t->sc elem-ty))] [(Base: sym cnt _ _) (flat/sc #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt)) sym)] + [(Distinction: _ _ t) ; from define-new-subtype + (t->sc t)] [(Refinement: par p?) (and/sc (t->sc par) (flat/sc p?))] [(Union: elems) diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt index 90c3fa71..7ae70e1a 100644 --- a/typed-racket-lib/typed-racket/rep/type-rep.rkt +++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt @@ -579,6 +579,17 @@ [#:frees (λ (f) (make-invariant (f value)))] [#:key 'continuation-mark-key]) +;; Distinction +;; comes from define-new-subtype +;; nm: a symbol representing the name of the type +;; id: a symbol created with gensym +;; ty: a type for the representation, where this will be a subtype of ty +(def-type Distinction ([nm symbol?] [id symbol?] [ty Type/c]) + [#:frees (λ (f) (f ty))] + [#:intern (list (Rep-seq ty) nm id)] + [#:fold-rhs (*Distinction nm id (type-rec-id ty))] + [#:key (Type-key ty)]) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; remove-dups: List[Type] -> List[Type] diff --git a/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt b/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt index db833499..54bc20b6 100644 --- a/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt +++ b/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt @@ -21,6 +21,7 @@ internal type-alias + new-subtype-def type-refinement typed-struct typed-struct/exec @@ -31,6 +32,7 @@ typecheck-failure type-alias? + new-subtype-def? typed-struct? typed-struct/exec?) @@ -50,6 +52,7 @@ (internal-forms internal-literals require/typed-internal define-type-alias-internal + define-new-subtype-internal define-type-internal define-typed-struct-internal define-typed-struct/exec-internal @@ -127,6 +130,8 @@ (define-internal-classes [type-alias (define-type-alias-internal name type args)] + [new-subtype-def + (define-new-subtype-internal name (constructor rep-type) #:gen-id gen-id)] [type-refinement (declare-refinement-internal predicate)] [typed-struct diff --git a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt index 3421fa41..e4888a20 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt @@ -67,6 +67,17 @@ [_:type-alias (list)] + ;; define-new-subtype + [form:new-subtype-def + ;; (define-new-subtype-internal name (constructor rep-type) #:gen-id gen-id) + (define name (syntax-e (attribute form.name))) + (define sym (syntax-e (attribute form.gen-id))) + (define rep-ty (parse-type (attribute form.rep-type))) + (define new-ty (-Distinction name sym rep-ty)) + (register-type (attribute form.constructor) (-> rep-ty new-ty)) + (register-type-alias (attribute form.name) new-ty) + (list)] + ;; declare-refinement ;; FIXME - this sucks and should die [t:type-refinement diff --git a/typed-racket-lib/typed-racket/types/abbrev.rkt b/typed-racket-lib/typed-racket/types/abbrev.rkt index 82d959d3..563c38e8 100644 --- a/typed-racket-lib/typed-racket/types/abbrev.rkt +++ b/typed-racket-lib/typed-racket/types/abbrev.rkt @@ -286,6 +286,10 @@ (define-syntax-rule (->opt args ... [opt ...] res) (opt-fn (list args ...) (list opt ...) res)) +;; from define-new-subtype +(define (-Distinction name sym ty) + (make-Distinction name sym ty)) + ;; class utilities (begin-for-syntax diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt index cf33d91b..c91c09be 100644 --- a/typed-racket-lib/typed-racket/types/printer.rkt +++ b/typed-racket-lib/typed-racket/types/printer.rkt @@ -517,6 +517,8 @@ `(Sequenceof ,@(map t->s ts))] [(Error:) 'Error] [(fld: t a m) `(fld ,(type->sexp t))] + [(Distinction: name sym ty) ; from define-new-subtype + name] [else `(Unknown Type: ,(struct->vector type))] )) diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt index b3cb9cb7..e6f24906 100644 --- a/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/typed-racket-lib/typed-racket/types/subtype.rkt @@ -292,6 +292,9 @@ #f] [((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _))) #f] + ;; from define-new-subtype + [((Distinction: _ _ t1) t2) + (subtype* A0 t1 t2)] ;; sequences are covariant [((Sequence: ts) (Sequence: ts*)) (subtypes* A0 ts ts*)] diff --git a/typed-racket-test/fail/define-new-subtype.rkt b/typed-racket-test/fail/define-new-subtype.rkt new file mode 100644 index 00000000..4c5d8375 --- /dev/null +++ b/typed-racket-test/fail/define-new-subtype.rkt @@ -0,0 +1,5 @@ +#lang typed/racket/base + +(require "../succeed/define-new-subtype.rkt") + +(sin (degrees 0)) diff --git a/typed-racket-test/succeed/define-new-subtype.rkt b/typed-racket-test/succeed/define-new-subtype.rkt new file mode 100644 index 00000000..3bab1d6d --- /dev/null +++ b/typed-racket-test/succeed/define-new-subtype.rkt @@ -0,0 +1,35 @@ +#lang typed/racket/base + +(provide Radians Degrees radians degrees + sin cos tan asin acos atan + degrees->radians radians->degrees + ) + +(require (prefix-in rkt: (combine-in typed/racket/base racket/math))) + +(define-new-subtype Radians (radians Real)) +(define-new-subtype Degrees (degrees Real)) + +(: sin : Radians -> Real) +(: cos : Radians -> Real) +(: tan : Radians -> Real) +(define (sin x) (rkt:sin x)) +(define (cos x) (rkt:sin x)) +(define (tan x) (rkt:tan x)) +(: asin : Real -> Radians) +(: acos : Real -> Radians) +(: atan : Real -> Radians) +(define (asin x) (radians (rkt:asin x))) +(define (acos x) (radians (rkt:acos x))) +(define (atan x) (radians (rkt:atan x))) + +(: degrees->radians : Degrees -> Radians) +(: radians->degrees : Radians -> Degrees) +(define (degrees->radians x) + (radians (rkt:degrees->radians x))) +(define (radians->degrees x) + (degrees (rkt:radians->degrees x))) + +(void + (sin (asin 1/2)) + )