[racket] TR define-new-type, Value Types
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
>
![[logo]](/logo.png){kind=logo}