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

From: Greg Hendershott (greghendershott at gmail.com)
Date: Fri Dec 28 21:27:48 EST 2012

> 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

Posted on the users mailing list.