It says that for all primes p, positive or negative, (next-prime p) will be an integer. Furthermore if p is a natural number, then (next-prime p) will also be a natural number.
This type can't be converted to a contract: Type Checker: The type of next-prime cannot be converted to a contract in: (next-prime 4)
My understanding is that a since N is a subset of Z a predicate can't determine whether which case to use. Is there an alternative construct, that I can use in order to get a contract?
My temporary solution is to provide untyped-next-prime
This has come up enough times that maybe TR should convert contracts of the form:
(case-> (-> <flat> ...) (-> <flat> ...))
into a dependent contract that checks the two 'flat' things? (I guess you'd have to have an ordering on types in case they overlap, but I presume you have this already.)
On Sat, Nov 17, 2012 at 1:18 PM, Jens Axel Søgaard
<jensa...@soegaard.net> wrote: > I have the following contract on next-prime :
> (: next-prime : (case-> (N -> N) (Z -> Z)) )
> It says that for all primes p, positive or negative, (next-prime p) > will be an integer. > Furthermore if p is a natural number, then (next-prime p) will also be > a natural number.
> This type can't be converted to a contract: > Type Checker: The type of next-prime cannot be converted to a > contract in: (next-prime 4)
> My understanding is that a since N is a subset of Z a predicate can't > determine whether > which case to use. Is there an alternative construct, that I can use > in order to get > a contract?
> My temporary solution is to provide untyped-next-prime
Its even simpler than that because the cases in case-> are ordered. There
are some intricacies when the first order checks of non flat contracts
overlap, but with non overlapping first order checks for higher order
contracts or only flat contracts it should be doable. I don't have a lot of
time for TR hacking currently, but if a bug is filed I may get to it at
some point.
On Nov 17, 2012 11:33 AM, "Robby Findler" <ro...@eecs.northwestern.edu>
wrote:
> This has come up enough times that maybe TR should convert contracts
> of the form:
> (case-> (-> <flat> ...) (-> <flat> ...))
> into a dependent contract that checks the two 'flat' things? (I guess
> you'd have to have an ordering on types in case they overlap, but I
> presume you have this already.)
> On Sat, Nov 17, 2012 at 1:18 PM, Jens Axel Søgaard
> <jensa...@soegaard.net> wrote:
> > I have the following contract on next-prime :
> > (: next-prime : (case-> (N -> N) (Z -> Z)) )
> > It says that for all primes p, positive or negative, (next-prime p)
> > will be an integer.
> > Furthermore if p is a natural number, then (next-prime p) will also be
> > a natural number.
> > This type can't be converted to a contract:
> > Type Checker: The type of next-prime cannot be converted to a
> > contract in: (next-prime 4)
> > My understanding is that a since N is a subset of Z a predicate can't
> > determine whether
> > which case to use. Is there an alternative construct, that I can use
> > in order to get
> > a contract?
> > My temporary solution is to provide untyped-next-prime
I've seen the first-order case come up a number of times, but not the higher-order one, so it may be best to be conservative and start there to see how it goes.
On Sat, Nov 17, 2012 at 2:09 PM, Eric Dobson <eric.n.dob...@gmail.com> wrote: > Its even simpler than that because the cases in case-> are ordered. There > are some intricacies when the first order checks of non flat contracts > overlap, but with non overlapping first order checks for higher order > contracts or only flat contracts it should be doable. I don't have a lot of > time for TR hacking currently, but if a bug is filed I may get to it at some > point.
> On Nov 17, 2012 11:33 AM, "Robby Findler" <ro...@eecs.northwestern.edu> > wrote:
>> This has come up enough times that maybe TR should convert contracts >> of the form:
>> (case-> (-> <flat> ...) (-> <flat> ...))
>> into a dependent contract that checks the two 'flat' things? (I guess >> you'd have to have an ordering on types in case they overlap, but I >> presume you have this already.)
>> On Sat, Nov 17, 2012 at 1:18 PM, Jens Axel Søgaard >> <jensa...@soegaard.net> wrote: >> > I have the following contract on next-prime :
>> > (: next-prime : (case-> (N -> N) (Z -> Z)) )
>> > It says that for all primes p, positive or negative, (next-prime p) >> > will be an integer. >> > Furthermore if p is a natural number, then (next-prime p) will also be >> > a natural number.
>> > This type can't be converted to a contract: >> > Type Checker: The type of next-prime cannot be converted to a >> > contract in: (next-prime 4)
>> > My understanding is that a since N is a subset of Z a predicate can't >> > determine whether >> > which case to use. Is there an alternative construct, that I can use >> > in order to get >> > a contract?
>> > My temporary solution is to provide untyped-next-prime
> It says that for all primes p, positive or negative, (next-prime p) > will be an integer. > Furthermore if p is a natural number, then (next-prime p) will also be > a natural number.
> This type can't be converted to a contract: > Type Checker: The type of next-prime cannot be converted to a > contract in: (next-prime 4)
> My understanding is that a since N is a subset of Z a predicate can't > determine whether > which case to use. Is there an alternative construct, that I can use > in order to get > a contract?
Vincent and I worked this out at the hackathon. There's now a very general but currently undocumented solution.
Most of the special functions have types that can't be converted to contracts. For example, the gamma function has the type
This could in principle be converted, but there are higher-order `case->' types in the math library that couldn't without running some serious theorem-proving. There probably always will be types that can't be converted to contracts, such types for functions that accept predicates (e.g. (Any -> Boolean : Real)).
I swear I will document this soon (it's on my TODO list!), but here's the general solution:
A Typed Racket module that imports `math/special-functions' will see gamma's original type, but its contract for untyped code is converted from the stated type (Real -> Real).
This should work for any type that TR can prove is a subtype of the original. Currently, `require/untyped-contract' can only be used in untyped Racket.
FWIW, this solution is only possible now that Racket has submodules.
The best place to use this is in "math/number-theory.rkt"... which I see is already using it for factorial and friends. You're all set.
Wouldn't it be better to use the dependent contract (when that works)? As an import to TR it definitely seems better, since it wouldn't be checking the right thing otherwise. (As an export from TR, I guess it doesn't matter.)
On Sat, Nov 17, 2012 at 2:18 PM, Neil Toronto <neil.toro...@gmail.com> wrote: > On 11/17/2012 12:18 PM, Jens Axel Søgaard wrote:
>> I have the following contract on next-prime :
>> (: next-prime : (case-> (N -> N) (Z -> Z)) )
>> It says that for all primes p, positive or negative, (next-prime p) >> will be an integer. >> Furthermore if p is a natural number, then (next-prime p) will also be >> a natural number.
>> This type can't be converted to a contract: >> Type Checker: The type of next-prime cannot be converted to a >> contract in: (next-prime 4)
>> My understanding is that a since N is a subset of Z a predicate can't >> determine whether >> which case to use. Is there an alternative construct, that I can use >> in order to get >> a contract?
> Vincent and I worked this out at the hackathon. There's now a very general > but currently undocumented solution.
> Most of the special functions have types that can't be converted to > contracts. For example, the gamma function has the type
> This could in principle be converted, but there are higher-order `case->' > types in the math library that couldn't without running some serious > theorem-proving. There probably always will be types that can't be converted > to contracts, such types for functions that accept predicates (e.g. (Any -> > Boolean : Real)).
> I swear I will document this soon (it's on my TODO list!), but here's the > general solution:
> A Typed Racket module that imports `math/special-functions' will see gamma's > original type, but its contract for untyped code is converted from the > stated type (Real -> Real).
> This should work for any type that TR can prove is a subtype of the > original. Currently, `require/untyped-contract' can only be used in untyped > Racket.
> FWIW, this solution is only possible now that Racket has submodules.
> The best place to use this is in "math/number-theory.rkt"... which I see is > already using it for factorial and friends. You're all set.
Yes. More automated is always better, for saving effort and reducing redundant annotations.
I see this in three ways:
* A stop-gap solution
* A last resort for types that can't be converted without importing Coq
* A way to squeeze better performance out of the typed/untyped boundary when it really counts
As an example of the last, `gamma' is exported to untyped code with the type (Real -> Real), when it could have the more specific type (Real -> (U Positive-Integer Flonum)), which has a slower contract check.
I don't know if performance "really matters" here, but I figured I'd consider it since I was already re-annotating.
> Wouldn't it be better to use the dependent contract (when that works)? > As an import to TR it definitely seems better, since it wouldn't be > checking the right thing otherwise. (As an export from TR, I guess it > doesn't matter.)
> Robby
> On Sat, Nov 17, 2012 at 2:18 PM, Neil Toronto <neil.toro...@gmail.com> wrote: >> On 11/17/2012 12:18 PM, Jens Axel Søgaard wrote:
>>> I have the following contract on next-prime :
>>> (: next-prime : (case-> (N -> N) (Z -> Z)) )
>>> It says that for all primes p, positive or negative, (next-prime p) >>> will be an integer. >>> Furthermore if p is a natural number, then (next-prime p) will also be >>> a natural number.
>>> This type can't be converted to a contract: >>> Type Checker: The type of next-prime cannot be converted to a >>> contract in: (next-prime 4)
>>> My understanding is that a since N is a subset of Z a predicate can't >>> determine whether >>> which case to use. Is there an alternative construct, that I can use >>> in order to get >>> a contract?
>> Vincent and I worked this out at the hackathon. There's now a very general >> but currently undocumented solution.
>> Most of the special functions have types that can't be converted to >> contracts. For example, the gamma function has the type
>> This could in principle be converted, but there are higher-order `case->' >> types in the math library that couldn't without running some serious >> theorem-proving. There probably always will be types that can't be converted >> to contracts, such types for functions that accept predicates (e.g. (Any -> >> Boolean : Real)).
>> I swear I will document this soon (it's on my TODO list!), but here's the >> general solution:
>> A Typed Racket module that imports `math/special-functions' will see gamma's >> original type, but its contract for untyped code is converted from the >> stated type (Real -> Real).
>> This should work for any type that TR can prove is a subtype of the >> original. Currently, `require/untyped-contract' can only be used in untyped >> Racket.
>> FWIW, this solution is only possible now that Racket has submodules.
>> The best place to use this is in "math/number-theory.rkt"... which I see is >> already using it for factorial and friends. You're all set.
