CODEWITHSUNDEEP
scalahaskellhigher-kinded-types
Kevin Meredith
Kevin Meredith

Reputation: 41909

Higher Kinded Types in Scala and Haskell

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]?

Upvotes: 5

Views: 691

Answers (3)

lmm
lmm

Reputation: 17431

F[_] in that context, i.e. as a type parameter to a class or method, always means a higher-kinded type, aka a type constructor. You can also write it as F[A] but would normally only do that if you were going to reuse the A to express a constraint, e.g. trait Something[F[A] <: Iterable[A]].

As the book says, the kind constrains what things (types or type constructors) can be put there. You can have a Foldable[List] or a Foldable[Option], because these are 1-argument type constructors, but you can't have a Foldable[String] or a Foldable[Either]. Likewise you can't have a Foldable[List[Int]], because List[Int] is an ordinary type like String (i.e. of kind *). And you can have a foldable for the type that is T[A] = Either[String, A], because that is a 1-parameter type, aka a 1-argument type constructor, aka a type of kind * -> *, though you have to write it using the somewhat excruciating syntax Foldable[({type T[A]=Either[String, A]})#T]. And you can see that it would only be possible to implement the given foldRight for "types" (type constructors) F that have the correct "shape"; if F is Int, then what would F[A] be?

There is a different scala usage of F[_] to mean an existential type, F[A] forSome { type A }; try not to get confused by this, they're unreleated.

Upvotes: 2

CR Drost
CR Drost

Reputation: 9807

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.

Upvotes: 3

miguel
miguel

Reputation: 714

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).

Upvotes: 5

Related Questions