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

Stay functional, my friends.

(relayed on his behalf)

Carl Eastlund


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

> 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.racine at 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.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>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
>>>>>>
>>>>>>
>>>>>
>>>>
>>>
>>
>
> ____________________
>   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/1b1d1bfd/attachment-0001.html>