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

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.

Neil ⊥

On 11/17/2012 01:27 PM, Robby Findler wrote:
> 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