<html><head/><body><html><head></head><body>Yes! This is exactly what I needed to know. (I suspected as much...my email earlier was in the midst of trying to figure out a huge type error I was getting (related to a bug report I sent in shortly after).) Thanks! Best, jmj -- Sent from my Android phone with K-9 Mail. <div class="gmail_quote">"J. Ian Johnson" <ianj@ccs.neu.edu> wrote:<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;"> <pre style="white-space: pre-wrap; word-wrap:break-word; font-family: monospace; margin-top: 0px">On a higher level note, if you're asking about the surrounding form for the @ 0, this is what is called a filter - meaning what type information do you learn if the output of the function tests to be non-false and likewise for false. (left of | is then branch info, right is else branch). If you test a number in an if, you will always go to the then branch. Thus in the then branch you just know that whatever was given to the function has the "not false" type. In the else branch you know the input has the "false" type. This is useless information in the number case, because Typed Racket already knows (Number @ 0) implies (! False @ 0). -Ian ----- Original Message ----- From: "Matthias Felleisen" <matthias@ccs.neu.edu> To: "Jordan Johnson" <jmj@fellowhuman.com> Cc: users@racket-lang.org Sent: Thursday, October 18, 2012 7:30:38 PM GMT -05:00 US/Canada Eastern Subject: Re: [racket] Meaning of "@" notation in TR To elaborate on Ian's answer, TR can't use 'x' from the function formals because x isn't in scope. So it has to use some other way of saying '0th' argument, '1st' '2nd' etc. On Oct 18, 2012, at 6:50 PM, Jordan Johnson wrote: <blockquote class="gmail_quote" style="margin: 0pt 0pt 1ex 0.8ex; border-left: 1px solid #729fcf; padding-left: 1ex;">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: <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a></blockquote> ____________________ Racket Users list: <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a> </pre></blockquote></div></body></html></body></html>