understanding the 'this' keyword in Alloy

Question

In the following code from section 4.7.2 of the Alloy book, what does the this keyword refer to?

module library/list [t]
sig List {}
sig NonEmptyList extends List {next: List, element: t} 

...

fun List.first : t {this.element} 
fun List.rest : List {this.next} 
fun List.addFront (e: t): List {
    {p: List | p.next = this and p.element = e} 
}

I would appreciate if you give me an elaborate description of this usage in Alloy.

Answer 1

Section 4.5.2 of Software Abstractions describes (among other things) what it calls the 'receiver' convention, that is the syntactic shorthand of writing functions and predicates as

fun X.f[y : Y, ...] { ... this ... }

instead of

fun f[x : X, y : Y, ...] { ... x ... }

That is, the declaration

fun List.first : t {this.element} 

is equivalent to (and shorthand / syntactic sugar for)

fun first[x : List] : t {x.element} 

And similarly for the other examples you give. The parallel would be even stronger if we said the long form was

fun first[this : List] : t {this.element} 

but while this is a useful illustration, it's not legal: this is a keyword and cannot be used as an ordinary variable name.

---

You ask for an "elaborate description" of the usage of this in Alloy. Here's a survey. The keyword this can be used in the following situations:

• In declarations and signature facts, this acts as a variable implicitly bound to each instance of the signature. So a declaration of the form

  sig Foo { ... } { copacetic[this] }
  

  is equivalent to

  sig Foo { ... }
  fact { all f : Foo | copacetic[f] }
  

• In declarations and signature facts, every reference to a field f declared or inherited by the signature is implicitly expanded to this.f, where this is implicitly bound as described above, unless the reference is prefixed with @. The example at the end of 4.2.4 illustrates the semantics.

• In the declaration bodies of functions and predicates declared using the 'receiver' convention, the keyword this acts as a variable implicitly bound to the first argument of the function or predicate. The example at the end of 4.5.2 illustrates this, as does the example cited here by the OP.

  The 'receiver' convention is defined in section B.7.5 of the language reference.

All of these are pointed to from the entry for this in the index of Software Abstractions; for more information, read the relevant passages.