[racket] A type that can't be converted to a contract

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.toronto at 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
>
>   (: gamma (case-> (One -> One)
>                    (Integer -> Positive-Integer)
>                    (Flonum -> Flonum)
>                    (Real -> (U Positive-Integer Flonum))))
>
> 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:
>
>   (require typed/untyped-utils)
>
>   (require/untyped-contract
>    "private/functions/gamma.rkt"
>    [gamma  (Real -> Real)])
>
>   (provide gamma)
>
> 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.
>
> Neil ⊥
>
>
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users