[racket] Meaning of "@" notation in TR

It occurs to me that explanation might be a bit too assuming.

I messed that up. The 0 is referring to which formal (function argument) the filter is about. Since x is the first (and only) formal of this function, 0 refers to it.

Were you to write
(lambda: ([x : Number] [y : Number]) y)

then you would get @ 1 in the filter's output. The (0) at the end (in your type) is referring to which actual value is returned. This allows Typed Racket to track equalities somewhat.
-Ian
----- Original Message -----
From: "J. Ian Johnson" <ianj at ccs.neu.edu>
To: "Jordan Johnson" <jmj at fellowhuman.com>
Cc: users at racket-lang.org
Sent: Thursday, October 18, 2012 7:18:01 PM GMT -05:00 US/Canada Eastern
Subject: Re: [racket] Meaning of "@" notation in TR

This is a DeBruijn index for the binding of the type parameter.
-Ian
----- Original Message -----
From: "Jordan Johnson" <jmj at fellowhuman.com>
To: users at racket-lang.org
Sent: Thursday, October 18, 2012 6:50:46 PM GMT -05:00 US/Canada Eastern
Subject: [racket] Meaning of "@" notation in TR


Hi all, 


I'm puzzled by this cryptic notation in Typed Racket (copied from the docs): 


( λ: ( [ x : Number ] ) x ) 


- : (Number -> Number : ((! False @ 0) | (False @ 0)) (0)) 




What does the "@ 0" mean? I have searched all of the TR doc pages, but I see no explanation. 


Thanks, 
jmj 


____________________
  Racket Users list:
  http://lists.racket-lang.org/users

____________________
  Racket Users list:
  http://lists.racket-lang.org/users