How can I use define/contract (or something equivalent) in Typed Racket?

3
votes

I am writing a function that accepts only positive numbers, and I want to ensure that it is used correctly both inside the module and elsewhere.

I wanted to write

#lang typed/racket
(require racket/contract)

(: excited-logarithm (-> Number Number))
(define/contract (excited-logarithm ([x : Number]) : Number)
  (-> (>=/c 0) number?)
  (displayln "Hold on to your decimals, we're going in!")
  (log x))

but Typed Racket doesn't provide its own define/contract, and vanilla define/contract doesn't understand Typed Racket's annotations (it throws a syntax error).

Can I work around this somehow? Can I use bare contract to attach a contract to excited-logarithm the way define/contract would?

Moreover, is there a good reason I shouldn't be doing this? Is mixing contracts and types discouraged?

Note: I suppose what I really want here is dependent typing, but that's not available in Racket.

1
racketcontracttyped-racket

1 Answers

2
votes

Simple answer here: use the type "Nonnegative-Real", or one of the other similar TR Types that capture this idea.

http://docs.racket-lang.org/ts-reference/type-ref.html?q=Positive-Real#%28form._%28%28lib.typed-racket%2Fbase-env%2Fbase-types..rkt%29..Positive-.Real%29%29

(There are also refinement types, but you don't need them, here.)