Interesting article, but I found some of the syntactic choices questionable. The use of lam a b instead of a -> b is strange, and definitely subverted my expectations in a detrimental way (and why did he re-use lam in the first place? Wouldn’t it be nice for your language and type grammars to look different?).
lam a b
a -> b