Merge pull request #149 from AlexKnauth/newtype

add define-new-subtype
This commit is contained in:
Alex Knauth 2015-07-30 02:08:19 -04:00
commit 5e1334c02e
12 changed files with 124 additions and 1 deletions

View File

@ -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)]{

View File

@ -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))))])))

View File

@ -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

View File

@ -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)

View File

@ -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]

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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))]
))

View File

@ -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*)]

View File

@ -0,0 +1,5 @@
#lang typed/racket/base
(require "../succeed/define-new-subtype.rkt")
(sin (degrees 0))

View File

@ -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))
)