title: Representing a fixpoint in a head-normal lambda calculus AST
body: <p>Consider the following normalized term representation, obtained during type checking:</p>
  
  <pre><code>data Normal a
    = Neutral (Neutral a)
    | Type
    | Pi (Normal a) (Normal (Maybe a))
    | Abstract (Normal (Maybe a))
  
  data Neutral a
    = Variable a
    | Apply (Neutral a) (Normal a)
  </code></pre>
  
  <p>I would like to be able to represent a fixpoint within this framework, or at least in a way that preserves its head-normal property, which is very convenient for implementing substitution and definitional equality.</p>
  
  <p>At first, I thought of using a fixpoint combinator defined in the calculus itself.  The Y combinator is out of the question, though, as with this term representation I cannot apply a lambda to a lambda.  The Z combinator is close to what I want, but assumes that the result is to be a function.</p>
  
  <p>If I were simply doing graph reduction, I would tie the knot with Haskell itself, leading to a lazy infinite syntax tree.  However, as this is being used for a dependent type checker, I need to be able to test for definitional equality on terms - it would get caught in an infinite loop this way.</p>