# Is there an implementation of higher kinded types in typed lambda calculus?

I can see that we can do higher kinded types ( * -> *) -> * in Scala and Haskell and other languages. I'm looking for a simpler vanilla implementation of just the basic static type checking system - perhaps in Prolog or MiniKanren.

My question is: Is there an implementation of higher kinded types in typed lambda calculus?

• This is pretty ambiguous. Is Lambda Calculus the language of implementation, or the base language that you've added a higher-kinded type system to? – jmite May 3 '16 at 5:29
• I took Lambda Calculus to be the 'theoretical language' that was then implemented by an 'actual' language. – hawkeye May 3 '16 at 8:40

• @hawkeye It depends on what you mean by HKTs. For me $\lambda\omega$ (from Barendregt's $\lambda$-cube) is the prototypical type-theory with full HKTs. However, type-inference for $\lambda\omega$ (not to mention $F_{\omega}$) doesn't appear to be decidable, because it's probably equivalent to higher-order unification (which is known to be undecidable). For example, say you want to unify $f\ x = List\ a$ where $f$ has kind $* \rightarrow *$, then you loose the principal-kind property. (Continued below.) – Martin Berger May 3 '16 at 9:02
• If you restrict which kind-functions are allowed as inhabitants of $* \rightarrow *$, in particular forbid $\lambda k^{*}. k$, you can get away with first-order unification. That's what Haskell does. Not many accessible papers around on HKTs, maybe M. P. Jones, "A system of constructor classes: overloading and implicit higher-order polymorphism", which describes Haskell's approach. – Martin Berger May 3 '16 at 9:04