cdiggins.com

I was asked an interesting question yesterday by Slava Pestov the inventor of the Factor language. Is the following well-typed and if so, what is its type:

[dup apply] dup apply

This is actually equivalent to

[m] m

Where m is a combinator from combinatory logic (see also: http://tunes.org/~iepos/joy.html ). You’ll notice that “omega” is defined as “mm”.

At first I thought it was well-typed and that my type inference was not able to deal with it because it was recursive. However, even with recursive types and type labeling it is not well typed. Let me start by saying what the type of “m” is (or should be, if labeled type inference was full functional):

m : (’A f=(’A f -> ‘B) -> ‘B)

However the type of omega can only be reduced to:

[m] m : (’A -> ‘B)

This is ill-typed because the stack variable ‘B appears for the first time to right of  the arrow. This was a surprise to me, but is a desirable outcome because omega is an infinite loop. Cool!