Higher Kinded Types in Scala and Haskell

Question

Data.Foldable shows the following algebraic data type:

data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a)

Its kind is * -> *. It requires an a type.

Prelude> :k Tree
Tree :: * -> *

Let's look now at trait Foldable[_], a "higher-kinded type" from Scala from Functional Programming in Scala:

trait Foldable[F[_]] {
  def foldRight[A,B](as: F[A])(z: B)(f: (A,B) => B): B
  ...
}

The excellent book says:

Just like values and functions have types, types and type constructors have kinds. Scala uses kinds to track how many type arguments a type constructor takes, ...

EDIT

When specifying trait Foldable[F[_]], does the F[_] always indicate a higher-kinded type? Is it possible for F[_] to be anything else? Could it be a type - F[A]?

Answer 1

The F[_] in Scala stands for something like * -> * in Haskell: that is a type which "receives" a concrete type (the _ in Scala and the first * in Haskell) and returns a new concrete type (F[A] for some concrete type A and concrete "container" F in Scala).

So yes, F[_] stands for some higher kinded type like List[_] or Option[_]. It wouldn't be useful to define traversable in scala like trait Foldable[A,F[A]] because we would be saying that Foldable needs to be defined with the specific thing being folded (the A).

Answer 2

You haven't asked much of a question, but if you want a general idea: yes, the "kind" system of both of these languages is a type system for their own type system. The * type is not a wildcard but a special type atom; * is the type of "concrete types" like String, [String], and Tree String.

In turn there are things like [] or Tree (see the difference?) which have kind * -> *; this is the type of "singly-parametrized types" which take a concrete type and produce another concrete type.

A last example: there are things called "monad transformers" like MaybeT which takes a monad like IO and produces another monad like IO . Maybe (if you will pardon the use of function composition operators where they're not generally admitted). What kind does that have? Why, (* -> *) -> * -> * of course: monads have kind * -> * so we take one of those types and transform it into another of those types.

I cannot speak with so much expertise on Scala syntax, but on the Internet we see a definition of a monad transformer trait in Scala as:

trait MonadTrans[F[_[_], _]] {
  def lift[G[_] : Monad, A](a: G[A]): F[G, A]
}

so I think your guess is mostly right (that the brackets indicate a dependent type).

Having a type theory of these things guarantees that you never write things like IO IO as a concrete type, or MaybeT String.