I'm addicted to optimizations. If I use Real -> Real, TR can't prove
that (log1p 1.0) is Float and... hmm. I'll let Vincent explain why
that's bad. :)
Another option is to provide both log1p and fllog1p. I just wrote
fllog1p anyway.
Neil ⊥
On 06/26/2012 07:05 PM, Matthias Felleisen wrote:
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
