[racket-dev] math collection [was: Hyperbolic functions]

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
<matthias at 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
>> <matthias at 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.toronto at 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
>>>
>