gradual-refinement-type-example.rkt

#lang racket/base

(module typed typed/racket/base
  (provide double)
  (define-type Increasing (([n : Natural]) . → . (Refine [a : Natural] (> a n))))
  (: double : Increasing → Increasing)
  ;; Modular type-checking of this module cannot eliminate:
  ;; - `(Refine [a : Natural] (> a n))` in `f`'s range
  ;; - `Natural` in `n`
  (define ((double f) n) (f (f n))))

(module untyped racket/base
  (require (submod ".." 'typed))
  (provide/contract [add2 (integer? . -> . integer?)])
  (define add2 (double add1)))