Now my example typechecks, but effectively I can't do anything with the function :-( so it is very unpractical (: 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)) ?? or any other workaround? should I instead use an untyped module? Thanks <div class="gmail_quote">2011/11/28 Sam Tobin-Hochstadt <<a href="mailto:samth@ccs.neu.edu">samth@ccs.neu.edu</a>> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div><div></div><div class="h5">On Mon, Nov 28, 2011 at 10:35 AM, Ismael Figueroa Palet <<a href="mailto:ifigueroap@gmail.com">ifigueroap@gmail.com</a>> 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). </div></div>You're probably looking for the type `Nothing'. Note that functions of type `(Nothing -> T)' are very hard to apply, though. -- sam th <a href="mailto:samth@ccs.neu.edu">samth@ccs.neu.edu</a> </blockquote></div> -- Ismael