Problem Detail: Most of us know the correspondence between combinatory logic and lambda calculus. But I’ve never seen (maybe I haven’t looked deep enough) the equivalent of “typed combinators”, corresponding to the simply typed lambda calculus. Does such thing exist? Where could one find information about it?
Asked By : Hugo S Ferreira
Answered By : Dave Clarke
The expressive completeness of the typed combinators compared to the simply typed lambda calculus has been demonstrated. For each untyped combinator, one needs a whole family of typed combinators. For example, one has
- $mathbf{I}_{alphatoalpha}$
- $mathbf{K}_{alphato(betatoalpha)}$
- $mathbf{S}_{alphato(betatogamma)to(alphatobetato(alphatogamma))}$
for all combinations of simple types $alpha,beta$ and $gamma$. Alternatively, just think of the types as type schemes (or polymorphic types) and enter them into Haskell and voila: combinators.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/1816
