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))))))

Trebuchet

There's no equivalent implementation in Haskell. Such an implementation would not typecheck. It is possible to write an implementation using a different strategy of course. – Stallfeed

Yes, I'm aware that it wouldn't type check. I guess the part I'm getting tripped up on is understanding what ((iota)(iota)) is doing in this implementation. – Trebuchet

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.

Unbutton

Approach #2 is beyond me, but I'm starting to grasp approach #1 would you be willing to explain it in a little greater detail? How exactly does that fix operator work? – Trebuchet

fix is a fixed-point combinator, which basically introduces unbounded recursion into a language that lacks it. If you've heard of the Y combinator, well, fix is the equivalent in Haskell. The short explanation is that fix f = f (f (f (f ...))) (an infinite tower of applications of f); since f can be lazy in Haskell, f has the choice to either return a value without using f (base case) or using the f (f (f (f ...))) stack (recursive case). – Unbutton

Small note about fix: generally you can convert a recursive function f = λx. ... f y ... into its anonymous version by adding an extra argument representing the recursive case and fixing the result: f = fix (λrec x. ... rec y ...). – Treadle

in you 1st approach you write iota x = x k s k , in 2nd - "iota is basically λx.x S K". Was that a typo perhaps? – Hilary

@WillNess: no, not a typo. The Wikipedia link shows both as possible ways of defining it, which lead to different iota-based definitions of s and k. For some reason, however, if you use the λx.x S K version in Haskell, while that typechecks, the related s and k definitions don't. – Unbutton

I'm having some trouble applying either definition. The Wikipedia link about One-point bases talks of X', which is the one you use in Approach #1. It says there that (X' X') X' =β K, and so I'd expect (fix iota') (fix iota') (fix iota') 1 2 to evaluate to 1, just as const 1 2 would in Haskell, but instead it gives a type error. Even :t fix iota' gives a type error. Nevertheless, this is a great answer. – Vivian