Of course, now we all know who to thank, the *real* brain behind this outfit, thank you, Most Functional Man In The World.
On Fri, Dec 28, 2012 at 10:04 PM, Ray Racine <ray.rac...@gmail.com> wrote: > Heh, defined the type predicate and never leveraged it. This is looking > very promising. > > #lang typed/racket > > (provide > Even Even? +e) > > (declare-refinement even?) > (define-type Even (Refinement even?)) > (define-predicate Even? Even) > > ;; Optimizer says this is in-lined away. Now I'm getting down right giddy. > (: An-Even (Number -> Even)) > (define (An-Even num) > (assert num Even?)) > > (: +e (Even Even -> Even)) > (define (+e e1 e2) > (An-Even (+ e1 e2))) > > (+e (An-Even 4) (An-Even 6)) > (+e (An-Even 2) (An-Even 3)) > > > On Fri, Dec 28, 2012 at 9:37 PM, Ray Racine <ray.rac...@gmail.com> wrote: > >> Can I just say, "DAMN YOU GUYS ARE GOOD." Thank you. >> >> #lang typed/racket >> >> (declare-refinement even?) >> >> (define-type Even (Refinement even?)) >> >> (define-predicate Even? Even) >> >> (: An-Even (Number -> Even)) >> (define (An-Even num) >> (if (Even? num) >> num >> (error 'I-DONT-DO-ODD))) >> >> (: +e (Even Even -> Even)) >> (define (+e e1 e2) >> (let ((y (+ e1 e2))) >> (if (Even? y) >> y >> (error 'RING-OF-EVEN-VIOLATION)))) >> >> (+e (An-Even 4) (An-Even 6)) >> (+e (An-Even 2) (An-Even 3)) >> >> >> On Fri, Dec 28, 2012 at 9:01 PM, Ray Racine <ray.rac...@gmail.com> wrote: >> >>> Thanks, I'll poke around with TR's refinement types. If anyone has a >>> reference detailing on the nature of TR's refinement types, please forward. >>> In progress paper etc. >>> >>> >>> On Fri, Dec 28, 2012 at 8:53 PM, Carl Eastlund <c...@ccs.neu.edu> wrote: >>> >>>> What you describe sounds exactly like Typed Racket's refinement types. >>>> Statically typed languages like SML often incorporate refinements that can >>>> be determined entirely statically. TR allows arbitrary dynamic checks for >>>> its refinements, so it gets the "weak sort of Dependent Type" results you >>>> mention. So I wouldn't judge the capabilities of TR's refinement types >>>> based on papers about SML. >>>> >>>> Carl Eastlund >>>> >>>> On Fri, Dec 28, 2012 at 8:35 PM, Ray Racine <ray.rac...@gmail.com>wrote: >>>> >>>>> Based on a google of a paper on refinement types in SML, no. Useful >>>>> in their own right, and thanks for pointing out their >>>>> (experimental) existence. I'm thinking more along the line of a quick win >>>>> of a weak sort of Dependent Type for value types such as Number and String >>>>> by leveraging existent Racket machinery. >>>>> >>>>> See >>>>> https://docs.google.com/document/d/10TQKgMiJTbVtkdRG53wsLYwWM2MkhtmdV25-NZvLLMA/edit >>>>> for >>>>> a Scala endeavor along similar lines. >>>>> >>>>> The goal is to support efficient generative, constrained, sub-types of >>>>> primitive value types, specifically String and Number with minimal surgery >>>>> to Racket. >>>>> >>>>> Consider: >>>>> >>>>> (define-value-type Age : Integer [1 .. 120]) >>>>> (define-value-type SSN : String [1 .. 9 | 11] ssn-validation-predicate) >>>>> >>>>> Goals: >>>>> >>>>> 1) Avoid boxing/unboxing (struct cell / cell-refs). >>>>> 2) Create generative sub-types of certain base types, String, Number >>>>> to satisfy TR. Note they are not opaque types but, i.e. T <: String >>>>> >>>>> Item 2) means >>>>> >>>>> ;; works as Ages are Integers >>>>> (: add-ages (Age Age -> Age)) >>>>> (define (sum-ages a1 a2) >>>>> (Age (+ a1 a2)) ;; + defined on Integers >>>>> >>>>> ;; not the same as (define-type Age Integer) because ... >>>>> (sum-ages 12 16) ;; fails as Integers are not Ages >>>>> >>>>> ;; lifting Integer to Age involves a runtime contract check, but no >>>>> allocation. >>>>> (sum-ages (Age 12) (Age 16)) ;; fine, no allocation >>>>> >>>>> A hand waved way of getting there, which got ugly quick and as I >>>>> typed. I was sort of brainstorming if I could get Value Types without >>>>> any >>>>> Racket internal surgery and with no more than a bit of macrology. >>>>> >>>>> So waving both hands wildly... >>>>> >>>>> 0) Modify the TR `cast' operator to recognize Value Type structures. >>>>> >>>>> a) The generated contract from the `cast' operator of a value type to >>>>> an appropriate Value Type structure succeeds at runtime for an instance of >>>>> the value type. >>>>> b) The generated contract from the `cast' operator applies the >>>>> gen:validator on the Value Type structure as part of the contract. >>>>> >>>>> 1) Extend the struct: macro to allow a struct: parent to be not only >>>>> another struct: but a [struct: | String | Number] >>>>> >>>>> a) IF the parent is a struct: nothing new to do here. >>>>> >>>>> b) If parent is a value type, String or a Number (value type) >>>>> - This is a Value Type structure. >>>>> - A value type structure has only one mandatory value which is of >>>>> the same type as the parent. >>>>> - A Value Type structure is -sealed- and may not be used as the >>>>> parent in another struct: definition. >>>>> - A Value Type structure's constructor is a (A -> A) pass-thru of >>>>> the value. i.e., the struct: is never allocated to wrap the value. >>>>> - A Value Type structure _may_ have a gen:validate generic method >>>>> associated with it. >>>>> >>>>> 4) To avoid creating a true Value Type structure instance via low >>>>> level apis, they would need to be modified to prohibit creating any >>>>> instance of a Value Type structure. >>>>> >>>>> What we are trying to achieve is all of the type checking from TR >>>>> using struct: to generate a new type at compile time, yet at runtime the >>>>> instance values of the Value Type are the primitive values and are NOT >>>>> manifested as the struct: instances. >>>>> >>>>> Example: >>>>> Create an SSN Value Type. >>>>> >>>>> ;; An SSN is String value, of length 9 or 11, which is validated by a >>>>> regular expression. >>>>> >>>>> (: ssn-validation-predicate (String -> Boolean : SSN)) >>>>> (define (ssn-validation-predicate str-ssn) >>>>> (regexp-match? ssn #rx(....))) >>>>> >>>>> (define-value-type SSN String [9 | 11] ssn-validation-predicate) ;; >>>>> >>>>> The above roughly expands to: >>>>> >>>>> (struct: SSN String ([value : String]) >>>>> #:methods gen:validate ssn-validation-predicate) >>>>> >>>>> (define SSN-validator-contract (and/contract ....)) ;;; combines >>>>> string-length 9|11 check with ssn-validation-predicate into a contract >>>>> >>>>> The struct: macro notes that this is a Value Type structure definition >>>>> because its parent is a value type, String, and not another struct:. So >>>>> the generated SSN constructor function avoids creating an actual structure >>>>> at runtime and allows a string value as successfully cast to a SSN after >>>>> applying any associated validation contract. >>>>> >>>>> (: SSN (String -> SSN)) >>>>> (define (SSN ssn) >>>>> (cast ssn SSN)) >>>>> >>>>> In the above ... >>>>> - `cast' knows we are casting to a Value Type, SSN, so generated >>>>> runtime contract allows a String value (and _not_ a SSN struct type >>>>> instance) to be "passed-thru" but lifted to type SSN for TR purposes. >>>>> - Therefore, the cast fails an actual instance of an SSN structure, >>>>> if one somehow managed to construct an instance. >>>>> - As part of the `cast' generated contract the SSN-validator-contract >>>>> and length checks are combined and applied interstitial in the pass-thru >>>>> of >>>>> (String -> String). >>>>> >>>>> And finally since SSN at runtime is a string value, at compile time >>>>> it's a subtype of String so... >>>>> >>>>> (substring (SSN "123-45-6789") 0 3) ;; works at TR compile time >>>>> checking and at runtime running >>>>> (substring (SSN "123x456-5689") 0 3) ;; fails validation at runtime, >>>>> though a sufficiently smart compiler would apply the contract validation >>>>> check at compile time for values known at compile time. >>>>> >>>>> Given: >>>>> >>>>> (: parse-ssn (SSN -> (Listof String))) >>>>> (define (parse-ssn ssn) >>>>> (regexp-split ssn #rx"-")) >>>>> >>>>> (parse-ssn "123-456-6789") ;; nope as strings are not SSNs >>>>> (parse-ssn (SSN "123-456-6789")) ;; works but runtime representation >>>>> remained as a string value, no struct: box/unbox. >>>>> >>>>> >>>>> >>>>> >>>>> >>>>> >>>>> On Fri, Dec 28, 2012 at 5:58 PM, Eric Dobson >>>>> <eric.n.dob...@gmail.com>wrote: >>>>> >>>>>> 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.rac...@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 >>>>>>> >>>>>>> >>>>>> >>>>> >>>>> ____________________ >>>>> Racket Users list: >>>>> http://lists.racket-lang.org/users >>>>> >>>>> >>>> >>> >> >
____________________ Racket Users list: http://lists.racket-lang.org/users
