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.
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.