Question 1: Agner: A concurrency tracer
Concurrency bugs, including especially deadlocks and race conditions, are notoriously difficult to replicate and diagnose, even in otherwise well-behaved, message-oriented languages such as Erlang. The problem is that, when multiple concurrent threads are executing, the relative order of critical events may depend unpredictably on factors such as the compiler version, CPU load, number of cores available, and other factors that are not easy to vary, and that might still change in the future. For example, consider the Erlang top-level expression:
P = self(), spawn(fun () -> P ! a end), P ! b, receive X -> X end.
In most current implementations, this would probably evaluate to b every time it is run. However, if there had been more code between the spawn and the sending of b, such as some nontrivial computations, or just timer:sleep(1), the result would be likely to change to a. In even slightly more complicated examples it quickly becomes infeasible for humans to consider all the possible execution scenarios and verify that they all lead to an acceptable outcome.
However, because of the inherent simplicity and cleanliness of the Erlang concurrency model, and exploiting the expressive power of Haskell with monads, it is quite feasible to construct a usable concurrency tracer that systematically explores the consequences of various scheduling choices and enumerates the ultimate possible outcomes, including step-by-step scenarios of how each outcome could arise. This task is about implementing a simple such tracer named Agner.
An overview of the Agner language
The syntax and semantics of Agner are closely based on Erlang, though quite a bit simpler. Mostly, Agner programs will have the same meanings as in Erlang, but there are some important differences. This overview presupposes a working knowledge of Erlang.
The sequential core
Like Erlang, Agner is an evaluation-oriented language, with a single-assignment store. The following expression forms are available (the exact syntactic and lexical rules will be specified later):
Atoms An atom is either a simple identifier starting with a lowercase letter, such as hello, or an (almost) arbitrary sequence of characters enclosed in single quotes, such as ‘Hello, world!’. The quotes are not part of the atom name, so that ‘hello’ and hello denote exactly the same atom. Atoms evaluate to themselves.
Variables Variables are simple identifiers starting with an uppercase letter or underscore. A variable can have a current value in the store, in which case it will evaluate to that value; or it can be unbound, in which case evaluating it signals an exception
程序代写 CS代考 加微信: cstutorcs
{badvar, ‘X’}, where X is the name of the variable. (In Agner, unlike in Erlang, unbound variables are detected only at runtime, rather than before execution.) Variables get values by pattern-matching (see below); once a variable has a value, that value cannot change.
Tuples A tuple expression is a comma-separated, possibly empty, sequence of expressions, enclosed in curly braces, such as {foo,X,{}}. Like in Erlang, such an expression simply evaluates to the tuple of values that its elements evaluate to.
Lists A list expression is either [] or of the form [Exp1 | Exp2]. Like in Erlang, the generalized form [Exp1, …, Expn] is syntactic sugar for
[Exp1 | [Exp2 | … [Expn | []]]] and [Exp1, …, Expn | ExpT] for
[Exp1 | [Exp2 | … [Expn | ExpT]]]
(As usual there is no requirement that ExpT must evaluate to a list.) In Agner, unlike in Erlang, lists are actually not a separate data type, but just an abbreviation, with [] representing the atom ‘[]’, and [Exp1 | Exp2] representing the tuple
{‘[|]’, Exp1, Exp2}. For example, [a] is just a more convenient notation for {‘[|]’, a, ‘[]’}.
Patterns and matches A pattern, like in Erlang, is a restricted expression built out of atoms, variables, and tuples (with list-notation desugared like for expressions). Additionally, the wildcard pattern _ acts like an anonymous variable (with each occurrence distinct). For example, {a, X, [H|_]} is a pattern. Also like in Erlang, and unlike in Haskell, a variable may occur multiple times in a pattern, as in {X,X}.
A match expression is of the form Pat = Exp. When evaluated, it evaluates Exp to a value and checks that that this value is of the shape described by the pattern, possibly binding variables occurring in the pattern. It also returns the value. For example,
{a, X, [H|_]} = {a, b, [foo, bar, baz]} will succeed and bind X to b and H to foo. If the pattern does not match the value, the exception {badmatch,V} is thrown, where V is the value that the expression evaluated to
If variable in the pattern is already bound, the value it would be (re)bound to must be
the same as its current value. For example, after X = a, the pattern {X,b} matches {a,b}, but not {c,b}. In particular, {X,X} = {Exp1,Exp2} (where X is previously
unbound), succeeds if and only if Exp1 and Exp2 evaluate to the same value. Sequences A sequence expression, often referred to as a body, is of the form
Exp1, …, Expn
(where 𝑛 ≥ 1). It evaluates all of the expressions in turn (possibly binding variables in matches), and returns the value of the last one. (If any of the expressions signal an exception, any bindings are undone.). An expression sequence can appear anywhere in an expression by enclosing it as begin Exp1, …, Expn end, but many places in the grammar also allow sequencing without an explicit begin.
Note that in Agner, unlike in Erlang, it is explicitly specified that all subexpressions
within a single expression are also evaluated from left to right. This means that, e.g., {X=a,X} evaluates to {a,a}, while {X,X=a} signals that X is unbound. (In Erlang,
both expressions are statically illegal.) Case analysis A case expression is of the form
case Exp of Pat1 -> Body1; …; Patn -> Bodyn end
(Erlang’s case guards are not supported.) Like in Erlang, first Exp is evaluated to a value V, which is then matched against all the patterns in turn. If V matches some Pati (possibly binding some variables), the corresponding Bodyi is evaluated and its result becomes the result of the case-expression. (Any variables bound by the expression, pattern-match, or body also remain bound after the case-expression.) If none of the patterns match, the case-expression signals the exception {badcase,V}.
In Erlang, variables bound by a Bodyi are in general not available after the case- expression, unless they are bound by all the cases. (Variables that fail this check are called unsafe, and cause compilation to fail.) Agner, which only detects unbound variables at runtime, imposes no such restrictions.
Functions A function call is an expression of the form Exp0(Exp1,…,Expn), where 𝑛 ≥ 0. Agner, like Erlang (and most other languages, except Haskell), has an eager semantics, so first all of the expressions are evaluated (from left to right), and then the function that Exp0 evaluates to is applied to the list of argument values.
Like in Erlang, there are two kinds of functions in Agner, named and anonymous. For the former, if Exp0 evaluates to (usually, is already) an atom f, the program must contain a declaration of a function with that name, of the form,
f(X1, …, Xn) -> Body.
Then the formal parameters (the X’s) are bound to the values of the corresponding actual parameters, the function body is evaluated, and its result becomes the result of the function call. Function declarations may be (mutually) recursive, as usual, and the functions may be declared in any order.
Note that, unlike in Erlang, there can only be a single clause in a function declaration, rather than a collection of ;-separated ones. Consequently, the function parameters must also be simple variable names, not more general patterns. Likewise, all the parameter names must be distinct in Agner; this is considered a syntactic restriction. Erlang’s multiple-clause functions can expressed, slightly more verbosely, by explicit case-expressions; for example, the Erlang function declaration
equal(X,X) -> true; equal(_,_) -> false. could be written in Agner as
equal(X,Y) -> case X of Y -> true; _-> false end.
Agner, like Erlang (and Haskell) is statically scoped. This means that any variables bound at the place where the function is called are not available in the function body. For example, with the declaration
foo(X) -> Z = {X,X}, Z.
the expression (sequence) Z = a, X = b, foo(c) will still evaluate to {c,c}, despite the seemingly conflicting binding for Z. Conversely, in foo(c), {X,Z}, the caller’s X and Z will remain unbound after the call, unless they already had values.
Unlike in Erlang, a named function can only have a single arity; that is, there cannot be declarations for both foo(X) -> … and foo(X,Y) -> … in the same program. Also, there are no modules, so all declared functions live in the same name space, shared with the built-in functions (BIFs). (However, there is a lexical hack for : that allows for better source-level compatibility with Erlang; see later.)
If the number of actual parameters in a function call does not agree with the number of formal parameters in the declaration, the exception {badarity, F} is signaled, where F is the function name. If the atom F is not declared as a function all, the exception will instead be {undef, F}. If F is neither an atom nor an anonymous function value, the exception is {badfun, F}.
The second kind of functions are the anonymous function values, produced by function expressions, fun (X1, …, Xn) -> Body end. Calling an anonymous function is very similar to calling a named one; for example,
F = fun(X) -> {X,X} end, F(a).
would evaluate to {a,a}. There is, however, a subtlety in that – again in accordance with static scoping – variables that are already bound at the place where the function- expression is evaluated (not where the resulting functional value is later called) are also available in the function body. For example,
F = fun(X) -> fun (Y) -> {X,Y} end end, G = F(a), G(b).
would evaluate to {a,b} in both Erlang and Agner. Note that formal parameters
always shadow any existing variables of the same name, so that
X = a, F = fun(X) -> X end, {F(b), X}.
evaluates to {b,a} as expected. However, other variables, even if they are seemingly “defined” in the function body by the pattern-matching syntax, may clash with already
existing bindings, so that (like in Erlang),
Y = a, F = fun(X) -> Y = X, {X,Y} end, F(b).
would actually signal a match exception. (But had the final call been F(a), the result
would still be {a,a}).
Functional values always compare as equal to themselves. For example,the match in F = fun(X) -> X end, F = F. would always succeed. It is unspecified whether two function values produced by different evaluations of identical or similar function expressions compare as equal. For example all of these may succeed or fail:
F = fun(X) -> X end, G = fun(X) -> X end, F = G.
F = fun(X) -> X end, G = fun(Y) -> Y end, F = G.
F = fun(X) -> X end, D = a, G = fun(X) -> X end, F = G.
Exceptions Unlike Erlang, Agner does not distinguish formally between various excep- tion classes, such as errors or thrown exceptions. Any Agner value (though usually an atom or a tuple starting with an atom) can be signaled as an exception using the BIF throw, e.g, throw({myErr,{X,Y})) (where X and Y are already bound). Likewise, many runtime errors also signal specific exceptions, as mentioned above. Unless it is caught, an exception aborts evaluation of the entire expression.
Exceptions are caught by try-expressions, with syntax
try Body0 catch Pat1 -> Body1; …; Patn -> Bodyn end
Like in Erlang, first Body0 is evaluated, and if this succeeds (i.e., does not signal an exception), the result becomes the result of the whole try (and the handler cases are ignored). But if Body0 signals an exception, the exception value is matched against the patterns in turn (just like in a case-expression), and if a match succeeds, the corresponding handler body is evaluated. (Any exceptions thrown by the handler are not themselves caught by this try, but may be handled by an outer one.) If none of the patterns match, the exception propagates to any enclosing handlers, or ultimately to the top level of the expression.
If any variables were bound by Body0 before the exception was signaled, those bindings are undone; but any bindings existing before the try are kept. For example, after
X = a, try Y = b, throw(e) catch e -> Z = c end. X will be bound to a and Z to c, but Y will be unbound.
The sequential subset of Agner is a reasonably expressive functional language in its own right. The main difference from Erlang is the lack of any significant library of functions such as lists:map; however, such functions can easily be defined explicitly using pattern- matching and recursion. Likewise, but with more effort, rudimentary integer arithmetic could be coded as a library, either using an unary representation, e.g, representing 3 as
{{{{}}}}, or – far more efficiently – as a list of bits, such as [one,one]. However, the real interest of Agner is of course in the concurrency features, described next.
Concurrency
Agner shares Erlang’s basic concurrency model: a concurrent system consists of a collection of processes that communicate only by sending messages to each other. Each process has an incoming message queue, and once delivered to the queue, all messages will be processed in the order in which they were delivered. Also, a process may selectively receive only messages of a certain form, as specified by patterns. The additional expression forms and BIFs relating to concurrency are as follows:
Process spawning The BIF spawn(F), where F is either a named or an anonymous function of arity 0, starts a new process computing F(). The ultimate value (or thrown exception) computed like this is discarded, but while it is running, the process may engage in communication with other processes. The spawn call returns the
pid (process id) of the newly spawned process. A pid is a special value that can be bound to variables and tested for equality against other values, but that cannot be otherwise constructed. A pid is guaranteed to be distinct from any other pid issued in the same run of the program (i.e. a pid is not reissued even if the process it originally referenced has died.)
In Agner, pids have a user-readable representation as sequences of numbers
have no semantic significance (such as linking or supervision). Also, it is not possible
to “forge” a pid as a suitably named atom, as in ‘<1.2>‘ ! a.
Message send A send expression has the syntax ExpP ! ExpM. Here, ExpP must evaluate to a 𝑃 that is a (possibly defunct) pid (otherwise, {badpid, P} is signaled), while ExpM can evaluate to any Agner value 𝑀. 𝑀 is delivered to to the message queue of the process 𝑃, if it is still alive; otherwise the message is just discarded. Messages sent by a process are delivered in the same order in which they were sent, but if two different processes are sending to the same pid, it is unspecified which one gets delivered first. In particular, there are no inherent fairness guarantees (e.g., in a denial-of-service scenario, where one process is uninterruptedly sending messages to a single pid, any other sends to that pid may never get through.)
Message receive A receive expression is more involved, having the form receive Pat1 -> Body1; …; Patn -> Bodyn end
Like for case-expressions in Agner, there are no guards, nor is possible to specify an after (i.e., timeout) case.
The semantics of the expression is that the process first sleeps until its message queue becomes non-empty. Then, it takes the first message from the queue and matches it against all the patterns in turn, like for a case. But if none of the patterns match, the message is not immediately put back on the queue, since trying to match it again against the same patterns would be pointless. Instead, the message is stashed in an internal list inside the process, and the next message from the incoming queue is examined. (If the queue has become empty, the process goes back to sleep.) Once a message is received that matches one of the patterns, the process first unstashes its internal list back unto the front of the message queue (preserving the original order), so that the next receive-expression will examine all the messages again from the oldest one.
Self-identification A process can find out its own pid (tyically to give it to someone else) by the BIF self().
Logging Afinal,Agner-specificBIF(butroughlycorrespondingtoErlang’s.io:format/2, when used for debugging information, though without any actual formatting func- tionality) is log(V) where V can be an arbitrary value. This adds adds (a textual representation of) V to the end of an event log that can be printed once the program stops (whether normally or by a deadlock). Also, the Agner system itself is allowed to add its own messages to the log; such messages will be specially tagged so as not to interfere with the user’s. The log function always returns the atom ok.
Log entries produced by the same process are recorded in the order in which they are made, but messages from different processes that are not causally related may be arbitrarily interleaved.
For simplicity, Agner does not support preemptive multi-threading: a well-behaved process is expected to eventually perform a send or receive, at which time a different process may be scheduled. Thus, processes spinning in a tight loop may cause the whole system to grind to a halt. Also, “fork bombs” (i.e., a process spawning unbounded numbers of subprocesses), like infinite recursion, are not handled gracefully in the basic version.
We can use the system to run the example from the introduction
$ agner “P = self(), spawn(fun () -> P ! a end), P ! b, receive X -> X end.” ===== result : value b (with deterministic scheduler)
This (coincidentally) agrees with the standard Erlang implementation. However. we can also explore the space of possibilites using the backtracking scheduler, which systematically tries all possible interleavings of runnable processes:
$ agner -bt “P = self(), spawn(fun () -> P ! a end), P ! b, receive X -> X end.” ===== result : value b (1 scenarios)
===== result : value a (1 scenarios)
If it seems puzzling how some of the final results can arise, we can ask the system to print out its detailed event log leading to a particular outcome. (If there are multiple ways to reach a particular result, only one, representative, scenario is shown.)
$ agner -sl -bt “P = self(), spawn(fun () -> P ! a end), P ! b, receive X -> X end.” ===== result : value b (1 scenarios)
system: Process <> spawning process <0>
system: selecting #1 of 2 ready processes
system: process <> sending b to self
system: Process <> inspecting b
system: Process <> unstashed 0 messages
system: Process <> terminated with value b
system: finished!
===== result : value a (1 scenarios)
system: Process <> spawning process <0>
system: selecting #2 of 2 ready processes
system: process <0> sending a to ready <>
system: Process <0> terminated with value a
system: process <> sending b to self
system: Process <> inspecting a
system: Process <> unstashed 0 messages
system: Process <> terminated with value a
system: finished!
浙大学霸代写 加微信 cstutorcs
Note that the actual contents of the system log is not specified; you can be as chatty or silent as you prefer, and the exact phrasing of particular events is also entirely up to you.
For a slightly larger example, we may define some helper functions to be used in the top- level expression. We also select a Monto-Carlo scheduler that makes random scheduling choices. (Newlines are added in the command line for readabilty):
$ agner -mc 1000
-p “r() -> receive X -> X end.
ss(P,X) -> spawn (fun () -> P ! X end).”
“P = self(), ss(P,a), ss(P,b), ss(P,c), {r(), r(), r()}.”
===== result : value {b,a,c} (163 / 1000 scenarios)
===== result : value {a,b,c} (173 / 1000 scenarios)
===== result : value {b,c,a} (183 / 1000 scenarios)
===== result : value {c,a,b} (169 / 1000 scenarios)
===== result : value {c,b,a} (157 / 1000 scenarios)
===== result : value {a,c,b} (155 / 1000 scenarios)
Running the tool with no arguments gives a brief usage summary.
The Agner implementation
The Agner system is divided into 4 main modules (as well as a couple of extra ones, containing shared type definitions and the like), as follows:
• TheParserreadsintheconcretesyntaxofAgnerprogramsandtop-levelexpressions into abstract syntax trees.
• The Evaluator handles the sequential part of the language, It also contains part of the support for the concurrency-related features with significant syntax-related aspects, specifically receive-expressions.
• TheSchedulerprovidesthemainsupportfortheconcurrentfeaturesofthelanguage. It orchestrates the sequential evaluation of expressions in the individual processes, as well as handling the communications aspects. It also allows various scheduling choices to be explored.
• Themainprogram,whichcontainsthetop-levelstand-alonetool(includingcommand- line option processing, file I/O, log filtering, and the like).
The main program is already provided, so your task is to implement the remaining three modules, according to the detailed specifications in the following. The sections are weighted roughly as indicated below; but as always, the exam is graded as a whole, and the various modules demonstrate complementary skills.
Program ::= epsilon
| FDecl Program
FDecl ::= atom “(” Varz “)” “->” Body “.”
Top ::= Body “.”
Exp ::= atom
| “(” Exp “)”
| “{” Expz “}”
| “[” ExpL “]”
| Pat “=” Exp
| “begin” Body “end”
| “case” Exp of Cases “end”
| Exp “(” Expz “)”
| “fun” “(” Varz “)” “->” Body “end”
| “try” Body “catch” Cases “end”
| Exp “!” Exp
| “receive” Cases “end”
Pat ::= atom
| “(” Pat “)”
| “{” Patz “}”
| “[” PatL “]”
Cases ::= Case
| Case “;” Cases
Case ::= Pat “->” Body
Body ::= Exps
Expz ::= epsilon
Exps ::= Exp
| Exp “,” Exps
ExpL ::= epsilon
| Exps “|” Exp
Patz ::= epsilon
Pats ::= Pat
| Pat “,” Pats
PatL ::= epsilon
| Pats “|” Pat
Varz ::= epsilon
Vars ::= var
| var “,” Vars
Figure 1: Concrete grammar of Agner
CS Help, Email: tutorcs@163.com
Question 1.1: The Parser (40%)
The concrete syntax of Agner programs is given in Figure 1 (in a notation similar to the parser notes). This grammar is supplemented with the following stipulations:
Disambiguation the operators “=” and ”!” have the same precedence and are right- associative. Function calls have higher higher precedence than match and send, so that, e.g., self() ! self() parses as (self()) ! (self()). Also, slightly unusually for a functional language, function application is non-associative, so that f(a)(b) is illegal syntax; it must be written as (f(a))(b).
Complex lexical tokens An identifier atom is a non-empty sequence of (Unicode) letters, digits(0 through 9), underscores (_) and at-signs starting with a lowercase letter. The following Agner keywords are not allowed as identifiers: begin, case, catch, end, fun, receive, and try. Other Erlang keywords, such as after are allowed, though it may be prudent to avoid them.
For pseudo-compatibilty with Erlang, colons (:) are also allowed as identifier characters (similarly to @), so that one could directly declare and call, e.g., a utility function named lists:reverse.
Alternatively, a general atom is any (possibly even empty) sequence of characters, enclosed in single quotes (‘). If this sequence is to contain single-quote or a backslash (\) characters, they must be written as \’ and \\, respectively. The escape sequences \n and \t stand for a newline and tab character; all others stand for just the second character. The outer quotes are not included in the atom name.
The rules for variable names var are the same as for identifier atoms (including the special inclusion of :, except that the first character must now be an uppercase letter or an underscore. (However, it cannot consist of only an underscore, since that is reserved for the wildcard pattern.) There is no analog of the general-atom syntax for variables.
Whitespace and comments Tokens may be surrounded by arbitrary whitespace, which is ignored, except for separating tokens that would otherwise run together, such as consecutive identifiers, variables, and keywords. Comments start with a percent sign (%) and run until the following newline (or end of file). Comments also act as whitespace for token separation.
The abstract syntax is defined in file AST.hs:
data Exp =
EAtom AName
| EVar VName
| ETup [Exp]
| EMatch Pat Exp | ESeq Exp Exp
| ECase Exp Cases | ECall Exp [Exp]
| EFun [VName] Exp | ETry Exp Cases
| ESend Exp Exp
| EReceive Cases
data Pat =
PAtom AName
| PVar VName | PTup [Pat] | PWild
type Cases = [(Pat, Exp)]
type AName = String atomNil = “[]” atomCons = “[|]”
type VName = String
data FDecl = FDecl AName [VName] Exp type Program = [FDecl]
The correspondence between the concrete and abstract syntax should be largely straight- forward. Note, however, that there is no separate AST type corresponding to Body; instead, commas used for sequencing correspond to the ESeq constructor.
The Parser should export two functions, corresponding to the two possible start symbols of the grammar:
parseProgram :: String -> Either String Program
parseTop :: String -> Either String Exp
Note that the parsing functions should also check that all functions are well formed, i.e., that there are no repeated variable names in a formal-parameter list.
For implementing your parser, you may use either the ReadP or the Parsec combinator library. If you use Parsec, then only plain Parsec is allowed, namely the following submod- ules of Text.Parsec: Prim, Char, Error, String, and Combinator (or the compatibility modules in Text.ParserCombinators.Parsec); in particular you are disallowed to use Text.Parsec.Token, Text.Parsec.Language, and Text.Parsec.Expr. As always, don’t worry about providing informative syntax-error messages if you use ReadP.
With ReadP’s lack of error messages, it may be a bit challenging to track down the location of syntax errors in large programs. However, since Agner syntax is very close to Erlang, you may be able to use the standard Erlang compiler on the failing file to see where the error is.
Question 1.2: The Evaluator (35%)
The evaluation model of Agner is value-oriented, where a value is given by the following datatype (in Runtime.hs):
data Value =
VAtom AName
| VTup [Value]
| VClos Env [VName] Exp | VPid Pid
type Env = [(VName,Value)] type Exn = Value
mkExn s v = VTup [VAtom s, v] type Outcome = Either Exn Value
The meanings of the constructors VAtom, VTup, and VPid should be obvious. VClos is a function closure, used for functional values. It consists of the formal parameters and body of the function expression, together with a copy of the environment at the time the function-expression was evaluated. An environment is simply a list of variables and their corresponding values, if any; unbound variables are not mentioned. As usual, only the first occurrence of a variable in the list matters.
Finally, an Agner exception is simply a value; we also define a convenience function for constructing exception values in the standard format. Outcome is a convenient abbreviation for the final result of an evaluation.
(The file also includes a simple pretty-printer showV for rendering values in a more readable form. To avoid potential confusion, it is not used as the default Show instance. The concurrency-related definitions in Runtime will be discussed later.)
The central type definition in the Evaluator is the Eval monad:
newtype Eval a = Eval {runEval :: FEnv -> Env -> Req (Either Exn (a, Env))} type FEnv = [(AName, (Int, [Value] -> Eval Value))]
An Eval-computation may draw upon a number of features of the evaluation context. First, it has Reader-like access to the function environment, in which all available named functions (both program-defined and built-in) are defined. The environment binds each such function name to a tuple of the function’s arity and the function itself, represented as taking a list of argument values, and returns (a computation of) the result value.
Second, an Eval computation receives the current (value) environment, as previously mentioned. Since expression evaluation may add bindings to the environment (using the match-operator =), the updated environment is also returned together with the (successful) computation result.
Since evaluation may fail, the result is actually an Either-type, with the left alternative being a thrown exception. Note that no updated environment is returned in this case; rather, the set of available bindings is rolled back to what it was when the failing computation was started in a try-expression.
Finally, the entire computation is performed in the Req monad, a generalization of the SimpleIO monad from the lectures. It is used only by the concurrency features discussed later; so for now, you may think of Req as simply the identity monad.
Your first (minor) task is to complete the Monad instance for Eval. This should not depend on what Req is, but merely that it is some monad.
Next, as usual, we define the operations accessing the features of the monad:
askFEnv :: Eval FEnv
getVar :: VName –