# [racket] Meaning of "@" notation in TR

 From: J. Ian Johnson (ianj at ccs.neu.edu) Date: Thu Oct 18 19:27:29 EDT 2012 Previous message: [racket] Meaning of "@" notation in TR Next message: [racket] A macro's `require' works in module but not in REPL Messages sorted by: [date] [thread] [subject] [author]

```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

```

 Posted on the users mailing list. Previous message: [racket] Meaning of "@" notation in TR Next message: [racket] A macro's `require' works in module but not in REPL Messages sorted by: [date] [thread] [subject] [author]