I'm saying that people can make mistakes in Racket currently that undermine the guarantees of the type system. But lets continue the other line first.
On Tue, Jun 26, 2012 at 8:28 PM, Matthias Felleisen <matth...@ccs.neu.edu> wrote: > > 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
