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:
f : <Type> x : (f : Type) = x
is a template(like c++) of a polymorphic type. Each that function f is evaluated creates a new function with the type matched. To code church intenger is :
//T -> (T -> T) -> T
n : (<Type>) x : (n : Type) f : ((n : Type) -> (n : Type)) = f x
// Realize it's so big because by monomorphization of <type> maybe need more syntax sugar (or HM (oh no please rs))
// (T -> (T -> T) -> T) -> T -> (T -> T) -> T
k : (<Type>) f : ((k : Type) -> ((k : Type) -> (k : Type)) -> (k : Type)) -> (k : Type) -> ((k : Type) -> (k : Type)) -> (k : Type) a : (k : Type) = f (a x) a
I can represent a sum type of a tuple(int, string) or just a int like this:
y : (Tuple <Int, String> | Number Int) x : Int = Number Int
t : (Tuple <Int, String> | Number Int) x : (<Int, String>) = Tuple ((first x) (second x))
f : (Tuple <Int, String> | Number Int) x : <Type> = x : <Type>
Furthermore, i also can represent a Maybe Monad like this:
Maybe : (Nothing | Just (x : Type)) x : <Type> = x
And use both to safe way get values:
_ : ((Maybe : Type) -> Int) x : (Tuple <Int, String> | Number Int) = (x of [
x : Tuple -> Nothing
x : Number -> (Just (f<(x : Type)> x))
// the compiler know that the value x in the case asuume the Number Type
])
I am thinking in add a new rule that to prevent expression like f x = d or f x = 3 or even f x y = x Give a set of a function fx variables free and bound variables (k f d) in expression x (k f d), the function fx is only possible if all variables are evaluated in lambda term.