Typed Turing-complete combinators?

It's well-known that the set of combinators S, K, and I

are Turing-complete. (And, of course, you don't need I,

as I = S K K.) However, in my mind they correspond

to the untyped lambda calculus, as the type needed for S

in this doesn't fit into the usual restrictions of the Hindley-Milner

type systems found in SML and Haskell.

That is, if we define, in Haskell (where we can't use the usual capitals):

Quote:

> i x = x

> k c x = c

> s f g x = ((f x) (g x))

Then Haskell gives the s combinator given the following type:

s :: (a -> b -> c) -> (a -> b) -> a -> c

Unfortunately, this isn't general enough, as it assumes that

x is a monomorphic function. Thus the terms like

((s i) i)

don't typecheck.

That's all well-known and a standard limitation of the Hindley-Milner

type system.

Suppose we want to live within that type system,

and suppose we give ourselves a recursion operator as a primitive,

as we must to get Turing-completeness. Call this recursion primitive "fix",

and define its semantics by:

Quote:

> fix g = g (fix g)

Now, my question is this. What's a minimal set of other combinators

needed to get Turing-completeness, assuming we have "fix" and want

to use combinators with their types given by Hindley-Milner?

I'm looking for "interesting" sets of combinators to show my students.

S and K are interesting, but do they work in such a typed context also?

I'm sure that there must be others that are equally neat.

Gary T. Leavens

--

Department of Computer Science, Iowa State University

229 Atanasoff Hall, Ames, Iowa 50011-1040 USA

URL: http://www.*-*-*.com/ ~leavens