title: Pragmatics of typed intermediate languages
body: <p>One trend in the compilation is to use <strong>typed intermediate languages</strong>. Haskell's <code>ghc</code> with its <code>core</code> intermediate language, a variant of System F-omega, is an example of this architecture [ 1 ]. Another is LLVM, which has a typed intermediate language at its core [ 2 ]. The benefit of this approach is that errors in the transformations that make up parts of the code generator can be detected early. In addition, the type information can be used during optimization and code generation.</p>
  
  <p>For efficiency, typed IRs are type-checked, rather than have their type inferred.  To make type-checks fast, each variable and each binder carry types for easy type-checking. </p>
  
  <p>However, many transformations in the compiler pipeline may introduce new variables. For example, a normalization transformation <code>K(.)</code> might transform an application</p>
  
  <pre><code>M(N)
  </code></pre>
  
  <p>into an expression like</p>
  
  <pre><code>let x = K(M) in
  let y = K(N) in x(y)
  </code></pre>
  
  <p><strong>Question.</strong> I wonder how compilers handle the issue of giving types to newly introduced
  variables. Do they re-typecheck, in the example above <code>K(M)</code> and <code>K(N)</code>? Isn't that time-consuming? And does it require passing an environment around? Do they use maps from AST nodes to type information to avoid re-running type checking?</p>
  
  <hr>
  
  <ol>
  <li><p>S. Marlow, S. Peyton Jones, <a href="http://www.aosabook.org/en/ghc.html" rel="noreferrer">The Glasgow Haskell Compiler</a>.</p></li>
  <li><p><a href="http://llvm.org/docs/LangRef.html#type-system" rel="noreferrer">LLVM Language Reference Manual</a>.</p></li>
  </ol>