[racket] Meaning of "@" notation in TR

From: Jordan Johnson (jmj at fellowhuman.com)
Date: Thu Oct 18 22:07:19 EDT 2012

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).)


Sent from my Android phone with K-9 Mail.

"J. Ian Johnson" <ianj at ccs.neu.edu> wrote:

>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).
>----- 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
>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
>> (λ: ([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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20121018/0c4601ca/attachment.html>

Posted on the users mailing list.