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?
$\begingroup$
$\endgroup$
1
-
$\begingroup$ You might be interested in The Reader Monad and Abstraction Elimination in The Monad.Reader, Issue 17. The Reader monad (or more precisely its applicative functor) is closely related to typed SKI. $\endgroup$Petr– Petr2012-12-11 10:14:34 +00:00Commented Dec 11, 2012 at 10:14
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
3
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}_{\alpha\to\alpha}$
- $\mathbf{K}_{\alpha\to(\beta\to\alpha)}$
- $\mathbf{S}_{\alpha\to(\beta\to\gamma)\to(\alpha\to\beta\to(\alpha\to\gamma))}$
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.
-
$\begingroup$ I never thought of the $\mathbf{S}$ combinator as acting over a Monad! Is that so? $\endgroup$Hugo Sereno Ferreira– Hugo Sereno Ferreira2012-05-13 10:27:25 +00:00Commented May 13, 2012 at 10:27
-
$\begingroup$ Actually, I've been pointed out that $\mathbf{S}$ corresponds to the
<*>operator of Applicative Functors, andpurethe $\mathbf{K}$. $\endgroup$Hugo Sereno Ferreira– Hugo Sereno Ferreira2012-05-13 10:41:52 +00:00Commented May 13, 2012 at 10:41 -
$\begingroup$ $\mathbf{S}$ is quite fundamental, so it could correspond to many things. $\mathbf{S}$ has the same type as the monad function $ap$ for functor $\Lambda X.\alpha\to X$. $\endgroup$Dave Clarke– Dave Clarke2012-05-13 14:40:29 +00:00Commented May 13, 2012 at 14:40