2
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ 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? $\endgroup$ – jmite May 3 '16 at 5:29
  • $\begingroup$ I took Lambda Calculus to be the 'theoretical language' that was then implemented by an 'actual' language. $\endgroup$ – hawkeye May 3 '16 at 8:40
3
$\begingroup$

I doubt you find mainstream languages with HKTs simpler than Scala and Haskell. And even those don't implement HKTs fully. Tim Sheard's Ωmega and some interactive proof assistants have HKTs too.

Chapters 29 and 30 of Types and Programming Languages show exactly how HKTs are added to a typing-system and how to do type-checking with HKTs. Why not do it yourself, it's instructive!

$\endgroup$
  • $\begingroup$ Yeah - its looking like TAPL or Practical Foundations of Programming Languages - thanks. $\endgroup$ – hawkeye May 3 '16 at 8:41
  • $\begingroup$ Could you expand on why Scala and Haskell don't support HKTs fully? A link perhaps? $\endgroup$ – hawkeye May 3 '16 at 8:44
  • 1
    $\begingroup$ @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.) $\endgroup$ – Martin Berger May 3 '16 at 9:02
  • $\begingroup$ 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. $\endgroup$ – Martin Berger May 3 '16 at 9:04
  • $\begingroup$ Scala's typing system is in flux. Have a look at the latest DOT paper The Essence of Dependent Object Types to see where the journey is probably going. $\endgroup$ – Martin Berger May 3 '16 at 9:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.