[racket] TR define-new-type, Value Types

Do refinement types work for what you want?

http://docs.racket-lang.org/ts-reference/Experimental_Features.html?q=refinement#(form._((lib._typed-racket/base-env/prims..rkt)._declare-refinement))

#lang typed/racket
(declare-refinement even?)
(: two (Refinement even?))
(define two
  (let ((x 2))
    (if (even? x) x (error 'bad))))

There are a couple of issues with them, mostly that they are not sound when
dealing with mutable objects or non pure functions, which allows you to
break the soundness of TR.
http://bugs.racket-lang.org/query/?cmd=view+audit-trail&pr=13059


On Fri, Dec 28, 2012 at 2:17 PM, Ray Racine <ray.racine at gmail.com> wrote:

> Any plans something along the lines of Scala's proposed Value Types.
>
> A path:
>
> Allow for "special" struct: decls (vstruct: ?) where the parent is a
> limited subset of non structure parent types (base value types such as
> String, Number).
>
> These special structures MUST contain one and only one value of the parent
> "special" type or it is a compile error.
> The structure constructor does not construct the wrapping structure but
> instead passes through the wrapped value, but *always* invokes the
> validator during pass-thru.
> TR treats the type as a subtype of the base value type.
>
> e.g.
>
> (struct: Identifier String ([value : String])
>   #:methods gen:validator (lambda (thing) ...) ;; is of type (Any ->
> Boolean : Identifier))
>
> (define id (Identifier "myidentifier")) ;; validator invoked, no structure
> was allocated, `id' is just a String value, is a subtype of String.
>
> (define uc-id (Identifer (string-upcase id))) ;; validator invoked, as id
> is a just a string no unboxing in (string-upcase id), in fact no
> allocations here at all.
>
> Under the covers the Identifier constructor never creates the structure,
> it acts as a pass through id : (String -> String) function.  i.e. the
> runtime representation of `id' is always as a String so any struct <->
> value boxing / unboxing is avoided.   I think there is enough machinery in
> place to get pretty close to this.
>
> What is gained?
>
> What is done internally in TR defining Natural, Index,
> Exact-Positive-Integer can now be done without special internal defining,
> just another constrained base type.  One can start to define things like
> Age [1 .. 120].
> Another is IMHO a HUGE source of program error is just not enough time to
> do proper validation at IO boundries where entering data is of the form
> Strings and Bytes and it needs to be lifted.
>
> Consider the following typical use case from Amazon's AWS API, a Tasklist
> parameter.
>
> Parameter - Tasklist : String[1-256]
>
> Specifies the task list to poll for activity tasks.
>
> The specified string must not start or end with whitespace. It must not
> contain a : (colon), / (slash), | (vertical bar), or any control characters
> (\u0000-\u001f | \u007f - \u009f). Also, it must not contain the literal
> string "arn".
>
> Most likely, I'll punt.
>
> (: call-it (String ... -> ...))
> (define (call-it task-list ...)
>
> If I'm ambitious today.
>
> ;; would prefer (define-new-type Tasklist String)
> (define-type Tasklist String) ;; tighten things later down the road,
> <sigh> none type generative
>
> (: call-it (Tasklist ... -> ...))
> (define (call-it task-list ...)
>
> What I'd like to do.
>
> (define-value-type Tasklist String [1 .. 256] (lambda (this) ....)) ;; mad
> use of regexp in validator fn (Any -> Boolean : Tasklist)
>
> (call-it (Tasklist "mytasklist") ...)
>
> (call-it (Tasklist "arn:bad/tasklist") ...)
>
> (define-value-type Age Integer [1 .. 120]) ;; no special validation beyond
> bounds check.
>
>
>
>
>
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20121228/17dd20f1/attachment.html>