doc/org.eclipse.xsemantics.doc/contents/Lambda-example.html

<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1" >
<title>Lambda</title>

<link href="book.css" rel="stylesheet" type="text/css">
<link href="code.css" rel="stylesheet" type="text/css">
<link rel="home" href="00-Main.html" title="">
</head>
<body>
<a name="Lambda"></a>
<h1>Lambda</h1>
<p>
From Wikipedia:
</p>
<p>
<em>"In mathematical logic and computer science, lambda calculus is a formal 
system for function definition, function application and recursion. 
The portion of lambda calculus relevant to computation is now called 
the untyped lambda calculus. In both typed and untyped versions, 
ideas from lambda calculus have found application in the fields of logic, 
recursion theory (computability), and linguistics, and have played an 
important role in the development of the theory of programming languages 
(with untyped lambda calculus being the original inspiration for 
functional programming, in particular Lisp, and typed lambda calculi 
serving as the foundation for modern type systems)."</em>
</p>
<p>
As another example of use of Xsemantics we also developed a prototype 
implementation of a lambda-calculus in XTEXT (we&apos;ll show the grammar in the following); 
in this lambda-calculus we can specify the type of the parameter of 
the abstraction, but we can also leave it empty; 
we can then infer the type of each lambda term. 
In particular, we infer types using type variables when 
the type of a term can be generic. 
The types of this lambda-calculus can be basic types 
(in this example integer or string), arrow types, and type variables 
(denoted by identifiers).
</p>
<p>
The challenging part in writing a type system for this language is 
that we need to perform <em>unification</em> in order to infer the <em>most general type</em>
(see, e.g., J. A. Robinson. Computational logic: The unification computation. 
Machine Intelligence, 6, 1971.).
</p>
<p>
Again, this is just a tutorial example, but this technique can be used 
to infer types in another language implemented in Xtext, 
especially for functional languages.
</p>
<a name="LambdaInANutshell"></a>
<h2>Lambda in a nutshell</h2>
<p>
You can think of lambda abstraction as a function definition 
(without a name), with a parameter (in this version we consider 
one single parameter) and a body, such as
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">lambda</span>&nbsp;x.&nbsp;x<br/>
</p>
</div>
</div>
</p>
<p>
which is the identity function (given an argument it returns the same argument). 
Lambda application, which corresponds to function invocation, is denoted 
without the parenthesis, thus if we have a lambda abstraction 
<span class="inlinecode">M</span> and an argument <span class="inlinecode">N</span> we write <span class="inlinecode">M&nbsp;N</span> to mean 
"invoke the function <span class="inlinecode">M</span> passing <span class="inlinecode">N</span> as the argument."
Of course, <span class="inlinecode">M&nbsp;N</span> is a well typed lambda term only if <span class="inlinecode">M</span>
is a function which takes as a parameter of a type <span class="inlinecode">T</span> and
<span class="inlinecode">N</span> is a lambda term with a type conformant to <span class="inlinecode">T</span>.
</p>
<p>
Both of the following definitions with an explicit type for 
the parameter are correct:
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">lambda</span>&nbsp;x&nbsp;:&nbsp;<span class="keyword">string</span>&nbsp;.&nbsp;x<br/>
<span class="keyword">lambda</span>&nbsp;x&nbsp;:&nbsp;<span class="keyword">int</span>&nbsp;.&nbsp;x<br/>
</p>
</div>
</div>
</p>
<p>
These two functions have types, respectively, 
<span class="inlinecode"><span class="keyword">string</span>&nbsp;-&gt;&nbsp;<span class="keyword">string</span></span> (given a string it returns a string) and 
<span class="inlinecode"><span class="keyword">int</span>&nbsp;-&gt;&nbsp;<span class="keyword">int</span></span>. Note that <em>arrow types</em> associate to the right, 
thus <span class="inlinecode">a&nbsp;-&gt;&nbsp;b&nbsp;-&gt;&nbsp;c</span> is to be intended as <span class="inlinecode">a&nbsp;-&gt;&nbsp;(b&nbsp;-&gt;&nbsp;c)</span>; otherwise, 
we must use parenthesis.
</p>
<p>
Indeed, we can be more general and say that the parameter 
<span class="inlinecode">x</span> can be "any" type, using a type variable (similar to Java generics):
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">lambda</span>&nbsp;x&nbsp;:&nbsp;a&nbsp;.&nbsp;x<br/>
</p>
</div>
</div>
</p>
<p>
This function then has type <span class="inlinecode">a&nbsp;-&gt;&nbsp;a</span>; note that since we return the 
argument as we received it, then the return type must be the same as 
the argument type, thus the type variable <span class="inlinecode">a</span> must be the same in <span class="inlinecode">a&nbsp;-&gt;&nbsp;a</span>.
</p>
<p>
In other cases, we cannot be generic; for instance, consider that in our 
language we have the unary operator <span class="inlinecode">-</span> which can be used on integers only. 
Then, the function
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">lambda</span>&nbsp;x&nbsp;.&nbsp;-x<br/>
</p>
</div>
</div>
</p>
<p>
imposes <span class="inlinecode">x</span> to be an integer, thus this function has type 
<span class="inlinecode"><span class="keyword">int</span>&nbsp;-&gt;&nbsp;<span class="keyword">int</span></span>.
</p>
<p>
Other functions can be partially generic, like the following one 
(which makes a little sense, it&apos;s used only as an example)
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">lambda</span>&nbsp;x&nbsp;.&nbsp;10<br/>
</p>
</div>
</div>
</p>
<p>
which has type <span class="inlinecode">a&nbsp;-&gt;&nbsp;<span class="keyword">int</span></span>.
</p>
<p>
We might also let the system infer the type 
(and that&apos;s what we intend to do with our type system definition).
</p>
<p>
For non trivial cases the type inference is more interesting than the 
examples we saw so far; for instance, consider this lambda abstraction
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">lambda</span>&nbsp;x&nbsp;.&nbsp;<span class="keyword">lambda</span>&nbsp;y.&nbsp;x&nbsp;y<br/>
</p>
</div>
</div>
</p>
<p>
which has type <span class="inlinecode">(a&nbsp;-&gt;&nbsp;b)&nbsp;-&gt;&nbsp;a&nbsp;-&gt;&nbsp;b</span>: how can this be inferred? 
Informally, <span class="inlinecode">x</span> cannot have any type, since in the body we read 
<span class="inlinecode">x&nbsp;y</span> then <span class="inlinecode">x</span> must be a function; for the moment we give it 
a generic type <span class="inlinecode">X1&nbsp;-&gt;&nbsp;X2</span>; what can the type of <span class="inlinecode">y</span> be? 
It can be a generic type, say <span class="inlinecode">X3</span>, but since we pass it to <span class="inlinecode">x</span> then 
it must have the same type of the argument of <span class="inlinecode">x</span>, thus we require 
<span class="inlinecode">X1</span> to be the same as <span class="inlinecode">X3</span>. The result of <span class="inlinecode">x&nbsp;y</span> will have 
the same type as the return type of <span class="inlinecode">x</span>, i.e., <span class="inlinecode">X2</span>. Thus, 
the above function has the following type: 
it takes an argument for the parameter <span class="inlinecode">x</span> of type <span class="inlinecode">X1&nbsp;-&gt;&nbsp;X2</span>, 
and it returns a function (the inner lambda abstraction) which takes 
an argument for the parameter <span class="inlinecode">y</span> of type <span class="inlinecode">X1</span> and returns 
something of type <span class="inlinecode">X2</span>. Thus, using different (and more readable)
type variable names, <span class="inlinecode">(a&nbsp;-&gt;&nbsp;b)&nbsp;-&gt;&nbsp;a&nbsp;-&gt;&nbsp;b</span> 
(we used the parenthesis since by default arrow types associate to the right). 
Again, the type variables make the function generic, provided 
that the same type is used for all occurrences of <span class="inlinecode">a</span> and the same 
type is used for all occurrences of <span class="inlinecode">b</span>.
</p>
<p>
<table>
<tr>
<td>
<span class="inlinecode"><span class="keyword">lambda</span>&nbsp;x&nbsp;.<span class="keyword">lambda</span>&nbsp;y.y&nbsp;x</span>
</td>
<td>
<span class="inlinecode">a&nbsp;-&gt;&nbsp;(a&nbsp;-&gt;&nbsp;b)&nbsp;-&gt;&nbsp;b</span>
</td>
</tr>
<tr>
<td>
<span class="inlinecode"><span class="keyword">lambda</span>&nbsp;f&nbsp;.(<span class="keyword">lambda</span>&nbsp;x.(f&nbsp;(f&nbsp;x)))</span>
</td>
<td>
<span class="inlinecode">(a&nbsp;-&gt;&nbsp;a)&nbsp;-&gt;&nbsp;a&nbsp;-&gt;&nbsp;a</span>
</td>
</tr>
<tr>
<td>
<span class="inlinecode"><span class="keyword">lambda</span>&nbsp;f&nbsp;.<span class="keyword">lambda</span>&nbsp;g.<span class="keyword">lambda</span>&nbsp;x.(f(g&nbsp;x))</span>
</td>
<td>
<span class="inlinecode">(a&nbsp;-&gt;&nbsp;b)&nbsp;-&gt;&nbsp;(c&nbsp;-&gt;&nbsp;a)&nbsp;-&gt;&nbsp;c&nbsp;-&gt;&nbsp;b</span>
</td>
</tr>
</table>
</p>
<p>
Note that there are functions which cannot be typed (at least with 
simple type systems we&apos;re used to), e.g.,
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">lambda</span>&nbsp;x&nbsp;.&nbsp;x&nbsp;x<br/>
</p>
</div>
</div>
</p>
<p>
cannot be typed, since <span class="inlinecode">x</span> should be a function, say with type 
<span class="inlinecode">a&nbsp;-&gt;&nbsp;b</span>, but since we apply <span class="inlinecode">x</span> to <span class="inlinecode">x</span> it should also be of 
type <span class="inlinecode">a</span>; however, <span class="inlinecode">a&nbsp;-&gt;&nbsp;b</span> and <span class="inlinecode">a</span> cannot be unified, 
since <span class="inlinecode">a</span> occurs in <span class="inlinecode">a&nbsp;-&gt;&nbsp;b</span>.
</p>
<a name="LambdaInXtext"></a>
<h2>Lambda implemented in Xtext</h2>
<p>
This is the grammar for our simple lambda calculus in Xtext:
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">grammar</span>&nbsp;org.eclipse.xsemantics.example.lambda.Lambda&nbsp;<span class="keyword">with</span>&nbsp;org.eclipse.xtext.common.Terminals<br/>
<span class="keyword">generate</span>&nbsp;lambda&nbsp;<span class="string">"http://xsemantics.sf.net/example/lambda/Lambda"</span><br/>
<br/>
Program:&nbsp;term=Term;<br/>
<br/>
<span class="comment">//&nbsp;left&nbsp;associative<br/>
</span>Term:&nbsp;TerminalTerm&nbsp;(=&gt;({Application.fun=<span class="keyword">current</span>}&nbsp;arg=TerminalTerm)*)&nbsp;;<br/>
<br/>
TerminalTerm&nbsp;<span class="keyword">returns</span>&nbsp;Term:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="string">&apos;(&apos;</span>&nbsp;Term&nbsp;<span class="string">&apos;)&apos;</span>&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;&nbsp;Constant&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;&nbsp;Arithmetics&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;&nbsp;Variable&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;&nbsp;Abstraction<br/>
;<br/>
<br/>
Constant:&nbsp;StringConstant&nbsp;|&nbsp;IntConstant&nbsp;;<br/>
StringConstant:&nbsp;string=STRING;<br/>
IntConstant:&nbsp;int=INT;<br/>
<br/>
Arithmetics:&nbsp;<span class="string">&apos;-&apos;</span>&nbsp;term=Term;<br/>
<br/>
Variable:&nbsp;ref=[Parameter];<br/>
<br/>
Abstraction:&nbsp;<span class="string">&apos;lambda&apos;</span>&nbsp;param=Parameter&nbsp;<span class="string">&apos;.&apos;</span>&nbsp;term=Term&nbsp;;<br/>
<br/>
Parameter:&nbsp;name=ID&nbsp;(<span class="string">&apos;:&apos;</span>&nbsp;type=Type)?&nbsp;;<br/>
<br/>
<span class="comment">//&nbsp;right&nbsp;associative<br/>
</span>Type:&nbsp;TerminalType&nbsp;({ArrowType.left&nbsp;=&nbsp;<span class="keyword">current</span>}&nbsp;<span class="string">&apos;-&gt;&apos;</span>&nbsp;right=Type)?&nbsp;;<br/>
<br/>
TerminalType&nbsp;<span class="keyword">returns</span>&nbsp;Type:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="string">&apos;(&apos;</span>&nbsp;Type&nbsp;<span class="string">&apos;)&apos;</span>&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;&nbsp;BasicType&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;&nbsp;TypeVariable<br/>
;<br/>
<br/>
BasicType:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{IntType}&nbsp;<span class="string">&apos;int&apos;</span>&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{StringType}&nbsp;<span class="string">&apos;string&apos;</span><br/>
;<br/>
<br/>
TypeVariable:&nbsp;typevarName=ID;<br/>
</p>
</div>
</div>
</p>
<a name="LambdaTypeSystem"></a>
<h2>Lambda Type Inference</h2>
<p>
Thus, we want to write the type system definition in Xsemantics for Lambda, 
also inferring types (performing unification for inferring the most general type).
</p>
<p>
In the following we will skip import statements.
</p>
<p>
We start with the auxiliary functions and judgments:
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">system</span>&nbsp;org.eclipse.xsemantics.example.lambda.xsemantics.LambdaXsemanticsSystem<br/>
<br/>
<span class="keyword">validatorExtends</span>&nbsp;org.eclipse.xsemantics.example.lambda.validation.AbstractLambdaJavaValidator<br/>
<br/>
<span class="keyword">inject</span>&nbsp;LambdaUtils&nbsp;lambdaUtils<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;notoccur(Type&nbsp;type,&nbsp;Type&nbsp;other)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">error</span>&nbsp;stringRep(type)&nbsp;+&nbsp;<span class="string">"&nbsp;occurs&nbsp;in&nbsp;"</span>&nbsp;+&nbsp;stringRep(other)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;typesubstitution(TypeSubstitutions&nbsp;substitutions,&nbsp;Type&nbsp;original)&nbsp;:&nbsp;Type<br/>
&nbsp;&nbsp;&nbsp;&nbsp;unify(TypeSubstitutions&nbsp;substitutions,&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Type&nbsp;left,&nbsp;Type&nbsp;right)&nbsp;:&nbsp;UnifyResult<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">error</span>&nbsp;<span class="string">"cannot&nbsp;unify&nbsp;"</span>&nbsp;+&nbsp;stringRep(left)&nbsp;+&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="string">"&nbsp;with&nbsp;"</span>&nbsp;+&nbsp;stringRep(right)<br/>
}<br/>
<br/>
<span class="keyword">judgments</span>&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;type&nbsp;|-&nbsp;TypeSubstitutions&nbsp;substitutions&nbsp;|&gt;&nbsp;Term&nbsp;term&nbsp;:&nbsp;<span class="keyword">output</span>&nbsp;Type<br/>
&nbsp;&nbsp;&nbsp;&nbsp;paramtype&nbsp;|~&nbsp;Parameter&nbsp;param&nbsp;:&nbsp;<span class="keyword">output</span>&nbsp;Type<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
Note that this type system uses a utility class implementing a map
for type substitutions which we will use during type inference
and unification
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">package</span>&nbsp;org.eclipse.xsemantics.example.lambda.xsemantics;<br/>
<br/>
<span class="keyword">public</span>&nbsp;<span class="keyword">class</span>&nbsp;TypeSubstitutions&nbsp;{<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">protected</span>&nbsp;Map&lt;String,&nbsp;Type&gt;&nbsp;substitutions&nbsp;=&nbsp;<span class="keyword">new</span>&nbsp;HashMap&lt;String,&nbsp;Type&gt;();<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;<span class="keyword">void</span>&nbsp;reset()&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;substitutions.clear();<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;<span class="keyword">void</span>&nbsp;add(String&nbsp;typeVariableName,&nbsp;Type&nbsp;mapped)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;substitutions.put(typeVariableName,&nbsp;mapped);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;Type&nbsp;mapped(String&nbsp;typeVariableName)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">return</span>&nbsp;substitutions.get(typeVariableName);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;Set&lt;Entry&lt;String,&nbsp;Type&gt;&gt;&nbsp;getSubstitutions()&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">return</span>&nbsp;substitutions.entrySet();<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
It uses <span class="inlinecode">UnionResult</span> that is basically an implementation of a pair
of <span class="inlinecode">Type</span>s.
</p>
<p>
Let&apos;s start with the auxiliary function implementations
that check that a type variable does NOT occur 
in another type term (judgment <em>notoccur</em>, which takes two input parameters):
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">auxiliary</span>&nbsp;notoccur(Type&nbsp;type,&nbsp;Type&nbsp;other)&nbsp;{&nbsp;<span class="keyword">true</span>&nbsp;}<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;notoccur(TypeVariable&nbsp;variable,&nbsp;TypeVariable&nbsp;other)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;variable.typevarName&nbsp;!=&nbsp;other.typevarName<br/>
}<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;notoccur(TypeVariable&nbsp;variable,&nbsp;ArrowType&nbsp;arrowType)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;notoccur(variable,&nbsp;arrowType.left)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;notoccur(variable,&nbsp;arrowType.right)<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
The base case (which simply always holds) catches all the other situations not handled by
the specific cases; the second case states that
a type variable does not occur in another one, if it has a different
name, and the third one that a type variable does not
in an arrow type if it occurs neither 
in the left nor in the right part of the arrow.
</p>
<p>
Now we show the implementation of the auxiliary function <em>typesubstitution</em>, which
takes as input parameters a map for type substitution and the original type
and returns the new type after performing substitutions.
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">auxiliary</span>&nbsp;typesubstitution(TypeSubstitutions&nbsp;substitutions,&nbsp;Type&nbsp;type)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;type<br/>
}<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;typesubstitution(TypeSubstitutions&nbsp;substitutions,&nbsp;TypeVariable&nbsp;variable)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">var</span>&nbsp;mapped&nbsp;=&nbsp;substitutions.mapped(variable.typevarName)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">if</span>&nbsp;(mapped&nbsp;!=&nbsp;<span class="keyword">null</span>)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;result&nbsp;=&nbsp;EcoreUtil::copy(mapped)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;typesubstitution(substitutions,&nbsp;result)&nbsp;<span class="comment">//&nbsp;recursive<br/>
</span>&nbsp;&nbsp;&nbsp;&nbsp;}&nbsp;<span class="keyword">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;variable<br/>
}<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;typesubstitution(TypeSubstitutions&nbsp;substitutions,&nbsp;ArrowType&nbsp;arrowType)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">var</span>&nbsp;Type&nbsp;subResult<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;result&nbsp;=&nbsp;EcoreUtil::copy(arrowType)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;subResult&nbsp;=&nbsp;typesubstitution(substitutions,&nbsp;arrowType.left)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;result.left&nbsp;=&nbsp;subResult<br/>
&nbsp;&nbsp;&nbsp;&nbsp;subResult&nbsp;=&nbsp;typesubstitution(substitutions,&nbsp;arrowType.right)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;result.right&nbsp;=&nbsp;subResult<br/>
&nbsp;&nbsp;&nbsp;&nbsp;result<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
The general case simply returns the input parameter as the result
(no substitution needed).
When we substitute a type variable we create a new <span class="inlinecode">Type</span> by 
cloning the value the type variable maps to (if there&apos;s
no existing mapping, it means that there&apos;s no need of 
substitution, and the result is simply the input argument). 
However, we cannot stop here: 
a type variable can map to another type variable (see the 
cases below for unification) which in turn can be mapped to something
else and so on, thus, we must make sure we apply all the substitutions 
that concern a type variable: we apply the substitution recursively 
on the result. 
</p>
<p>
For instance, if we have the mappings 
<span class="inlinecode">X1</span> to <span class="inlinecode">(<span class="keyword">int</span>-&gt;X2)</span> and <span class="inlinecode">X2</span> to <span class="inlinecode"><span class="keyword">string</span></span> 
and we have apply the substitutions to the the type <span class="inlinecode">X1-&gt;X2</span>, 
the result must be
<span class="inlinecode">(<span class="keyword">int</span>-&gt;<span class="keyword">string</span>)-&gt;<span class="keyword">string</span></span>.
</p>
<p>
The substitution for an arrow type simply delegates it to its components
(but again, it clones the original type, and acts on the clone).
</p>
<p>
Cloning is mandatory, as explained in <a href="Lambda-example.html#WhyCloning" title="Go to &quot;Why Cloning?&quot;" >section WhyCloning</a>.
</p>
<p>
Note that, if we do not need to have a reference to the original input type,
the substitution judgment can also be invoked by passing the same
argument both for the input and as the output parameter (as we will see
in the following).
</p>
<p>
The auxiliary function for unification
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
unify(TypeSubstitutions&nbsp;substitutions,&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Type&nbsp;left,&nbsp;Type&nbsp;right)&nbsp;:&nbsp;Type<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">error</span>&nbsp;<span class="string">"cannot&nbsp;unify&nbsp;"</span>&nbsp;+&nbsp;stringRep(left)&nbsp;+&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="string">"&nbsp;with&nbsp;"</span>&nbsp;+&nbsp;stringRep(right)<br/>
</p>
</div>
</div>
</p>
<p>
takes the substitutions map, two types and outputs the unified type:
it tries to unify the two input types, and if the unification
succeeds it outputs two new types which are the unified version of the
two input types after performing the substitutions (which are
also recorded in the <em>substitutions</em> parameter).
</p>
<p>
The implementation of this auxiliary function 
considers all possible cases that make sense
(the default case simply fails); let&apos;s start considering the
simpler ones:
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">auxiliary</span>&nbsp;unify(TypeSubstitutions&nbsp;substitutions,&nbsp;Type&nbsp;t1,&nbsp;Type&nbsp;t2)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">//&nbsp;if&nbsp;we&nbsp;get&nbsp;here&nbsp;we&nbsp;cannot&nbsp;unify&nbsp;the&nbsp;two&nbsp;types<br/>
</span>&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">fail</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">null</span><br/>
}&nbsp;<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;unify(TypeSubstitutions&nbsp;substitutions,&nbsp;StringType&nbsp;t1,&nbsp;StringType&nbsp;t2)&nbsp;<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;EcoreUtil.copy(t1)<br/>
}<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;unify(TypeSubstitutions&nbsp;substitutions,&nbsp;IntType&nbsp;t1,&nbsp;IntType&nbsp;t2)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;EcoreUtil.copy(t1)<br/>
}<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;unify(TypeSubstitutions&nbsp;substitutions,&nbsp;TypeVariable&nbsp;typeVar,&nbsp;BasicType&nbsp;basicType)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;substitutions.add(typeVar.typevarName,&nbsp;basicType)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;EcoreUtil.copy(basicType)<br/>
}<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;unify(TypeSubstitutions&nbsp;substitutions,&nbsp;BasicType&nbsp;basicType,&nbsp;TypeVariable&nbsp;typeVar)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;unify(substitutions,&nbsp;typeVar,&nbsp;basicType)<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
Besides the trivial cases, a type variable unifies with a basic type,
and the type variable is replaced by (a clone) of that basic type (and
the substitution is recorded).  Note that we must also consider the
symmetric case.
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">auxiliary</span>&nbsp;unify(TypeSubstitutions&nbsp;substitutions,&nbsp;TypeVariable&nbsp;left,&nbsp;TypeVariable&nbsp;right)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">//&nbsp;unify&nbsp;both&nbsp;variables&nbsp;with&nbsp;a&nbsp;fresh&nbsp;new&nbsp;variable<br/>
</span>&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;fresh&nbsp;=&nbsp;lambdaUtils.createFreshTypeVariable<br/>
&nbsp;&nbsp;&nbsp;&nbsp;substitutions.add(left.typevarName,&nbsp;fresh)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;substitutions.add(right.typevarName,&nbsp;fresh)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;fresh<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
When we need to unify two type variables we create a fresh new
type variable (using the utility class <a class="jdoc" href="http://help.eclipse.org/helios/topic/org.eclipse.platform.doc.isv/reference/api/org/eclipse/xsemantics/example/lambda/xsemantics/LambdaUtils.html" title="View JavaDoc"><abbr title="org.eclipse.xsemantics.example.lambda.xsemantics.LambdaUtils" >LambdaUtils</abbr></a>,
and we map both variables to that new fresh variable.
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">auxiliary</span>&nbsp;unify(TypeSubstitutions&nbsp;substitutions,&nbsp;TypeVariable&nbsp;v,&nbsp;ArrowType&nbsp;arrow)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">//&nbsp;occur&nbsp;check<br/>
</span>&nbsp;&nbsp;&nbsp;&nbsp;notoccur(v,&nbsp;arrow)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;substitutions.add(v.typevarName,&nbsp;arrow)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;EcoreUtil.copy(arrow)<br/>
}<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;unify(TypeSubstitutions&nbsp;substitutions,&nbsp;ArrowType&nbsp;arrow,&nbsp;TypeVariable&nbsp;v)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;unify(substitutions,&nbsp;v,&nbsp;arrow)<br/>
}<br/>
<br/>
<span class="keyword">auxiliary</span>&nbsp;unify(TypeSubstitutions&nbsp;substitutions,&nbsp;ArrowType&nbsp;arrow1,&nbsp;ArrowType&nbsp;arrow2)<br/>
{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;newArrow1&nbsp;=&nbsp;EcoreUtil.copy(arrow1)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;newArrow2&nbsp;=&nbsp;EcoreUtil.copy(arrow2)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">var</span>&nbsp;result&nbsp;=&nbsp;unify(substitutions,&nbsp;arrow1.left,&nbsp;arrow2.left)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;newArrow1.left&nbsp;=&nbsp;EcoreUtil.copy(result)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;newArrow2.left&nbsp;=&nbsp;EcoreUtil.copy(result)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;result&nbsp;=&nbsp;unify(substitutions,&nbsp;arrow1.right,&nbsp;arrow2.right)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;newArrow1.right&nbsp;=&nbsp;EcoreUtil.copy(result)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;newArrow2.right&nbsp;=&nbsp;EcoreUtil.copy(result)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;newArrow1<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
When we unify a type variable with an arrow type, before substituting
that type variable with the arrow type, we must first check that
the variable does not occur in the arrow type (otherwise the unification
fails).  And two arrow types are unified by unifying their components.
</p>
<p>
Now we can start examining the actual typing rules.
</p>
<p>
First of all we need a dedicated judgment for <span class="inlinecode">Param</span>, since it is
not a subclass of <span class="inlinecode">Term</span>:
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">rule</span>&nbsp;ParameterType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|~&nbsp;Parameter&nbsp;param&nbsp;:&nbsp;Type&nbsp;type<br/>
<span class="keyword">from</span>&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;param.type&nbsp;!=&nbsp;<span class="keyword">null</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;type&nbsp;=&nbsp;EcoreUtil::copy(param.type)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">or</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;type&nbsp;=&nbsp;lambdaUtils.createFreshTypeVariable<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
Remember that we can write the type of abstraction&apos;s parameter, and in
that case the type is the clone of the original one; otherwise, we
give the parameter a brand new type variable.
</p>
<p>
The judgment for typing takes as a parameter also the <em>substitutions</em>
mapping table, since, as we will see, when inferring a type, we must also
apply the possible substitutions computed so far.
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">axiom</span>&nbsp;StringConstantType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|-&nbsp;TypeSubstitutions&nbsp;substitutions&nbsp;|&gt;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;StringConstant&nbsp;stringConstant&nbsp;:&nbsp;lambdaUtils.createStringType<br/>
<br/>
<span class="keyword">axiom</span>&nbsp;IntConstantType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|-&nbsp;TypeSubstitutions&nbsp;substitutions&nbsp;|&gt;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;IntConstant&nbsp;intConstant&nbsp;:&nbsp;lambdaUtils.createIntType<br/>
</p>
</div>
</div>
</p>
<p>
The typing of constants is trivial.
</p>
<p>
For the typing of a variable, one might be tempted to write
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="comment">//&nbsp;WRONG!<br/>
</span><span class="keyword">rule</span>&nbsp;VariableType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|-&nbsp;TypeSubstitutions&nbsp;substitutions&nbsp;|&gt;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Variable&nbsp;variable&nbsp;:&nbsp;Type&nbsp;type<br/>
<span class="keyword">from</span>&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|~&nbsp;variable.ref&nbsp;:&nbsp;type<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
that is, the type of a variable is the type of the referred parameter.
However, this would not work, 
since in the meantime we might have collected substitutions for
possible type variables occurring in the type type of the
referred parameter.  Thus, the type of a variable, is the
type of the referred parameter AFTER we have applied to it
possible substitutions, that is:
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">rule</span>&nbsp;VariableType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|-&nbsp;TypeSubstitutions&nbsp;substitutions&nbsp;|&gt;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Variable&nbsp;variable&nbsp;:&nbsp;Type&nbsp;type<br/>
<span class="keyword">from</span>&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;type&nbsp;=&nbsp;typesubstitution(substitutions,&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;EcoreUtil::copy(<span class="keyword">env</span>(G,&nbsp;variable.ref,&nbsp;Type)))<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
Note also that we rely on the fact that the type of the parameter is
in the environment (the environment will be updated with such information
later in the typing rule for abstraction).
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">rule</span>&nbsp;ArithmeticsType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|-&nbsp;TypeSubstitutions&nbsp;substitutions&nbsp;|&gt;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Arithmetics&nbsp;arithmetics&nbsp;:&nbsp;IntType&nbsp;intType<br/>
<span class="keyword">from</span>&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;intType&nbsp;=&nbsp;lambdaUtils.createIntType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|-&nbsp;substitutions&nbsp;|&gt;&nbsp;arithmetics.term&nbsp;:&nbsp;<span class="keyword">var</span>&nbsp;Type&nbsp;termType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">//&nbsp;the&nbsp;term&nbsp;type&nbsp;must&nbsp;be&nbsp;unifiable&nbsp;with&nbsp;int&nbsp;type<br/>
</span>&nbsp;&nbsp;&nbsp;&nbsp;unify(substitutions,&nbsp;termType,&nbsp;intType)<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
The code for <span class="inlinecode">Arithmetics</span> will be integer, however, we must
check whether the type of the subterm has a type which can be
unified with <span class="inlinecode">IntType</span>.
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">rule</span>&nbsp;AbstractionType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|-&nbsp;TypeSubstitutions&nbsp;substitutions&nbsp;|&gt;&nbsp;Abstraction&nbsp;abstraction&nbsp;:&nbsp;ArrowType&nbsp;type<br/>
<span class="keyword">from</span>&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|~&nbsp;abstraction.param&nbsp;:&nbsp;<span class="keyword">var</span>&nbsp;Type&nbsp;paramType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G,&nbsp;abstraction.param&nbsp;&lt;-&nbsp;paramType&nbsp;|-&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;substitutions&nbsp;|&gt;&nbsp;abstraction.term&nbsp;:&nbsp;<span class="keyword">var</span>&nbsp;Type&nbsp;termType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;paramType&nbsp;=&nbsp;typesubstitution(substitutions,&nbsp;paramType)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;termType&nbsp;=&nbsp;typesubstitution(substitutions,&nbsp;termType)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;type&nbsp;=&nbsp;lambdaUtils.createArrowType(paramType,&nbsp;termType)<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
For typing a lambda abstraction we take the type of the parameter and we type the body 
of the abstraction after putting the mapping for the type of the parameter in the environment
(see also <a href="XsemanticsSyntax.html#Environment" title="Go to &quot;Rule Environment&quot;" >section Environment</a>). 
Then we apply possible substitutions to the type of the parameter and the type of the body, 
and we return a brand new arrow type, using the two components.
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">rule</span>&nbsp;ApplicationType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|-&nbsp;TypeSubstitutions&nbsp;substitutions&nbsp;|&gt;&nbsp;Application&nbsp;application&nbsp;:&nbsp;Type&nbsp;type<br/>
<span class="keyword">from</span>&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|-&nbsp;substitutions&nbsp;|&gt;&nbsp;application.fun&nbsp;:&nbsp;<span class="keyword">var</span>&nbsp;Type&nbsp;funType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">//&nbsp;make&nbsp;sure&nbsp;funType&nbsp;can&nbsp;be&nbsp;unified&nbsp;ArrowType<br/>
</span>&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">var</span>&nbsp;arrowType&nbsp;=&nbsp;lambdaUtils.createFreshArrowType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;arrowType&nbsp;=&nbsp;unify(substitutions,&nbsp;funType,&nbsp;arrowType)&nbsp;<span class="keyword">as</span>&nbsp;ArrowType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;G&nbsp;|-&nbsp;substitutions&nbsp;|&gt;&nbsp;application.arg&nbsp;:&nbsp;<span class="keyword">var</span>&nbsp;Type&nbsp;argType<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">//&nbsp;unify&nbsp;arrow&nbsp;left&nbsp;with&nbsp;the&nbsp;type&nbsp;of&nbsp;the&nbsp;argument<br/>
</span>&nbsp;&nbsp;&nbsp;&nbsp;unify(substitutions,&nbsp;arrowType.left,&nbsp;argType)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">//&nbsp;the&nbsp;result&nbsp;is&nbsp;the&nbsp;arrow&nbsp;right&nbsp;after&nbsp;substitutions<br/>
</span>&nbsp;&nbsp;&nbsp;&nbsp;type&nbsp;=&nbsp;typesubstitution(substitutions,&nbsp;arrowType.right)<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
For typing a lambda application, we require the left part of the application
to be a function, thus we take its type and we 
make sure it can be unified with a generic arrow type. 
Then, we take the type of the argument, and we try to unify it with the left part of the arrow type. 
If also this unification succeeds, the resulting type is the right part of the arrow type
(after substitutions).
</p>
<p>
Let&apos;s see, informally, how these rules infer the type for
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">lambda</span>&nbsp;x.&nbsp;<span class="keyword">lambda</span>&nbsp;f.&nbsp;f&nbsp;-x<br/>
</p>
</div>
</div>
</p>
<p>
To avoid ambiguities with the <span class="inlinecode">-&gt;</span> of <span class="inlinecode">ArrowType</span> in the following example we use 
<span class="inlinecode">--&gt;</span> for substitution mappings (which are shown in <span class="inlinecode">{&nbsp;}</span>). 
Try not to confuse mappings for parameters and mappings representing type variable substitutions, 
which have strings as keys.  Mappings for the environment are represented as
<span class="inlinecode">key&nbsp;&lt;-&nbsp;value</span>.
</p>
<p>
This is informally the trace of the rules:
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
*&nbsp;AbstractionType<br/>
**&nbsp;what&nbsp;is&nbsp;the&nbsp;type&nbsp;of&nbsp;x?&nbsp;a&nbsp;fresh&nbsp;type&nbsp;variable&nbsp;X1<br/>
**&nbsp;type&nbsp;the&nbsp;body&nbsp;(<span class="keyword">lambda</span>&nbsp;f.&nbsp;f&nbsp;-x)&nbsp;with&nbsp;environment&nbsp;mapping&nbsp;x&nbsp;&lt;-&nbsp;X1<br/>
***&nbsp;AbstractionType<br/>
****&nbsp;what&nbsp;is&nbsp;the&nbsp;type&nbsp;of&nbsp;f?&nbsp;a&nbsp;fresh&nbsp;type&nbsp;variable&nbsp;X2<br/>
****&nbsp;type&nbsp;the&nbsp;body&nbsp;(f&nbsp;-x)&nbsp;with&nbsp;(additional)&nbsp;environment&nbsp;mapping&nbsp;f&nbsp;&lt;-&nbsp;X2<br/>
*****&nbsp;ApplicationType<br/>
******&nbsp;what&nbsp;is&nbsp;the&nbsp;type&nbsp;of&nbsp;the&nbsp;left&nbsp;part?&nbsp;the&nbsp;type&nbsp;variable&nbsp;X2<br/>
******&nbsp;(we&nbsp;used&nbsp;VariableType)<br/>
******&nbsp;but&nbsp;it&nbsp;must&nbsp;be&nbsp;an&nbsp;arrow&nbsp;type<br/>
******&nbsp;unify&nbsp;X2&nbsp;with&nbsp;a&nbsp;fresh&nbsp;arrow&nbsp;type&nbsp;(X3&nbsp;-&gt;&nbsp;X4)<br/>
******&nbsp;this&nbsp;will&nbsp;generate&nbsp;the&nbsp;substitution&nbsp;<span class="string">&apos;X2&apos;</span>&nbsp;--&gt;&nbsp;(X3&nbsp;-&gt;&nbsp;X4)<br/>
******&nbsp;{<span class="string">&apos;X2&apos;</span>&nbsp;--&gt;&nbsp;(X3&nbsp;-&gt;&nbsp;X4)}<br/>
******&nbsp;thus&nbsp;now&nbsp;the&nbsp;type&nbsp;of&nbsp;f&nbsp;is&nbsp;(X3&nbsp;-&gt;&nbsp;X4)<br/>
******&nbsp;what&nbsp;is&nbsp;the&nbsp;type&nbsp;of&nbsp;the&nbsp;right&nbsp;part?&nbsp;it&nbsp;is&nbsp;<span class="keyword">int</span><br/>
******&nbsp;(we&nbsp;used&nbsp;ArithmeticsType,&nbsp;and&nbsp;we&nbsp;unified&nbsp;type&nbsp;of&nbsp;x,&nbsp;X1&nbsp;with&nbsp;<span class="keyword">int</span>)<br/>
******&nbsp;{<span class="string">&apos;X2&apos;</span>&nbsp;--&gt;&nbsp;(X3&nbsp;-&gt;&nbsp;X4),&nbsp;<span class="string">&apos;X1&apos;</span>&nbsp;--&gt;&nbsp;<span class="keyword">int</span>}<br/>
******&nbsp;try&nbsp;to&nbsp;unify&nbsp;X3&nbsp;with&nbsp;<span class="keyword">int</span><br/>
******&nbsp;{<span class="string">&apos;X2&apos;</span>&nbsp;--&gt;&nbsp;(X3&nbsp;-&gt;&nbsp;X4),&nbsp;<span class="string">&apos;X1&apos;</span>&nbsp;--&gt;&nbsp;<span class="keyword">int</span>,&nbsp;<span class="string">&apos;X3&apos;</span>&nbsp;--&gt;&nbsp;<span class="keyword">int</span>}<br/>
******&nbsp;thus&nbsp;now&nbsp;the&nbsp;type&nbsp;of&nbsp;f&nbsp;is&nbsp;(<span class="keyword">int</span>&nbsp;-&gt;&nbsp;X4)<br/>
******&nbsp;the&nbsp;type&nbsp;of&nbsp;the&nbsp;application&nbsp;is&nbsp;X4<br/>
****&nbsp;apply&nbsp;the&nbsp;substitution&nbsp;to&nbsp;the&nbsp;type&nbsp;of&nbsp;param&nbsp;and&nbsp;body<br/>
****&nbsp;f&nbsp;of&nbsp;type&nbsp;X2,&nbsp;becomes&nbsp;f&nbsp;of&nbsp;type&nbsp;(<span class="keyword">int</span>&nbsp;-&gt;&nbsp;X4)<br/>
****&nbsp;the&nbsp;type&nbsp;of&nbsp;body&nbsp;(f&nbsp;-x)&nbsp;becomes&nbsp;X4<br/>
****&nbsp;the&nbsp;resulting&nbsp;type&nbsp;is&nbsp;then&nbsp;(<span class="keyword">int</span>&nbsp;-&gt;&nbsp;X4)&nbsp;-&gt;&nbsp;X4<br/>
**&nbsp;apply&nbsp;the&nbsp;substitution&nbsp;to&nbsp;the&nbsp;type&nbsp;of&nbsp;param&nbsp;and&nbsp;body<br/>
**&nbsp;x&nbsp;of&nbsp;type&nbsp;X1&nbsp;becomes&nbsp;x&nbsp;of&nbsp;type&nbsp;<span class="keyword">int</span><br/>
**&nbsp;the&nbsp;body&nbsp;has&nbsp;type&nbsp;(<span class="keyword">int</span>&nbsp;-&gt;&nbsp;X4)&nbsp;-&gt;&nbsp;X4<br/>
**&nbsp;the&nbsp;type&nbsp;of&nbsp;our&nbsp;term&nbsp;is&nbsp;<span class="keyword">int</span>&nbsp;-&gt;&nbsp;(<span class="keyword">int</span>&nbsp;-&gt;&nbsp;X4)&nbsp;-&gt;&nbsp;X4<br/>
</p>
</div>
</div>
</p>
<p>
This type, let&apos;s write it for simplicity as <span class="inlinecode"><span class="keyword">int</span>&nbsp;-&gt;&nbsp;(<span class="keyword">int</span>&nbsp;-&gt;&nbsp;a)&nbsp;-&gt;&nbsp;a</span>,
says that we must pass to this lambda term a function which takes an integer, 
and a function which takes an integer and returns "any type"; 
as a result we will have that "any type". 
Thus the following lambda application terms are well typed 
(remember that application associates to the left):
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
(<span class="keyword">lambda</span>&nbsp;x.&nbsp;<span class="keyword">lambda</span>&nbsp;f.&nbsp;f&nbsp;-x)&nbsp;(10)&nbsp;(<span class="keyword">lambda</span>&nbsp;y.&nbsp;-y)<br/>
(<span class="keyword">lambda</span>&nbsp;x.&nbsp;<span class="keyword">lambda</span>&nbsp;f.&nbsp;f&nbsp;-x)&nbsp;(1)&nbsp;(<span class="keyword">lambda</span>&nbsp;y.&nbsp;<span class="string">"foo"</span>)<br/>
</p>
</div>
</div>
</p>
<p>
The first one will return <span class="inlinecode">10</span> (actually <span class="inlinecode">--10</span>), the second one <span class="inlinecode"><span class="string">"foo"</span></span>.
</p>
<a name="WhyCloning"></a>
<h3>Why Cloning?</h3>
<p>
Remember that the types we are manipulating might have been
explicitly specified in the text of the program by the programmer,
thus, if we did not use clones, during substitutions, we would directly
modifying the AST of the original program, which is not what we want.
</p>
<a name="LambdaChecking"></a>
<h2>Lambda Type Checking</h2>
<p>
Now that we wrote all the rules for inferring types of Lambda terms, 
we can write a checkrule (see <a href="XsemanticsSyntax.html#CheckRules" title="Go to &quot;Rules for Validator: checkrule&quot;" >section CheckRules</a>) that says that a Lambda <span class="inlinecode">Program</span> 
is correct if we can assign a type to the term (starting from an empty environment):
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">checkrule</span>&nbsp;CheckProgram&nbsp;<span class="keyword">for</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;Program&nbsp;program<br/>
<span class="keyword">from</span>&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;lambdaUtils.resetCounter<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">//&nbsp;if&nbsp;we&nbsp;can&nbsp;type&nbsp;the&nbsp;program&nbsp;term<br/>
</span>&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">empty</span>&nbsp;|-&nbsp;<span class="keyword">new</span>&nbsp;TypeSubstitutions()&nbsp;|&gt;&nbsp;program.term&nbsp;:&nbsp;<span class="keyword">var</span>&nbsp;Type&nbsp;type<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
The invocation of <span class="inlinecode">resetCounter</span> is just to reset the counter used by
<a class="jdoc" href="http://help.eclipse.org/helios/topic/org.eclipse.platform.doc.isv/reference/api/org/eclipse/xsemantics/example/lambda/xsemantics/LambdaUtils.html" title="View JavaDoc"><abbr title="org.eclipse.xsemantics.example.lambda.xsemantics.LambdaUtils" >LambdaUtils</abbr></a> to create fresh
type variables.
</p>
<a name="LambdaCustomization"></a>
<h2>Customizations for Lambda</h2>
<p>
Since type variables during the type inference have the form <span class="inlinecode">X&lt;number&gt;</span> which
makes it hard to visually interpret an inferred type, we use a custom <a class="jdoc" href="http://help.eclipse.org/helios/topic/org.eclipse.platform.doc.isv/reference/api/org/eclipse/xsemantics/runtime/StringRepresentation.html" title="View JavaDoc"><abbr title="org.eclipse.xsemantics.runtime.StringRepresentation" >StringRepresentation</abbr></a>,
namely <a class="jdoc" href="http://help.eclipse.org/helios/topic/org.eclipse.platform.doc.isv/reference/api/org/eclipse/xsemantics/example/lambda/xsemantics/LambdaStringRepresentationWithTypeBeautifier.html" title="View JavaDoc"><abbr title="org.eclipse.xsemantics.example.lambda.xsemantics.LambdaStringRepresentationWithTypeBeautifier" >LambdaStringRepresentationWithTypeBeautifier</abbr></a>,
which relies on <a class="jdoc" href="http://help.eclipse.org/helios/topic/org.eclipse.platform.doc.isv/reference/api/org/eclipse/xsemantics/example/lambda/xsemantics/LambdaTypeBeautifier.html" title="View JavaDoc"><abbr title="org.eclipse.xsemantics.example.lambda.xsemantics.LambdaTypeBeautifier" >LambdaTypeBeautifier</abbr></a>: this
will consistently replace type variables in an inferred type with letters.
For instance, <span class="inlinecode">X1&nbsp;-&gt;&nbsp;X3&nbsp;-&gt;&nbsp;(X4&nbsp;-&gt;&nbsp;X3)</span> would become <span class="inlinecode">a&nbsp;-&gt;&nbsp;b&nbsp;-&gt;&nbsp;(c&nbsp;-&gt;&nbsp;b)</span>.
</p>
<p>
Another customization that we perform in this example, is the way error markers
will be generated.
</p>
<p>
For instance, due to the way error markers are generated
(<a href="XsemanticsSyntax.html#ErrorGeneration" title="Go to &quot;Error Marker Generation&quot;" >section ErrorGeneration</a>), if we have the following code
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">lambda</span>&nbsp;f&nbsp;.&nbsp;-<span class="string">&apos;f&apos;</span><br/>
</p>
</div>
</div>
</p>
<p>
we would get an error since the rule <em>ArithmeticsType</em>
cannot be applied.  However, we would like also to know why
it cannot be applied, i.e., because the string type of the string
literal <span class="inlinecode"><span class="string">&apos;f&apos;</span></span> cannot be unified with the int type required
by <em>ArithmeticsType</em>.
</p>
<p>
We can fix this by injecting a custom
<a class="jdoc" href="http://help.eclipse.org/helios/topic/org.eclipse.platform.doc.isv/reference/api/org/eclipse/xsemantics/runtime/validation/XsemanticsValidatorFilter.html" title="View JavaDoc"><abbr title="org.eclipse.xsemantics.runtime.validation.XsemanticsValidatorFilter" >XsemanticsValidatorFilter</abbr></a>,
so that it also shows the rules which failed from that point on: 
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">class</span>&nbsp;LambdaValidatorFilter&nbsp;<span class="keyword">extends</span>&nbsp;XsemanticsValidatorFilter&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;@Inject&nbsp;<span class="keyword">extension</span>&nbsp;TraceUtils<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">override</span>&nbsp;filterRuleFailedExceptions(RuleFailedException&nbsp;e)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;inner&nbsp;=&nbsp;e.innermostRuleFailedExceptionWithNodeModelSources<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">if</span>&nbsp;(inner&nbsp;!=&nbsp;null)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">return</span>&nbsp;inner.failureAsList<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">else</span>&nbsp;<span class="comment">//&nbsp;we&nbsp;must&nbsp;return&nbsp;at&nbsp;least&nbsp;a&nbsp;failure,&nbsp;so&nbsp;we&nbsp;default&nbsp;to&nbsp;the&nbsp;passed&nbsp;one<br/>
</span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">return</span>&nbsp;Lists::newArrayList(e)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
}
</p>
</div>
</div>
</p>
<a name="LambdaTypeInferenceIDE"></a>
<h2>Use of Type Inference in the IDE</h2>
<p>
We can also use the generated Java code for the inference type system to create an editor popup 
action (for the editor of Lambda) to automatically infer types and add the types in the program text, 
in particular we set the types of the parameters of abstractions.  
Most of the code we show here deals with Eclipse plugin development: 
the part which uses the code of the type system generated by Xsemantics is minimal.
</p>
<p>
This is done in the class <a class="jdoc" href="http://help.eclipse.org/helios/topic/org.eclipse.platform.doc.isv/reference/api/org/eclipse/xsemantics/example/lambda/xsemantics/LambdaTypeModifier.html" title="View JavaDoc"><abbr title="org.eclipse.xsemantics.example.lambda.xsemantics.LambdaTypeModifier" >LambdaTypeModifier</abbr></a>
(you can see the complete code in the sources of the Lambda example); we show here just the main parts:
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">public</span>&nbsp;<span class="keyword">class</span>&nbsp;LambdaTypeModifier&nbsp;{<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;@Inject<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">protected</span>&nbsp;LambdaXsemanticsSystem&nbsp;typeSystem;&nbsp;<span class="comment">//&nbsp;generated&nbsp;by&nbsp;Xsemantics<br/>
</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;@Inject<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">protected</span>&nbsp;Provider&lt;LambdaTypeBeautifier&gt;&nbsp;lambdaTypeBeautifierProvider;<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;RuleFailedException&nbsp;setAllTypes(Term&nbsp;term)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Result&lt;Type&gt;&nbsp;result&nbsp;=&nbsp;typeSystem.type(<span class="keyword">new</span>&nbsp;TypeSubstitutions(),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;LambdaTermUtils.cloneWithoutTypes(term));<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">if</span>&nbsp;(result.getRuleFailedException()&nbsp;!=&nbsp;null)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">return</span>&nbsp;result.getRuleFailedException();<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Type&nbsp;inferredType&nbsp;=&nbsp;result.getValue();<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;beautifyType(inferredType);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;setAllTypes(term,&nbsp;inferredType);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">return</span>&nbsp;null;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">protected</span>&nbsp;<span class="keyword">void</span>&nbsp;beautifyType(Type&nbsp;paramType)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;lambdaTypeBeautifierProvider.get().beautifyTypeVariables(paramType);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;...<br/>
</p>
</div>
</div>
</p>
<p>
Through the generated type system we infer the type of the term and then we update all 
the types of the parameters of the abstractions in the term. 
Note that before we "beautify" the type variable names.
</p>
<p>
As explained in the Xtext documentation, since we need to modify the EMF model of the program 
in the open editor, we need to use the <a class="jdoc" href="http://download.eclipse.org/modeling/tmf/xtext/javadoc/2.7/org/eclipse/xtext/ui/editor/model/IXtextDocument.html" title="View JavaDoc"><abbr title="org.eclipse.xtext.ui.editor.model.IXtextDocument" >IXtextDocument</abbr></a> <a class="srcLink" href="https://github.com/eclipse/xtext/blob/v2.7.0/plugins/org.eclipse.xtext.ui/src/org/eclipse/xtext/ui/editor/model/IXtextDocument.java" title="View Source Code" >(src)</a> 
and its <span class="inlinecode">modify</span> method, with a
<a class="jdoc" href="http://download.eclipse.org/modeling/tmf/xtext/javadoc/2.7/org/eclipse/xtext/util/concurrent/IUnitOfWork.html" title="View JavaDoc"><abbr title="org.eclipse.xtext.util.concurrent.IUnitOfWork" >IUnitOfWork</abbr></a> <a class="srcLink" href="https://github.com/eclipse/xtext/blob/v2.7.0/plugins/org.eclipse.xtext.util/src/org/eclipse/xtext/util/concurrent/IUnitOfWork.java" title="View Source Code" >(src)</a>; this is done by the class 
<a class="jdoc" href="http://help.eclipse.org/helios/topic/org.eclipse.platform.doc.isv/reference/api/org/eclipse/xsemantics/example/lambda/ui/typing/LambdaTermModifier.html" title="View JavaDoc"><abbr title="org.eclipse.xsemantics.example.lambda.ui.typing.LambdaTermModifier" >LambdaTermModifier</abbr></a>:
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">public</span>&nbsp;<span class="keyword">class</span>&nbsp;LambdaTermModifier&nbsp;{<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;@Inject<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">protected</span>&nbsp;LambdaTypeModifier&nbsp;lambdaTypeModifier;<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;<span class="keyword">void</span>&nbsp;modifyTermWithInferredType(IXtextDocument&nbsp;xtextDocument)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;xtextDocument.modify(<span class="keyword">new</span>&nbsp;IUnitOfWork.Void&lt;XtextResource&gt;()&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;<span class="keyword">void</span>&nbsp;process(XtextResource&nbsp;resource)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Program&nbsp;program&nbsp;=&nbsp;(Program)&nbsp;resource.getContents().get(0);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;lambdaTypeModifier.setAllTypes(program.getTerm());<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;});<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
Then we have the code implementing the editor action (<a class="jdoc" href="http://help.eclipse.org/helios/topic/org.eclipse.platform.doc.isv/reference/api/org/eclipse/xsemantics/example/lambda/ui/popup/actions/InferTypesAction.html" title="View JavaDoc"><abbr title="org.eclipse.xsemantics.example.lambda.ui.popup.actions.InferTypesAction" >InferTypesAction</abbr></a>):
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">public</span>&nbsp;<span class="keyword">class</span>&nbsp;InferTypesAction&nbsp;<span class="keyword">implements</span>&nbsp;IEditorActionDelegate&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">protected</span>&nbsp;IEditorPart&nbsp;editor;<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">protected</span>&nbsp;LambdaTermModifier&nbsp;lambdaTermModifier;<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;InferTypesAction()&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;lambdaTermModifier&nbsp;=&nbsp;LambdaUiUtil.getInjector().getInstance(<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;LambdaTermModifier.<span class="keyword">class</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;<span class="keyword">void</span>&nbsp;run(IAction&nbsp;action)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;IXtextDocument&nbsp;xtextDocument&nbsp;=&nbsp;((XtextEditor)&nbsp;editor).getDocument();<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;lambdaTermModifier.modifyTermWithInferredType(xtextDocument);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;<span class="keyword">void</span>&nbsp;selectionChanged(IAction&nbsp;action,&nbsp;ISelection&nbsp;selection)&nbsp;{<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">public</span>&nbsp;<span class="keyword">void</span>&nbsp;setActiveEditor(IAction&nbsp;action,&nbsp;IEditorPart&nbsp;targetEditor)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">this</span>.editor&nbsp;=&nbsp;targetEditor;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;}<br/>
<br/>
}<br/>
</p>
</div>
</div>
</p>
<p>
Let&apos;s see this editor action in action: suppose you have the following opened lambda file 
(this is the abstraction for composing functions):
</p>
<p>
<div class="literallayout">
<div class="incode">
<p class="code">
<span class="keyword">lambda</span>&nbsp;f&nbsp;.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">lambda</span>&nbsp;g&nbsp;.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">lambda</span>&nbsp;x&nbsp;.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;f&nbsp;(g&nbsp;x)<br/>
</p>
</div>
</div>
</p>
<p>
We can right click on the editor and select the infer type action.
And the content of the editor will be updated with the inferred types:
</p>
<p>
<div class="image" >
<img src="images/lambda_example_compose.jpeg" class=" " 
/>
<div class="caption">
The original lambda program
</div>
</div>
</p>
<p>
<div class="image" >
<img src="images/lambda_example_compose_action.jpeg" class=" " 
/>
<div class="caption">
Invoke the context menu action
</div>
</div>
</p>
<p>
<div class="image" >
<img src="images/lambda_example_compose_inferred.jpeg" class=" " 
/>
<div class="caption">
The modified lambda program with inferred types
</div>
</div>
</p>
</body>
</html>