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

[Ray Racine]

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.

 

[Eric Dobson]

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

____________________
  Racket Users list:
  http://lists.racket-lang.org/users

[Ray Racine]

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.

[Carl Eastlund]

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

[Ray Racine]

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.

[Greg Hendershott]

> 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.

After reading Eric's post, and not finding much in the Racket docs, I
searched and found this:

http://www.ccs.neu.edu/racket/pubs/dissertation-tobin-hochstadt.pdf

Which I'd been reading until seeing more posts in this thread:

It's helpful but I can't get this example from it to work in TR:

#lang typed/racket

(: just-even (Number -> (Refinement even?)))
(define (just-even n)
(if (even? n) n (error 'just-even)))

(: halve ((Refinement even?) -> Number))
(define (halve n)
(/ n 2))

==>

Type Checker: Expected Integer, but got Number in: n
Type Checker: Expected (Refinement Integer even?), but got Number in: n

[Ray Racine]

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))

[Ray Racine]

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))

[Ray Racine]

Of course, now we all know who to thank, the *real* brain behind this outfit, thank you, Most Functional Man In The World.

[Carl Eastlund]

Stay functional, my friends.

(relayed on his behalf)

Carl Eastlund

[Neil Toronto]

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 ⊥

> <mailto:eric.n...@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.r...@gmail.com <mailto:ray.r...@gmail.com>>

[Ray Racine]

Ah, well ... arbitrary predicates ... certainly a desirable incremental improvement to the current feature set for refinement types.  

Bummer.