title: Adventures with the untyped lambda calculus
body: <p>We occasionally have people ask about implementing the untyped lambda calculus in Haskell. [Naturally, I now cannot <em>find</em> any of these questions, but I'm sure I've seen them!] Just for giggles, I thought I'd spend some time playing with this.</p>
  
  <p>It's trivial enough to do something like</p>
  
  <pre><code>i = \ x -&gt; x
  k = \ x y -&gt; x
  s = \ f g x -&gt; (f x) (g x)
  </code></pre>
  
  <p>This works perfectly. However, as soon as you try to do something like</p>
  
  <pre><code>s i i
  </code></pre>
  
  <p>the type-checker rightly complains about an infinite type. Basically <em>everything</em> in the untyped lambda calculus is a function &mdash; which essentially means all functions have <em>infinite</em> arity. But Haskell only allows functions of finite arity. (Because, really, why would you want infinite arity?)</p>
  
  <p>Well, it turns out we can easily side-step that limitation:</p>
  
  <pre><code>data Term = T (Term -&gt; Term)
  
  T f ! x = f x
  
  i = T $ \ x -&gt; x
  k = T $ \ x -&gt; T $ \ y -&gt; x
  s = T $ \ f -&gt; T $ \ g -&gt; T $ \ x -&gt; (f ! x) ! (g ! x)
  </code></pre>
  
  <p>This works perfectly, and allows arbitrary lambda expressions to be constructed and executed. For example, we can easily build a function to turn an <code>Int</code> into a Church numeral:</p>
  
  <pre><code>zero = k ! i
  succ = s ! (s ! (k ! s) ! k)
  
  encode 0 = zero
  encode n = succ ! (encode $ n-1)
  </code></pre>
  
  <p>Again, this works perfectly.</p>
  
  <p>Now write a decode function.</p>
  
  <p>&hellip;yeah, good luck with that! The trouble is, we can <em>create</em> arbitrary lambda terms, but we can't <em>inspect</em> them in any way. So we need to add some way to do that.</p>
  
  <hr>
  
  <p>So far, the best idea I've come up with is this:</p>
  
  <pre><code>data Term x = F (Term x -&gt; Term x) | R (Term x -&gt; x)
  
  F f ! x =            f x
  R f ! x = R $ \ _ -&gt; f x
  
  out :: Term x -&gt; x
  out (R f) = f (error "mu")
  out (F _) =   (error "nu")
  
  i = F $ \ x -&gt; x
  k = F $ \ x -&gt; F $ \ y -&gt; x
  s = F $ \ f -&gt; F $ \ g -&gt; F $ \ x -&gt; (f ! x) ! (g ! x)
  </code></pre>
  
  <p>I can now do something like</p>
  
  <pre><code>decode :: Term Int -&gt; Int
  decode ti = out $ ti ! R (\ tx -&gt; 1 + out tx) ! R (\ tx -&gt; 0)
  </code></pre>
  
  <p>This works great for Church Bools and Church numerals.</p>
  
  <hr>
  
  <p>Things start to go horribly wrong when I start trying to do anything high-order. Having thrown away all the type information to implement the <em>untyped</em> lambda calculus, I'm now struggling to convince the type checker to let me do what I want to do.</p>
  
  <p>This works:</p>
  
  <pre><code>something = F $ \ x -&gt; F $ \ n -&gt; F $ \ s -&gt; s ! x
  nothing   =            F $ \ n -&gt; F $ \ s -&gt; n
  
  encode :: Maybe x -&gt; Term x
  encode (Nothing) = nothing
  encode (Just  x) = something ! x
  </code></pre>
  
  <p>This does not:</p>
  
  <pre><code>decode :: Term x -&gt; Maybe (Term x)
  decode tmx = out $ tmx ! R (\ tx -&gt; Nothing) ! R (\ tx -&gt; Just tx)
  </code></pre>
  
  <p>I've tried a dozen slight variations on this; none of them type-check. It's not that I don't understand why it fails, but rather than I can't figure out any way for it to succeed. (Most particularly, <code>R Just</code> is clearly ill-typed.)</p>
  
  <p>It's almost as if I want a function <code>forall x y. Term x -&gt; Term y</code>. Because, for <em>pure</em> untyped terms, this should always be possible. It's only terms involving <code>R</code> where that won't work. But I can't figure out how to phrase that in the Haskell type system.</p>
  
  <p>(For example, try changing the type of <code>F</code> to <code>forall x. Term x -&gt; Term x</code>. Now the definition of <code>k</code> is ill-typed, since the inner <code>F $ \ y -&gt; x</code> cannot actually return <em>any</em> type, but only the [now fixed] type of <code>x</code>.)</p>
  
  <p>Any anybody smarter than me have a better idea?</p>