[racket] Meaning of "@" notation in TR

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 at ccs.neu.edu>
To: "Jordan Johnson" <jmj at fellowhuman.com>
Cc: users at 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:

> 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