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

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> 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> 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> 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>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>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
>>>
>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20121228/80e3f195/attachment-0001.html>