Huh? On Jun 26, 2012, at 9:27 PM, Robby Findler wrote:
> Well, you wouldn't. Are the implementations of the contracts proven to > be equivalent currently? Or do you just have a theorem that matches up > the ones in some model somewhere? > > Robby > > On Tue, Jun 26, 2012 at 8:05 PM, Matthias Felleisen > <matth...@ccs.neu.edu> 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
