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

From: Neil Toronto (neil.toronto at gmail.com)
Date: Fri Dec 28 22:54:15 EST 2012

I've never been able to get this to work with arbitrary predicates.


#lang typed/racket

(: divisible-by-three? (Integer -> Boolean))
(define (divisible-by-three? n)
   (zero? (modulo n 3)))

(declare-refinement divisible-by-three?)
(define-type Div3 (Refinement divisible-by-three?))

Type Checker: cannot declare refinement for non-predicate Nothing in: 
(Refinement divisible-by-three?)


I've thought of using this for a matrix type, by defining them as 
non-empty, two-dimensional arrays, but never got past the experimental-ness.

Neil ⊥

On 12/28/2012 08:04 PM, Ray Racine 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.racine at gmail.com
> <mailto:ray.racine at 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.racine at gmail.com
>     <mailto:ray.racine at 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 <cce at ccs.neu.edu
>         <mailto:cce at 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.racine at gmail.com <mailto:ray.racine at 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.dobson at gmail.com
>                 <mailto:eric.n.dobson at 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.racine at gmail.com <mailto: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
>
>
>
>
>                 ____________________
>                    Racket Users list:
>                 http://lists.racket-lang.org/users
>
>
>
>
>
>
>
> ____________________
>    Racket Users list:
>    http://lists.racket-lang.org/users
>


Posted on the users mailing list.