Higher kinded types

[Lindsay Winkler]

Hi,

I'm reading http://haskellbook.com/, and in chapter 11,

* -> * -> *

is referred to as a higher-kinded type.  I'm struggling to match this up with my understanding of a higher-kinded type, namely that it is a higher-order function in the realm of types.

And I understand a higher-order function to be a function that accepts another function as an argument.

Accordingly, I think that a higher-kinded type, could look like:

(* -> *) -> *

Am I missing some equivalence between * -> * -> * and (* -> *) -> *, or is this possibly an error in the book?

Thanks very much,

Lindsay. 

[Jed Wesley-Smith]

Lindsay,

A Higher Kinded Type (HKT) is simply a type which takes a type as a parameter and returns a type, aka a type constructor. Simple examples are things like List, where you need to give it a type parameter (say String) to get fully formed type `List String`. A concrete type constructor like List is not though an example of HKT, HKT is the ability to abstract over things that are type constructors (or have kinds more complex than simply *).

So the equivalence with a higher order function  (HOF) is that takes a function as an argument.

I think your confusion stems from the notation. A function is generally 'a -> b', whereas a type is simply '*'. So a simple HOF is something like `(a -> b) -> a -> b` (given a function f: a -> b, return a new function: a -> b, whereas the simplest HKT is `* -> *' (given a type, return a type).

I wrote a blogpost ages ago that is Scala flavoured, but might help:

https://blogs.atlassian.com/2013/09/scala-types-of-a-higher-kind/

cheers,

jed.

The information contained in this e-mail message and any accompanying files is or may be confidential. If you are not the intended recipient, any use, dissemination, reliance, forwarding, printing or copying of this e-mail or any attached files is unauthorised. This e-mail is subject to copyright. No part of it should be reproduced, adapted or communicated without the written consent of the copyright owner. If you have received this e-mail in error please advise the sender immediately by return e-mail or telephone and delete all copies. Fairfax Media does not guarantee the accuracy or completeness of any information contained in this e-mail or attached files. Internet communications are not secure, therefore Fairfax Media does not accept legal responsibility for the contents of this message or attached files.

--
You received this message because you are subscribed to the Google Groups "nicta-fp" group.
To unsubscribe from this group and stop receiving emails from it, send an email to nicta-fp+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Matthew Brecknell]

I don't have the Haskell book (no time to read it!), so I can't comment on the content there. I would be surprised if it described "* -> * -> *" as a type, higher-kinded or otherwise, because "* -> * -> *" is a kind, not a type. It pays to be careful which side of the "::" you are talking about!

In my opinion, the terminology of "higher-kinded type" is a bit broken. When I think of the word "type", I think literally of "*", so a type is any thing that can go to the left of ":: *", and nothing else. With this view, describing a type as having a "higher kind" seems dubious, because a type always has kind "*", by definition. Sure, a type constructor can have kind "* -> *", or even "(* -> *) -> *", but a type constructor is not a type (in this view).

But then, "constructor" is hard to say, so when the context makes clear that one is talking about a constructor, one tends to drop that word.

So, when I hear "Foo is a higher-kinded type", I take it as shorthand for "Foo is a type constructor with a higher-order kind", because Foo must be a type constructor to have a higher-order kind. And when I hear "Haskell has higher-kinded types", I take it as shorthand for "Haskell has a type system which allows type constructors with higher-order kinds".

Now, what is a higher-order kind? I think Lindsay has it right: "(* -> *) -> *" is a higher-order kind, whereas "* -> * -> *" is merely a first-order kind.

[Lindsay Winkler]

Thank you very much!

The underlying motivation is that I'm trying to understand exactly what enables a language like Haskell to have something like Functor as a type constraint (and therefore enable you to treat something as a Functor, with no interest in what the concrete nature of the thing is).

I've seen it said that "higher kinded types" are the distinction - Haskell has HKT but Java, Swift etc. do not.

But it seems to me that any language with generics has * -> * -> *.  It just normally looks like T<A, B> - that is, something generic in two parameters.

And that therefore the distinguishing feature must be the possibility of (* -> *) -> *

Which is exactly what both of you have said, on further reflection.  I'm not overly fussed about exactly what it's called, but I do want to make sure I understand the concept.  From the handful of conversations I've had about it to date, I get the impression that HKT is not a term that's used very rigorously ie. I sense that sometimes it can encompass * -> *, whereas others use it to mean specifically things like (* -> *) -> *

To unsubscribe from this group and stop receiving emails from it, send an email to nicta-fp+u...@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "nicta-fp" group.

To unsubscribe from this group and stop receiving emails from it, send an email to nicta-fp+u...@googlegroups.com.

[Jed Wesley-Smith]

Any language such as Java or Swift that supports generics, or parameterised types, has type constructors. The distinguishing feature of these languages that do not support higher-kinded types is that type parameters can only have the kind *, ie. they must _always_ be fully formed types. HKT allows you to abstract across type constructors with more complex kinds, such as * -> *, so we effectively can have a type parameter F[_] (abusing scala syntax) that is a type constructor, and can be instantiated to F[A], F[String] etc, and can be passed any type constructor of the right kind, eg. List[_], Maybe[_], Future[_], Map[Key, _] etc.

The question of whether describing F[_] as a higher kinded type or not is interesting – as Matt says, F[_] is most definitely _not_ a type, but then the type parameter A is not a type either, but a type variable. So, we're really talking about higher-kinded type parameters/variables, not higher kinded types.

Whether we want/need to distinguish between higher-kinded type parameters and higher-order kinds is not necessarily that interesting unless we have a language that only supports the first but not the latter. I am not aware of a language that has this restriction.

cheers,

jed.