Cat can now infer the type of M and reject Omega

I’ve talked a lot about the “m” combinator (”dup apply”) which is a critical component of nameless recursion algorithms. The most recent Cat interpreter in the subversion repository is able to infer the type correctly of the “m” combinator as “(’A self -> ‘B)”. This type is the same as: “(’A (’A self -> ‘B) -> ‘B)”. You can see the type itself is recursive. What is also interesting is that the “omega” combinator, defined in combinatory logic as “m(m)” or in Cat: “[m] m”, is rejected by the type system. The inferred type is  “(’A -> ‘B)”. This is ill-typed because ‘B can not be deduced from the stack. In simple terms, ‘B does not appear in the consumption, so it can never be assigned a concrete type.

I still have more testing to do, but I should have a new version of Cat posted in a few days.

Leave a Reply

You must be logged in to post a comment.