2.7.7.2 Note

This operation allows arbitrary information or comments to be embedded in a virtual code application in such a way that it will be ignored by avram when executing it. For the silly language, a note function is defined in the standard prelude so as to imply the following theorem.

T11

[[note]] (f,c) = ((nil,nil),((nil,nil),(nil,(nil,(f,c)))))

Intuitively, the argument f represents a function, and the argument c represents the comment, annotation, or whatever, that will be embedded but ignored in the virtual code.

Semantically, a function with a note attached is the same as the function by itself, as the following property stipulates for any non-nil f.

P8

([[note]] (f,c)) x = f x

A possible reason for using this feature might be to support a language that performs run-time type checking by hanging type tags on everything. Another possible use would be to include symbolic information needed by a debugger.

This document was generated on November 8, 2012 using texi2html 1.82.