Before everything Kei name isn't a official, but can to be (i don't know yet), therefore i will accept suggestions. The idea of kei is for creating safe mini-libs for system language programming like c++ with a high level of predictability of compilation with small specifics functional optimizations. Let's go to rules of typed lambda calculus:
x : σ E T, x is a constant type of T', T, x:σ |- e:t T |- n : σ -> t T |- k : σ
T |- x : σ T |- c:T' T |- (λx:σ. e):(σ -> t) T |- (n k):t
Fine, now let's go to introduce kei language: Give a function that receives T and returns T: