Typed Turing-complete combinators? 
Author Message
 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):

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

> 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

Tue, 31 Jul 2001 03:00:00 GMT  
 [ 1 post ] 

 Relevant Pages 

1. are dylan macros Turing-complete?

2. Searching for a Turing Complete Compiled Language

3. fixpoint combinator without recursive types?

4. 1) type inferencing 2) monadic parser combinators 3) functional symbol tables

5. type decls and the ML Y combinator

6. Recursion, least fixed point combinators, etc.

7. Y combinator

8. optimisation of combinators

9. Combinators

10. Combinator Parsers

11. >> combinator in Haskell

12. Combinators for data flow / Laws of Form


Powered by phpBB® Forum Software