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?

Improve this question
$\endgroup$
2
  • 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$
    – Joey Eremondi
    Commented May 3, 2016 at 5:29
  • $\begingroup$ I took Lambda Calculus to be the 'theoretical language' that was then implemented by an 'actual' language. $\endgroup$
    – hawkeye
    Commented May 3, 2016 at 8:40

1 Answer 1

Reset to default
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!

Improve this answer
$\endgroup$
5
  • $\begingroup$ Yeah - its looking like TAPL or Practical Foundations of Programming Languages - thanks. $\endgroup$
    – hawkeye
    Commented May 3, 2016 at 8:41
  • $\begingroup$ Could you expand on why Scala and Haskell don't support HKTs fully? A link perhaps? $\endgroup$
    – hawkeye
    Commented May 3, 2016 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
    Commented May 3, 2016 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
    Commented May 3, 2016 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
    Commented May 3, 2016 at 9:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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