How would you check soundness between a type and its contract? Types, like theorem provers, are addictive. The more expressivity they provide, the more programmers want to play with them.
Use Real -> Real and you'll be fine. -- Matthias On Jun 26, 2012, at 8:37 PM, Robby Findler wrote: > In this case, the contract could turn into a dependent one with the > same semantics. Does it make sense for TR to allow a user to declare > the equivalent contract? > > Robby > > On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto <neil.toro...@gmail.com> wrote: >> Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to >> have precise types. For example, log1p could have the type >> >> (case-> (Zero -> Zero) >> (Float -> Float) >> (Real -> Real)) >> >> It was easy to get the implementation to typecheck, but when I tried to plot >> it in untyped Racket, I got this: >> >> Type Checker: The type of log1p cannot be converted to a contract in: log1p >> >> I really don't want to have two versions of the library. Could TR use the >> most general type (Real -> Real) as the contract? Or would that be unsound? >> >> Neil ⊥ >> _________________________ >> Racket Developers list: >> http://lists.racket-lang.org/dev > > _________________________ > Racket Developers list: > http://lists.racket-lang.org/dev _________________________ Racket Developers list: http://lists.racket-lang.org/dev