Embedding higher kinded types (monads!) into the untyped lambda calculus

Question

It's possible to encode various types in the untyped lambda calculus through higher order functions.

Examples:
zero  = λfx.      x
one   = λfx.     fx
two   = λfx.   f(fx)
three = λfx. f(f(fx))
etc

true  = λtf. t
false = λtf. f

tuple = λxyb. b x y
null  = λp. p (λxy. false)

I was wondering if any research has gone into embedding other less conventional types. It would be brilliant if there is some theorem which asserts that any type can be embedded. Maybe there are restrictions, for example only types of kind * can be embedded.

If it is indeed possible to represent less conventional types, it would be awesome to see an example. I'm particularly keen on seeing what the members of the monad type class look like.

Answer 1

It's possible to represent pretty much any type you want. But since monadic operations are implemented differently for every type, it is not possible to write >>= once and have it work for every instance.

However, you can write generic functions that depend on evidence of the instance of the typeclass. Consider e here to be a tuple, where fst e contains a "bind" definition, and snd e contains a "return" definition.

bind = λe. fst e    -- after applying evidence, bind looks like λmf. ___
return = λe. snd e  -- after applying evidence, return looks like λx. ___

fst = λt. t true
snd = λt. t false

-- join x = x >>= id
join = λex. bind e x (λz. z)

-- liftM f m1 = do { x1 <- m1; return (f x1) }
-- m1 >>= \x1 -> return (f x1)
liftM = λefm. bind e m (λx. return e (f x))

You would then have to define an "evidence tuple" for every instance of Monad. Notice that the way we defined bind and return: they work just like the other "generic" Monad methods we have defined: they must first be given evidence of Monad-ness, and then they function as expected.

We can represent Maybe as a function that takes 2 inputs, the first is a function to perform if it is Just x, and the second is a value to replace it with if it is Nothing.

just = λxfz. f x
nothing = λfz. z

-- bind and return for maybes
bindMaybe = λmf. m f nothing
returnMaybe = just

maybeMonadEvidence = tuple bindMaybe returnMaybe

Lists are similar, represent a List as its folding function. Therefore, a list is a function that takes 2 inputs, a "cons" and an "empty". It then performs foldr myCons myEmpty on the list.

nil = λcz. z
cons = λhtcz. c h (t c z)

bindList = λmf. concat (map f m)
returnList = λx. cons x nil

listMonadEvidence = tuple bindList returnList

-- concat = foldr (++) []
concat = λl. l append nil

-- append xs ys = foldr (:) ys xs
append = λxy. x cons y

-- map f = foldr ((:) . f) []
map = λfl. l (λx. cons (f x)) nil

Either is also straightforward. Represent an either type as a function that takes two functions: one to apply if it is a Left, and another to apply if it is a Right.

left = λlfg. f l
right = λrfg. g r

-- Left l >>= f = Left l
-- Right r >>= f = f r
bindEither = λmf. m left f
returnEither = right

eitherMonadEvidence = tuple bindEither returnEither

Don't forget, functions themselves (a ->) form a monad. And everything in the lambda calculus is a function...so...don't think about it too hard. ;) Inspired directly from the source of Control.Monad.Instances

-- f >>= k = \ r -> k (f r) r
bindFunc = λfkr. k (f r) r
-- return = const
returnFunc = λxy. x

funcMonadEvidence = tuple bindFunc returnFunc

Answer 2

You are mixing up the type level with the value level. In untyped lambda calculus there are no monads. There can be monadic operations (value level), but not monads (type level). The operations themselves can be the same, though, so you don't lose any expressive power. So the question itself doesn't really make sense.

Answer 3

Well, we already have tuples and booleans, hence we can represent Either and in turn any non-recursive sum type based on that:

type Either a b = (Bool, (a, b))
type Maybe a    = Either () a

And Maybe is a member of the Monad type class. Translation to lambda notation is left as exercise.