[racket] typed racket: equivalent to Any for function types?

On Mon, Nov 28, 2011 at 11:05 AM, Ismael Figueroa Palet
<ifigueroap at gmail.com> wrote:
> Now my example typechecks, but effectively I can't do anything with the
> function :-( so it is very unpractical

There's no way to have a type that accepts all functions, and also
allows you to apply them to particular arguments.  What if that
function wasn't prepared to accept that argument?  What should happen
then?

> (: f ((Nothing -> Any) -> True))
> (define (f g) #t)
> (f (lambda: ([x : Integer]) #t))
>
> is there any way to make the typechecker happy, but being able to apply
> functions?
>
> For me, it would be something like:
>
> (: f ((Bottom -> True) -> True))
> (define (f g) (g 1))
> (f (lambda: ([x : Integer]) #t))

If this program type checked, then you could do this:

(f (lambda: ([x : String]) (string-append "a" x)))

and then you'd get a runtime error from `string-append'.  Those kind
of runtime errors are exactly what Typed Racket rules out.

> ?? or any other workaround?
> should I instead use an untyped module?

It really depends on what you're trying to do.  What would you want to
happen in the case of `string-append'?  Once you know what can happen
then, it's easier to figure out the right solution.

> 2011/11/28 Sam Tobin-Hochstadt <samth at ccs.neu.edu>
>>
>> On Mon, Nov 28, 2011 at 10:35 AM, Ismael Figueroa Palet
>> <ifigueroap at gmail.com> wrote:
>> > As Any is supertype of all values, what is the equivalent type for
>> > function
>> > types?
>> >
>> > (Any -> Any) does not work because of the contra-variant requirement of
>> > the
>> > argument.
>> >
>> > (: f ((Any -> Any) -> True))
>> > (define (f g) #t)
>> >
>> > (f (lambda (x) x) #t) ;; works
>> > (f (lambda: ([x : Integer]) #f)) ;; does not work
>> >
>> > The error is:
>> >
>> > Type Checker: Expected (Any -> Any), but got (Integer -> Any) in:
>> > (lambda:
>> > ((x : Integer)) #f)
>> >
>> > If I understand it correctly, the type I'm looking for is (Bottom ->
>> > Any),
>> > which satisfies the contra-variant and variant requirements for function
>> > subtyping. However, the Bottom type doesn't seem to exist (at least at
>> > the
>> > user-level, because I remember seeing some error messages that mentioned
>> > Top
>> > and Bottom).
>>
>> You're probably looking for the type `Nothing'.  Note that functions
>> of type `(Nothing -> T)' are very hard to apply, though.
>>
>> --
>> sam th
>> samth at ccs.neu.edu
>
>
>
> --
> Ismael
>
>



-- 
sam th
samth at ccs.neu.edu