cdiggins.com

Mockingbird is a mnemonic for the M combinator in combinatory logic which is defined as M = SII in the SK calculus and M = \a.aa in the Lambda calculus.

Interestingly I tried to figure out the type for this combinator using the type inference feature of SML 98 and F# and ran into an error. When I posted a query to comp.lang.functional I recieved some very illuminating responses.

In summary the issue resolves around the purposeful limitation of many type inference algorithms to infer recursive types.

For those who insist on recursive types inferred O’Caml is capable of doing it using the -rectypes option. The result yields:

# fun a -> a a;;
- : (’a -> ‘b as ‘a) -> ‘b =

Thanks to Andreas Rossberg and Benedikt Schmidt for their helpful explanations.

For more information see: http://cristal.inria.fr/~fpottier/publis/fpottier-appsem-2005.pdf 

 

This entry was posted on Friday, December 22nd, 2006 at 10:32 pm and is filed under Everything. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.