8

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))))))
Josh Voigts
  • 4,114
  • 1
  • 18
  • 43
  • 6
    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. – n. m. could be an AI Aug 14 '12 at 22:01
  • 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. – Josh Voigts Aug 14 '12 at 23:11

1 Answers1

13

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.

Luis Casillas
  • 29,802
  • 7
  • 49
  • 102
  • 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? – Josh Voigts Aug 15 '12 at 00:09
  • 1
    `fix` is a [fixed-point combinator](http://en.wikipedia.org/wiki/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). – Luis Casillas Aug 15 '12 at 00:24
  • 1
    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 `fix`ing the result: `f = fix (λrec x. ... rec y ...)`. – Vitus Aug 15 '12 at 02:08
  • 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? – Will Ness Aug 15 '12 at 07:45
  • @WillNess: no, not a typo. The [Wikipedia link](http://en.wikipedia.org/wiki/Combinatory_logic#One-point_basis) 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. – Luis Casillas Aug 15 '12 at 16:42