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

From: Sam Tobin-Hochstadt (samth at ccs.neu.edu)
Date: Tue Jun 26 22:19:18 EDT 2012

On Tue, Jun 26, 2012 at 9:36 PM, Robby Findler
<robby at eecs.northwestern.edu> wrote:
> The safety in this case doesn't generalize to contracts like the one
> Neil is suggesting when you go from an untyped value to a typed one,
> tho, right?

Right, if we have an untyped value which we'd like to give the
`case->` type that Neil described, we'd need to use a dependent
contract, as you suggested.  That's on the longer-term todo list.

For the typed->untyped case, when the arguments and results are all
first-order, the algorithm that Vincent uses for printing `case->`
types will also work for generating appropriate simpler contracts,
such as `(-> real? real?)`.

Sam

> Robby
>
> On Tue, Jun 26, 2012 at 8:32 PM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
>> Certainly the dependent contract approach will work, but the 'Real -> Real'
>> contract is also safe, so I'll see about generating that.
>>
>> Sam
>>
>> On Jun 26, 2012 8:37 PM, "Robby Findler" <robby at eecs.northwestern.edu>
>> 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


Posted on the dev mailing list.