I'm going to take the few pieces of knowledge I have about lambda calculi and ask a pair of very uninformed questions :-)Is it possible to embed the corners of the lambda cube within the untyped lambda calculus?  It would seem that this might lead to a language where the programmer implements the type system in the language, rather than having it already implemented in the compiler.  Also, maybe the concept of type system could be generalized to any arbitrary compile-time or run-time constraint checking.  Does such a language already exist?
Can type information be encoded in the untyped lambda calculus?
programming languages;lambda calculus;typing;type checking