Implementing Iota in Haskell

Question

Iota is a ridiculously small "programming language" using only one combinator. I'm interested in understanding how it works, but it would be helpful to see the implementation in a language I'm familiar with.

I found an implementation of the Iota programming language written in Scheme. I've been having a little trouble translating it to Haskell though. It's rather simple, but I'm relatively new to both Haskell and Scheme.

How would you write an equivalent Iota implementation in Haskell?

(let iota ()
  (if (eq? #\* (read-char)) ((iota)(iota))
      (lambda (c) ((c (lambda (x) (lambda (y) (lambda (z) ((x z)(y z))))))
           (lambda (x) (lambda (y) x))))))

Answer 1

I've been teaching myself some of this stuff, so I sure hope I get the following right...

As n.m. mentions, the fact that Haskell is typed is of enormous importance to this question; type systems restrict what expressions can be formed, and in particular the most basic type systems for the lambda calculus forbid self-application, which ends up giving you a non-Turing complete language. Turing completeness is added on top of the basic type system as an extra feature to the language (either a fix :: (a -> a) -> a operator or recursive types).

This doesn't mean you can't implement this at all in Haskell, but rather that such an implementation is not going to have just one operator.

Approach #1: implement the second example one-point combinatory logic basis from here, and add a fix function:

iota' :: ((t1 -> t2 -> t1)
          -> ((t5 -> t4 -> t3) -> (t5 -> t4) -> t5 -> t3)
          -> (t6 -> t7 -> t6)
          -> t)
         -> t
iota' x = x k s k 
    where k x y = x
          s x y z = x z (y z)

fix :: (a -> a) -> a
fix f = let result = f result in result

Now you can write any program in terms of iota' and fix. Explaining how this works is a bit involved. (EDIT: note that this iota' is not the same as the λx.x S K in the original question; it's λx.x K S K, which is also Turing-complete. It is the case that iota' programs are going to be different from iota programs. I've tried the iota = λx.x S K definition in Haskell; it typechecks, but when you try k = iota (iota (iota iota)) and s = iota (iota (iota (iota iota))) you get type errors.)

Approach #2: Untyped lambda calculus denotations can be embedded into Haskell using this recursive type:

newtype D = In { out :: D -> D }

D is basically a type whose elements are functions from D to D. We have In :: (D -> D) -> D to convert a D -> D function into a plain D, and out :: D -> (D -> D) to do the opposite. So if we have x :: D, we can self-apply it by doing out x x :: D.

Give that, now we can write:

iota :: D
iota = In $ \x -> out (out x s) k
    where k = In $ \x -> In $ \y -> x
          s = In $ \x -> In $ \y -> In $ \z -> out (out x z) (out y z)

This requires some "noise" from the In and out; Haskell still forbids you to apply a D to a D, but we can use In and out to get around this. You can't actually do anything useful with values of type D, but you could design a useful type around the same pattern.

---

EDIT: iota is basically λx.x S K, where K = λx.λy.x and S = λx.λy.λz.x z (y z). I.e., iota takes a two-argument function and applies it to S and K; so by passing a function that returns its first argument you get S, and by passing a function that returns its second argument you get K. So if you can write the "return first argument" and the "return second argument" with iota, you can write S and K with iota. But S and K are enough to get Turing completeness, so you also get Turing completeness in the bargain. It does turn out that you can write the requisite selector functions with iota, so iota is enough for Turing completeness.

So this reduces the problem of understanding iota to understanding the SK calculus.