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

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 ⊥