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" <i...@ccs.neu.edu> To: "Jordan Johnson" <j...@fellowhuman.com> Cc: users@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" <j...@fellowhuman.com> To: users@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 ____________________ Racket Users list: http://lists.racket-lang.org/users
